# Documentation

Mathlib.RingTheory.Etale

# Formally étale morphisms #

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

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

theorem Algebra.FormallyUnramified_iff (R : Type u) [] (A : Type u) [] [Algebra R A] :
∀ ⦃B : Type u⦄ [inst : ] [inst_1 : Algebra R B] (I : ), I ^ 2 =
class Algebra.FormallyUnramified (R : Type u) [] (A : Type u) [] [Algebra R A] :
• comp_injective : ∀ ⦃B : Type u⦄ [inst : ] [inst_1 : Algebra R B] (I : ), I ^ 2 =

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

Instances
theorem Algebra.FormallySmooth_iff (R : Type u) [] (A : Type u) [] [Algebra R A] :
∀ ⦃B : Type u⦄ [inst : ] [inst_1 : Algebra R B] (I : ), I ^ 2 =
class Algebra.FormallySmooth (R : Type u) [] (A : Type u) [] [Algebra R A] :
• comp_surjective : ∀ ⦃B : Type u⦄ [inst : ] [inst_1 : Algebra R B] (I : ), I ^ 2 =

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

Instances
theorem Algebra.FormallyEtale_iff (R : Type u) [] (A : Type u) [] [Algebra R A] :
∀ ⦃B : Type u⦄ [inst : ] [inst_1 : Algebra R B] (I : ), I ^ 2 =
class Algebra.FormallyEtale (R : Type u) [] (A : Type u) [] [Algebra R A] :
• comp_bijective : ∀ ⦃B : Type u⦄ [inst : ] [inst_1 : Algebra R B] (I : ), I ^ 2 =

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.

Instances
instance Algebra.FormallyEtale.to_unramified {R : Type u} [] {A : Type u} [] [Algebra R A] [h : ] :
instance Algebra.FormallyEtale.to_smooth {R : Type u} [] {A : Type u} [] [Algebra R A] [h : ] :
theorem Algebra.FormallyEtale.of_unramified_and_smooth {R : Type u} [] {A : Type u} [] [Algebra R A] [h₁ : ] [h₂ : ] :
theorem Algebra.FormallyUnramified.lift_unique {R : Type u} [] {A : Type u} [] [Algebra R A] {B : Type u} [] [_RB : Algebra R B] (I : ) (hI : ) (g₁ : A →ₐ[R] B) (g₂ : A →ₐ[R] B) (h : AlgHom.comp () g₁ = AlgHom.comp () g₂) :
g₁ = g₂
theorem Algebra.FormallyUnramified.ext {R : Type u} [] {A : Type u} [] [Algebra R A] {B : Type u} [] [Algebra R B] (I : ) (hI : ) {g₁ : A →ₐ[R] B} {g₂ : A →ₐ[R] B} (H : ∀ (x : A), ↑() (g₁ x) = ↑() (g₂ x)) :
g₁ = g₂
theorem Algebra.FormallyUnramified.lift_unique_of_ringHom {R : Type u} [] {A : Type u} [] [Algebra R A] {B : Type u} [] [Algebra R B] {C : Type u} [] (f : B →+* C) (hf : ) (g₁ : A →ₐ[R] B) (g₂ : A →ₐ[R] B) (h : RingHom.comp f g₁ = RingHom.comp f g₂) :
g₁ = g₂
theorem Algebra.FormallyUnramified.ext' {R : Type u} [] {A : Type u} [] [Algebra R A] {B : Type u} [] [Algebra R B] {C : Type u} [] (f : B →+* C) (hf : ) (g₁ : A →ₐ[R] B) (g₂ : A →ₐ[R] B) (h : ∀ (x : A), f (g₁ x) = f (g₂ x)) :
g₁ = g₂
theorem Algebra.FormallyUnramified.lift_unique' {R : Type u} [] {A : Type u} [] [Algebra R A] {B : Type u} [] [Algebra R B] {C : Type u} [] [Algebra R C] (f : B →ₐ[R] C) (hf : ) (g₁ : A →ₐ[R] B) (g₂ : A →ₐ[R] B) (h : AlgHom.comp f g₁ = AlgHom.comp f g₂) :
g₁ = g₂
theorem Algebra.FormallySmooth.exists_lift {R : Type u} [] {A : Type u} [] [Algebra R A] {B : Type u} [] [_RB : Algebra R B] [] (I : ) (hI : ) (g : A →ₐ[R] B I) :
f, = g
noncomputable def Algebra.FormallySmooth.lift {R : Type u} [] {A : Type u} [] [Algebra R A] {B : Type u} [] [Algebra R B] [] (I : ) (hI : ) (g : A →ₐ[R] B I) :

For a formally smooth R-algebra A and a map f : A →ₐ[R] B ⧸ I with I square-zero, this is an arbitrary lift A →ₐ[R] B.

Instances For
@[simp]
theorem Algebra.FormallySmooth.comp_lift {R : Type u} [] {A : Type u} [] [Algebra R A] {B : Type u} [] [Algebra R B] [] (I : ) (hI : ) (g : A →ₐ[R] B I) :
AlgHom.comp () () = g
@[simp]
theorem Algebra.FormallySmooth.mk_lift {R : Type u} [] {A : Type u} [] [Algebra R A] {B : Type u} [] [Algebra R B] [] (I : ) (hI : ) (g : A →ₐ[R] B I) (x : A) :
↑() (↑() x) = g x
noncomputable def Algebra.FormallySmooth.liftOfSurjective {R : Type u} [] {A : Type u} [] [Algebra R A] {B : Type u} [] [Algebra R B] {C : Type u} [] [Algebra R C] [] (f : A →ₐ[R] C) (g : B →ₐ[R] C) (hg : ) (hg' : ) :

For a formally smooth R-algebra A and a map f : A →ₐ[R] B ⧸ I with I nilpotent, this is an arbitrary lift A →ₐ[R] B.

Instances For
@[simp]
theorem Algebra.FormallySmooth.liftOfSurjective_apply {R : Type u} [] {A : Type u} [] [Algebra R A] {B : Type u} [] [Algebra R B] {C : Type u} [] [Algebra R C] [] (f : A →ₐ[R] C) (g : B →ₐ[R] C) (hg : ) (hg' : ) (x : A) :
g (↑() x) = f x
@[simp]
theorem Algebra.FormallySmooth.comp_liftOfSurjective {R : Type u} [] {A : Type u} [] [Algebra R A] {B : Type u} [] [Algebra R B] {C : Type u} [] [Algebra R C] [] (f : A →ₐ[R] C) (g : B →ₐ[R] C) (hg : ) (hg' : ) :
AlgHom.comp g () = f
theorem Algebra.FormallySmooth.of_equiv {R : Type u} [] {A : Type u} {B : Type u} [] [Algebra R A] [] [Algebra R B] [] (e : A ≃ₐ[R] B) :
theorem Algebra.FormallyUnramified.of_equiv {R : Type u} [] {A : Type u} {B : Type u} [] [Algebra R A] [] [Algebra R B] (e : A ≃ₐ[R] B) :
theorem Algebra.FormallyEtale.of_equiv {R : Type u} [] {A : Type u} {B : Type u} [] [Algebra R A] [] [Algebra R B] [] (e : A ≃ₐ[R] B) :
instance Algebra.FormallySmooth.mvPolynomial (R : Type u) [] (σ : Type u) :
theorem Algebra.FormallySmooth.comp (R : Type u) [] (A : Type u) [] [Algebra R A] (B : Type u) [] [Algebra R B] [Algebra A B] [] [] [] :
theorem Algebra.FormallyUnramified.comp (R : Type u) [] (A : Type u) [] [Algebra R A] (B : Type u) [] [Algebra R B] [Algebra A B] [] :
theorem Algebra.FormallyUnramified.of_comp (R : Type u) [] (A : Type u) [] [Algebra R A] (B : Type u) [] [Algebra R B] [Algebra A B] [] :
theorem Algebra.FormallyEtale.comp (R : Type u) [] (A : Type u) [] [Algebra R A] (B : Type u) [] [Algebra R B] [Algebra A B] [] [] [] :
theorem Algebra.FormallySmooth.of_split {R : Type u} [] {P : Type u} {A : Type u} [] [Algebra R A] [] [Algebra R P] (f : P →ₐ[R] A) [] (g : A →ₐ[R] P ^ 2) (hg : = ) :
theorem Algebra.FormallySmooth.iff_split_surjection {R : Type u} [] {P : Type u} {A : Type u} [] [Algebra R A] [] [Algebra R P] (f : P →ₐ[R] A) (hf : ) [] :
g, =

Let P →ₐ[R] A be a surjection with kernel J, and P a formally smooth R-algebra, then A is formally smooth over R iff the surjection P ⧸ J ^ 2 →ₐ[R] A has a section.

Geometric intuition: we require that a first-order thickening of Spec A inside Spec P admits a retraction.

instance Algebra.FormallyUnramified.base_change {R : Type u} [] {A : Type u} [] [Algebra R A] (B : Type u) [] [Algebra R B] :
instance Algebra.FormallySmooth.base_change {R : Type u} [] {A : Type u} [] [Algebra R A] (B : Type u) [] [Algebra R B] [] :
instance Algebra.FormallyEtale.base_change {R : Type u} [] {A : Type u} [] [Algebra R A] (B : Type u) [] [Algebra R B] [] :
theorem Algebra.FormallySmooth.of_isLocalization {R : Type u} {Rₘ : Type u} [] [CommRing Rₘ] (M : ) [Algebra R Rₘ] [] :
theorem Algebra.FormallyUnramified.of_isLocalization {R : Type u} {Rₘ : Type u} [] [CommRing Rₘ] (M : ) [Algebra R Rₘ] [] :

This holds in general for epimorphisms.

theorem Algebra.FormallyEtale.of_isLocalization {R : Type u} {Rₘ : Type u} [] [CommRing Rₘ] (M : ) [Algebra R Rₘ] [] :
theorem Algebra.FormallySmooth.localization_base {R : Type u} {Rₘ : Type u} {Sₘ : Type u} [] [CommRing Rₘ] [CommRing Sₘ] (M : ) [Algebra R Sₘ] [Algebra R Rₘ] [Algebra Rₘ Sₘ] [IsScalarTower R Rₘ Sₘ] [] [] :
theorem Algebra.FormallyUnramified.localization_base {R : Type u} {Rₘ : Type u} {Sₘ : Type u} [] [CommRing Rₘ] [CommRing Sₘ] (M : ) [Algebra R Sₘ] [Algebra R Rₘ] [Algebra Rₘ Sₘ] [IsScalarTower R Rₘ Sₘ] [] :

This actually does not need the localization instance, and is stated here again for consistency. See Algebra.FormallyUnramified.of_comp instead.

The intended use is for copying proofs between Formally{Unramified, Smooth, Etale} without the need to change anything (including removing redundant arguments).

theorem Algebra.FormallyEtale.localization_base {R : Type u} {Rₘ : Type u} {Sₘ : Type u} [] [CommRing Rₘ] [CommRing Sₘ] (M : ) [Algebra R Sₘ] [Algebra R Rₘ] [Algebra Rₘ Sₘ] [IsScalarTower R Rₘ Sₘ] [] [] :
theorem Algebra.FormallySmooth.localization_map {R : Type u} {S : Type u} {Rₘ : Type u} {Sₘ : Type u} [] [] [CommRing Rₘ] [CommRing Sₘ] (M : ) [Algebra R S] [Algebra R Sₘ] [Algebra S Sₘ] [Algebra R Rₘ] [Algebra Rₘ Sₘ] [IsScalarTower R Rₘ Sₘ] [IsScalarTower R S Sₘ] [] [IsLocalization (Submonoid.map () M) Sₘ] [] :
theorem Algebra.FormallyUnramified.localization_map {R : Type u} {S : Type u} {Rₘ : Type u} {Sₘ : Type u} [] [] [CommRing Rₘ] [CommRing Sₘ] (M : ) [Algebra R S] [Algebra R Sₘ] [Algebra S Sₘ] [Algebra R Rₘ] [Algebra Rₘ Sₘ] [IsScalarTower R Rₘ Sₘ] [IsScalarTower R S Sₘ] [IsLocalization (Submonoid.map () M) Sₘ] :
theorem Algebra.FormallyEtale.localization_map {R : Type u} {S : Type u} {Rₘ : Type u} {Sₘ : Type u} [] [] [CommRing Rₘ] [CommRing Sₘ] (M : ) [Algebra R S] [Algebra R Sₘ] [Algebra S Sₘ] [Algebra R Rₘ] [Algebra Rₘ Sₘ] [IsScalarTower R Rₘ Sₘ] [IsScalarTower R S Sₘ] [] [IsLocalization (Submonoid.map () M) Sₘ] [] :