Etale morphisms

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. 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.

TODO:

• Show that étale is stable under base change.

theorem Algebra.formallyEtale_iff (R : Type u) [CommSemiring R] (A : Type u) [Semiring 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 (AlgHom.comp (Ideal.Quotient.mkₐ R I))

class Algebra.FormallyEtale (R : Type u) [CommSemiring R] (A : Type u) [Semiring 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.

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

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

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

theorem Algebra.FormallyEtale.of_unramified_and_smooth {R : Type u} [CommSemiring R] {A : Type u} [Semiring 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} [CommSemiring R] {A : Type u} {B : Type u} [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] [Algebra.FormallyEtale R A] (e : A ≃ₐ[R] B) : Algebra.FormallyEtale R B

theorem Algebra.FormallyEtale.comp (R : Type u) [CommSemiring R] (A : Type u) [CommSemiring A] [Algebra R A] (B : Type u) [Semiring 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} [CommSemiring R] {A : Type u} [Semiring A] [Algebra R A] (B : Type u) [CommSemiring B] [Algebra R B] [Algebra.FormallyEtale R A] : Algebra.FormallyEtale B (TensorProduct R B A)

Equations

• ⋯ = ⋯

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

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

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

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

theorem Algebra.Etale.of_equiv {R : Type u} [CommRing R] {A : Type u} {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 : Type u) (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

Étale is stable under composition.

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.