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.

Main definition and results

• HasStandardEtaleSurjectionOn: The predicate "there exists a standard etale algebra A over R that surjects onto S[1/f]".
• Algebra.IsUnramified.exist_HasStandardEtaleSurjectionOn_of_exists_adjoin_singleton_eq_top: The claim is true when S has the form R[X]/I and is finite over R.

TODO (@erdOne)

• Extend the result to arbitrary finite algebras.
• Extend the result to arbitrary finite-type algebras (needs Zariski's main theorem).

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.

Equations

• HasStandardEtaleSurjectionOn R f = ∃ (P : StandardEtalePair R) (φ : P.Ring →ₐ[R] Localization.Away f), Function.Surjective ⇑φ

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_hasStandardEtaleSurjectionOn_of_exists_adjoin_singleton_eq_top {R : Type u_1} {S : Type u_3} [CommRing R] [CommRing S] [Algebra R S] [Module.Finite R S] (H : ∃ (x : S), adjoin R {x} = ⊤) (Q : Ideal S) [Q.IsPrime] [IsUnramifiedAt R Q] : ∃ f ∉ Q, HasStandardEtaleSurjectionOn R f