Local structure of unramified algebras

In this file, we will prove that if S is a finite type R-algebra unramified at Q, then there exists f ∉ Q and a standard etale algebra A over R that surjects onto S[1/f]. Geometrically, this says that unramified morphisms locally are closed subsets of etale covers.

As a corollary, we also obtain results about the local structure of etale and smooth algebras.

Main definition and results

• HasStandardEtaleSurjectionOn: The predicate "there exists a standard etale algebra A over R that surjects onto S[1/f]".
• Algebra.IsUnramifiedAt.exists_hasStandardEtaleSurjectionOn: If S is a finite type R-algebra that is unramified at a prime p, then there exists a standard etale algebra over R that surjects onto S[1/f] for some f ∉ p.
• Algebra.IsEtaleAt.exists_isStandardEtale: If S is a finitely presented R-algebra that is etale at a prime p, then S[1/f] is standard etale for some f ∉ p.
• Algebra.IsSmoothAt.exists_isStandardEtale_mvPolynomial: If S is a finitely presented R-algebra that is smooth at a prime p, then there exists some f ∉ p such that S[1/f] is R-isomorphic to a standard etale algebra over R[x₁,...,xₙ].

def HasStandardEtaleSurjectionOn (R : Type u_1) {S : Type u_3} [CommRing R] [CommRing S] [Algebra R S] (f : S) : Prop

The predicate "there exists a standard etale algebra A over R that surjects onto S[1/f]". We shall show if S is R-unramified at Q then there exists f ∉ Q satisfying it.

theorem HasStandardEtaleSurjectionOn.mk {R : Type u_1} {A : Type u_2} {S : Type u_3} [CommRing R] [CommRing A] [CommRing S] [Algebra R S] [Algebra R A] [Algebra.IsStandardEtale R A] {Sf : Type u_4} [CommRing Sf] [Algebra R Sf] [Algebra S Sf] [IsScalarTower R S Sf] {f : S} [IsLocalization.Away f Sf] (φ : A →ₐ[R] Sf) (H : Function.Surjective ⇑φ) : HasStandardEtaleSurjectionOn R f

theorem HasStandardEtaleSurjectionOn.of_dvd {R : Type u_1} {S : Type u_3} [CommRing R] [CommRing S] [Algebra R S] {f g : S} (H : HasStandardEtaleSurjectionOn R f) (h : f ∣ g) : HasStandardEtaleSurjectionOn R g

theorem HasStandardEtaleSurjectionOn.isStandardEtale {R : Type u_1} {S : Type u_3} [CommRing R] [CommRing S] [Algebra R S] {f : S} (H : HasStandardEtaleSurjectionOn R f) [Algebra.Etale R (Localization.Away f)] : Algebra.IsStandardEtale R (Localization.Away f)

theorem Algebra.IsUnramifiedAt.exists_notMem_forall_ne_mem_and_adjoin_eq_top {R : Type u_1} {S : Type u_3} [CommRing R] [CommRing S] [Algebra R S] (Q : Ideal S) [Q.IsPrime] [Module.Finite R S] [IsUnramifiedAt R Q] : ∃ t ∉ Q, (∀ Q' ∈ (Ideal.under R Q).primesOver S, Q' ≠ Q → t ∈ Q') ∧ adjoin (Ideal.under R Q).ResidueField {(algebraMap S Q.ResidueField) t} = ⊤

theorem Algebra.IsUnramifiedAt.exists_primesOver_under_adjoin_eq_singleton_and_residueField_bijective {R : Type u_1} {S : Type u_3} [CommRing R] [CommRing S] [Algebra R S] (Q : Ideal S) [Q.IsPrime] [Module.Finite R S] [IsUnramifiedAt R Q] : ∃ (x : S), (Ideal.under (↥(adjoin R {x})) Q).primesOver S = {Q} ∧ Function.Bijective ⇑(algebraMap (Ideal.under (↥(adjoin R {x})) Q).ResidueField Q.ResidueField)

Let S be an finite R-algebra that is unramified at some prime Q. Then there exists some x : S such that Q is the unique prime lying over P := Q ∩ R⟨x⟩ and κ(P) = κ(Q).

@[instance 100]

instance Algebra.IsUnramifiedAt.instQuasiFiniteOfEssFiniteTypeOfFormallyUnramified {R : Type u_1} {S : Type u_3} [CommRing R] [CommRing S] [Algebra R S] [EssFiniteType R S] [FormallyUnramified R S] : QuasiFinite R S

theorem Algebra.IsUnramifiedAt.exists_hasStandardEtaleSurjectionOn {R : Type u_1} {S : Type u_3} [CommRing R] [CommRing S] [Algebra R S] (Q : Ideal S) [Q.IsPrime] [FiniteType R S] [IsUnramifiedAt R Q] : ∃ f ∉ Q, HasStandardEtaleSurjectionOn R f

theorem Algebra.IsEtaleAt.exists_isStandardEtale {R : Type u_1} {S : Type u_3} [CommRing R] [CommRing S] [Algebra R S] (Q : Ideal S) [Q.IsPrime] [FinitePresentation R S] [IsEtaleAt R Q] : ∃ f ∉ Q, IsStandardEtale R (Localization.Away f)

Stacks Tag 00UE

theorem Algebra.IsSmoothAt.exists_isStandardEtale_mvPolynomial {R : Type u_1} {S : Type u_3} [CommRing R] [CommRing S] [Algebra R S] {p : Ideal S} [p.IsPrime] [FinitePresentation R S] [IsSmoothAt R p] : ∃ f ∉ p, ∃ (n : ℕ) (x : Algebra (MvPolynomial (Fin n) R) (Localization.Away f)), IsScalarTower R (MvPolynomial (Fin n) R) (Localization.Away f) ∧ IsStandardEtale (MvPolynomial (Fin n) R) (Localization.Away f)

Given S a finitely presented R-algebra, and p a prime of S. If S is smooth over R at p, then there exists f ∉ p such that R → S[1/f] factors through some R[X₁,...,Xₙ], and that S[1/f] is standard etale over R[X₁,...,Xₙ].