Algebra.exists_etale_isFiniteSplit
A finite étale algebra becomes a finite product of the base on an étale neighbourhood of any prescribed prime. No constant-rank hypothesis is needed.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
@[expose] public section
open TensorProduct
universe u
namespace Algebra
variable {R A : Type u} [CommRing R] [CommRing A] [Algebra R A]Lean source · statement
lemma exists_etale_isFiniteSplit [Module.Finite R A] [Algebra.Etale R A]
(p : PrimeSpectrum R) :
∃ (S : Type u) (_ : CommRing S) (_ : Algebra R S),
Algebra.Etale R S ∧
p ∈ Set.range (PrimeSpectrum.comap (algebraMap R S)) ∧
Algebra.IsFiniteSplit S (S ⊗[R] A)