Etale morphisms

An R-algebra A is formally étale if 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. It 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) [CommRing R] (A : Type u) [CommRing A] [Algebra R A] : Prop

An R algebra A is formally étale if for every R-algebra, every square-zero ideal I : Ideal B and f : A →ₐ[R] B ⧸ I, there exists exactly one lift A →ₐ[R] B.

See https://stacks.math.columbia.edu/tag/00UQ

• comp_bijective ⦃B : Type u⦄ [CommRing B] [Algebra R B] (I : Ideal B) : I ^ 2 = ⊥ → Function.Bijective (Ideal.Quotient.mkₐ R I).comp

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

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

@[instance 100]

instance Algebra.FormallyEtale.to_unramified {R : Type u} [CommRing R] {A : Type u} [CommRing A] [Algebra R A] [h : Algebra.FormallyEtale R A] : Algebra.FormallyUnramified R A

@[instance 100]

instance Algebra.FormallyEtale.to_smooth {R : Type u} [CommRing R] {A : Type u} [CommRing A] [Algebra R A] [h : Algebra.FormallyEtale R A] : Algebra.FormallySmooth R A

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

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

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

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

instance Algebra.FormallyEtale.base_change {R : Type u} [CommRing R] {A : Type u} [CommRing A] [Algebra R A] (B : Type u) [CommRing B] [Algebra R B] [Algebra.FormallyEtale R A] : Algebra.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 Rₘ : Type u} [CommRing R] [CommRing Rₘ] (M : Submonoid R) [Algebra R Rₘ] [IsLocalization M Rₘ] : Algebra.FormallyEtale R Rₘ

theorem Algebra.FormallyEtale.localization_base {R Rₘ Sₘ : Type u} [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ₘ] [Algebra.FormallyEtale R Sₘ] : Algebra.FormallyEtale Rₘ Sₘ

theorem Algebra.FormallyEtale.localization_map {R S Rₘ Sₘ : Type u} [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ₘ] [Algebra.FormallyEtale R S] : Algebra.FormallyEtale Rₘ Sₘ

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

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

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

Note that the definition https://stacks.math.columbia.edu/tag/00U1 in the stacks project is different, but https://stacks.math.columbia.edu/tag/00UR shows that it is equivalent to the definition here.

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

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

Being étale is transported via algebra isomorphisms.

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

Etale is stable under composition.

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

Etale is stable under base change.

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

Localization at an element is étale.