Étale morphisms

An R-algebra A is formally etale if Ω[A⁄R] and H¹(L_{A/R}) both vanish. This is equivalent to the standard definition that "for every R-algebra B, every square-zero ideal I : Ideal B and f : A →ₐ[R] B ⧸ I, there exists exactly one lift A →ₐ[R] B". An R-algebra A is étale if it is formally étale and of finite presentation.

We show that the property extends onto nilpotent ideals, and that these properties are stable under R-algebra homomorphisms and compositions.

We show that étale is stable under algebra isomorphisms, composition and localization at an element.

class Algebra.FormallyEtale (R : Type u) (A : Type v) [CommRing R] [CommRing A] [Algebra R A] : Prop

An R-algebra A is formally etale if both Ω[A⁄R] and H¹(L_{A/R}) are zero. For the infinitesimal lifting definition, see FormallyEtale.iff_comp_bijective.

• subsingleton_kaehlerDifferential : Subsingleton Ω[A⁄R]
• subsingleton_h1Cotangent : Subsingleton (H1Cotangent R A)

theorem Algebra.formallyEtale_iff (R : Type u) (A : Type v) [CommRing R] [CommRing A] [Algebra R A] : FormallyEtale R A ↔ Subsingleton Ω[A⁄R] ∧ Subsingleton (H1Cotangent R A)

@[instance 100]

instance Algebra.FormallyEtale.instFormallyUnramified {R : Type u} {A : Type v} [CommRing R] [CommRing A] [Algebra R A] [FormallyEtale R A] : FormallyUnramified R A

@[instance 100]

instance Algebra.FormallyEtale.instFormallySmooth {R : Type u} {A : Type v} [CommRing R] [CommRing A] [Algebra R A] [FormallyEtale R A] : FormallySmooth R A

theorem Algebra.FormallyEtale.iff_formallyUnramified_and_formallySmooth {R : Type u} {A : Type v} [CommRing R] [CommRing A] [Algebra R A] : FormallyEtale R A ↔ FormallyUnramified R A ∧ FormallySmooth R A

@[deprecated Algebra.FormallyEtale.iff_formallyUnramified_and_formallySmooth (since := "2025-11-03")]

theorem Algebra.FormallyEtale.iff_unramified_and_smooth {R : Type u} {A : Type v} [CommRing R] [CommRing A] [Algebra R A] : FormallyEtale R A ↔ FormallyUnramified R A ∧ FormallySmooth R A

Alias of Algebra.FormallyEtale.iff_formallyUnramified_and_formallySmooth.

theorem Algebra.FormallyEtale.of_formallyUnramified_and_formallySmooth {R : Type u} {A : Type v} [CommRing R] [CommRing A] [Algebra R A] [FormallyUnramified R A] [FormallySmooth R A] : FormallyEtale R A

@[deprecated Algebra.FormallyEtale.of_formallyUnramified_and_formallySmooth (since := "2025-11-03")]

theorem Algebra.FormallyEtale.of_unramified_and_smooth {R : Type u} {A : Type v} [CommRing R] [CommRing A] [Algebra R A] [FormallyUnramified R A] [FormallySmooth R A] : FormallyEtale R A

Alias of Algebra.FormallyEtale.of_formallyUnramified_and_formallySmooth.

theorem Algebra.FormallyEtale.comp_bijective (R : Type u) (A : Type v) {B : Type u_1} [CommRing R] [CommRing A] [Algebra R A] [CommRing B] [Algebra R B] [FormallyEtale R A] (I : Ideal B) (hI : I ^ 2 = ⊥) : Function.Bijective (Ideal.Quotient.mkₐ R I).comp

theorem Algebra.FormallyEtale.iff_comp_bijective {R : Type u} {A : Type v} [CommRing R] [CommRing A] [Algebra R A] : FormallyEtale R A ↔ ∀ ⦃B : Type (max u v)⦄ [inst : CommRing B] [inst_1 : Algebra R B] (I : Ideal B), I ^ 2 = ⊥ → Function.Bijective (Ideal.Quotient.mkₐ R I).comp

An R-algebra A is formally etale iff "for every R-algebra B, every square-zero ideal I : Ideal B and f : A →ₐ[R] B ⧸ I, there exists a unique lift A →ₐ[R] B".

theorem Algebra.FormallyEtale.of_equiv {R : Type u} {A : Type v} {B : Type u_1} [CommRing R] [CommRing A] [Algebra R A] [CommRing B] [Algebra R B] [FormallyEtale R A] (e : A ≃ₐ[R] B) : FormallyEtale R B

theorem Algebra.FormallyEtale.iff_of_equiv {R : Type u} {A : Type v} {B : Type u_1} [CommRing R] [CommRing A] [Algebra R A] [CommRing B] [Algebra R B] (e : A ≃ₐ[R] B) : FormallyEtale R A ↔ FormallyEtale R B

theorem Algebra.FormallyEtale.comp (R : Type u) (A : Type v) (B : Type u_1) [CommRing R] [CommRing A] [Algebra R A] [CommRing B] [Algebra R B] [Algebra A B] [IsScalarTower R A B] [FormallyEtale R A] [FormallyEtale A B] : FormallyEtale R B

theorem Algebra.FormallyEtale.Algebra.FormallyEtale.of_restrictScalars {R : Type u} {A : Type v} {B : Type u_1} [CommRing R] [CommRing A] [Algebra R A] [CommRing B] [Algebra R B] [Algebra A B] [IsScalarTower R A B] [FormallyUnramified R A] [FormallyEtale R B] : FormallyEtale A B

theorem Algebra.FormallyEtale.Algebra.FormallyEtale.iff_of_surjective {R S : Type u} [CommRing R] [CommRing S] [Algebra R S] (h : Function.Surjective ⇑(algebraMap R S)) : FormallyEtale R S ↔ IsIdempotentElem (RingHom.ker (algebraMap R S))

instance Algebra.FormallyEtale.instTensorProduct {R : Type u} {A : Type v} {B : Type u_1} [CommRing R] [CommRing A] [Algebra R A] [CommRing B] [Algebra R B] [FormallyEtale R A] : FormallyEtale B (TensorProduct R B A)

We now consider a commutative square of commutative rings

R -----> S
|        |
|        |
v        v
Rₘ ----> Sₘ

where Rₘ and Sₘ are the localisations of R and S at a multiplicatively closed subset M of R.

Let R, S, Rₘ, Sₘ be commutative rings

Let M be a multiplicatively closed subset of R

Assume that the rings are in a commutative diagram as above.

and that Rₘ and Sₘ are localizations of R and S at M.

theorem Algebra.FormallyEtale.of_isLocalization {R : Type u_2} {Rₘ : Type u_4} [CommRing R] [CommRing Rₘ] (M : Submonoid R) [Algebra R Rₘ] [IsLocalization M Rₘ] : FormallyEtale R Rₘ

theorem Algebra.FormallyEtale.localization_base {R : Type u_2} {Rₘ : Type u_4} {Sₘ : Type u_5} [CommRing R] [CommRing Rₘ] [CommRing Sₘ] (M : Submonoid R) [Algebra R Sₘ] [Algebra R Rₘ] [Algebra Rₘ Sₘ] [IsScalarTower R Rₘ Sₘ] [IsLocalization M Rₘ] [FormallyEtale R Sₘ] : FormallyEtale Rₘ Sₘ

theorem Algebra.FormallyEtale.localization_map {R : Type u_2} {S : Type u_3} {Rₘ : Type u_4} {Sₘ : Type u_5} [CommRing R] [CommRing S] [CommRing Rₘ] [CommRing Sₘ] (M : Submonoid R) [Algebra R S] [Algebra R Sₘ] [Algebra S Sₘ] [Algebra R Rₘ] [Algebra Rₘ Sₘ] [IsScalarTower R Rₘ Sₘ] [IsScalarTower R S Sₘ] [IsLocalization M Rₘ] [IsLocalization (Submonoid.map (algebraMap R S) M) Sₘ] [FormallyEtale R S] : FormallyEtale Rₘ Sₘ

The localization of a formally étale map is formally étale.

class Algebra.Etale (R : Type u) (A : Type v) [CommRing R] [CommRing A] [Algebra R A] : Prop

An R-algebra A is étale if it is formally étale and of finite presentation.

• formallyEtale : FormallyEtale R A
• finitePresentation : FinitePresentation R A

theorem Algebra.Etale.of_equiv {R : Type u} {A : Type v} {B : Type u_1} [CommRing R] [CommRing A] [Algebra R A] [CommRing B] [Algebra R B] [Etale R A] (e : A ≃ₐ[R] B) : Etale R B

Being étale is transported via algebra isomorphisms.

theorem Algebra.Etale.comp (R : Type u) (A : Type v) (B : Type u_1) [CommRing R] [CommRing A] [Algebra R A] [CommRing B] [Algebra R B] [Algebra A B] [IsScalarTower R A B] [Etale R A] [Etale A B] : Etale R B

Étale is stable under composition.

instance Algebra.Etale.baseChange (R : Type u) (A : Type v) (B : Type u_1) [CommRing R] [CommRing A] [Algebra R A] [CommRing B] [Algebra R B] [Etale R A] : Etale B (TensorProduct R B A)

Étale is stable under base change.

theorem Algebra.Etale.of_isLocalizationAway {R : Type u} {A : Type v} [CommRing R] [CommRing A] [Algebra R A] (r : R) [IsLocalization.Away r A] : Etale R A

Localization at an element is étale.

@[deprecated Algebra.Etale.of_isLocalizationAway (since := "2025-11-03")]

theorem Algebra.Etale.of_isLocalization_Away {R : Type u} {A : Type v} [CommRing R] [CommRing A] [Algebra R A] (r : R) [IsLocalization.Away r A] : Etale R A

Alias of Algebra.Etale.of_isLocalizationAway.

---

Localization at an element is étale.

def RingHom.FormallyEtale {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] (f : R →+* S) : Prop

A ring homomorphism R →+* A is formally étale if it is formally unramified and formally smooth. See Algebra.FormallyEtale.

Equations

• f.FormallyEtale = Algebra.FormallyEtale R S

theorem RingHom.formallyEtale_algebraMap {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] : (algebraMap R S).FormallyEtale ↔ Algebra.FormallyEtale R S