# mathlibdocumentation

ring_theory.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.formally_unramified_iff (R : Type u) (A : Type u) [semiring A] [ A] :
∀ ⦃B : Type u⦄ [_inst_6 : [_inst_7 : B] (I : ideal B), I ^ 2 =
@[class]
structure algebra.formally_unramified (R : Type u) (A : Type u) [semiring A] [ A] :
Prop
• comp_injective : ∀ ⦃B : Type ?⦄ [_inst_6 : [_inst_7 : B] (I : ideal B), 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 of this typeclass
theorem algebra.formally_smooth_iff (R : Type u) (A : Type u) [semiring A] [ A] :
∀ ⦃B : Type u⦄ [_inst_6 : [_inst_7 : B] (I : ideal B), I ^ 2 =
@[class]
structure algebra.formally_smooth (R : Type u) (A : Type u) [semiring A] [ A] :
Prop
• comp_surjective : ∀ ⦃B : Type ?⦄ [_inst_6 : [_inst_7 : B] (I : ideal B), 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 of this typeclass
theorem algebra.formally_etale_iff (R : Type u) (A : Type u) [semiring A] [ A] :
∀ ⦃B : Type u⦄ [_inst_6 : [_inst_7 : B] (I : ideal B), I ^ 2 =
@[class]
structure algebra.formally_etale (R : Type u) (A : Type u) [semiring A] [ A] :
Prop
• comp_bijective : ∀ ⦃B : Type ?⦄ [_inst_6 : [_inst_7 : B] (I : ideal B), 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 of this typeclass
theorem algebra.formally_etale.iff_unramified_and_smooth {R : Type u} {A : Type u} [semiring A] [ A] :
@[protected, instance]
def algebra.formally_etale.to_unramified {R : Type u} {A : Type u} [semiring A] [ A] [h : A] :
@[protected, instance]
def algebra.formally_etale.to_smooth {R : Type u} {A : Type u} [semiring A] [ A] [h : A] :
theorem algebra.formally_etale.of_unramified_and_smooth {R : Type u} {A : Type u} [semiring A] [ A] [h₁ : A] [h₂ : A] :
theorem algebra.formally_unramified.lift_unique {R : Type u} {A : Type u} [semiring A] [ A] {B : Type u} [comm_ring B] [ B] (I : ideal B) (hI : is_nilpotent I) (g₁ g₂ : A →ₐ[R] B) (h : I).comp g₁ = I).comp g₂) :
g₁ = g₂
theorem algebra.formally_unramified.ext {R : Type u} {A : Type u} [semiring A] [ A] {B : Type u} [comm_ring B] [ B] (I : ideal B) (hI : is_nilpotent I) {g₁ g₂ : A →ₐ[R] B} (H : ∀ (x : A), (g₁ x) = (g₂ x)) :
g₁ = g₂
theorem algebra.formally_smooth.exists_lift {R : Type u} {A : Type u} [semiring A] [ A] {B : Type u} [comm_ring B] [ B] (I : ideal B) (hI : is_nilpotent I) (g : A →ₐ[R] B I) :
∃ (f : A →ₐ[R] B), I).comp f = g
noncomputable def algebra.formally_smooth.lift {R : Type u} {A : Type u} [semiring A] [ A] {B : Type u} [comm_ring B] [ B] (I : ideal B) (hI : is_nilpotent I) (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.

Equations
@[simp]
theorem algebra.formally_smooth.comp_lift {R : Type u} {A : Type u} [semiring A] [ A] {B : Type u} [comm_ring B] [ B] (I : ideal B) (hI : is_nilpotent I) (g : A →ₐ[R] B I) :
I).comp g) = g
@[simp]
theorem algebra.formally_smooth.mk_lift {R : Type u} {A : Type u} [semiring A] [ A] {B : Type u} [comm_ring B] [ B] (I : ideal B) (hI : is_nilpotent I) (g : A →ₐ[R] B I) (x : A) :
( g) x) = g x
noncomputable def algebra.formally_smooth.lift_of_surjective {R : Type u} {A : Type u} [semiring A] [ A] {B : Type u} [comm_ring B] [ B] {C : Type u} [comm_ring C] [ C] (f : A →ₐ[R] C) (g : B →ₐ[R] C) (hg : function.surjective g) (hg' : is_nilpotent ) :

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.

Equations
@[simp]
theorem algebra.formally_smooth.lift_of_surjective_apply {R : Type u} {A : Type u} [semiring A] [ A] {B : Type u} [comm_ring B] [ B] {C : Type u} [comm_ring C] [ C] (f : A →ₐ[R] C) (g : B →ₐ[R] C) (hg : function.surjective g) (hg' : is_nilpotent ) (x : A) :
g ( hg') x) = f x
@[simp]
theorem algebra.formally_smooth.comp_lift_of_surjective {R : Type u} {A : Type u} [semiring A] [ A] {B : Type u} [comm_ring B] [ B] {C : Type u} [comm_ring C] [ C] (f : A →ₐ[R] C) (g : B →ₐ[R] C) (hg : function.surjective g) (hg' : is_nilpotent ) :
g.comp hg') = f
theorem algebra.formally_smooth.of_equiv {R : Type u} {A B : Type u} [semiring A] [ A] [semiring B] [ B] (e : A ≃ₐ[R] B) :
theorem algebra.formally_unramified.of_equiv {R : Type u} {A B : Type u} [semiring A] [ A] [semiring B] [ B] (e : A ≃ₐ[R] B) :
theorem algebra.formally_etale.of_equiv {R : Type u} {A B : Type u} [semiring A] [ A] [semiring B] [ B] (e : A ≃ₐ[R] B) :
@[protected, instance]
def algebra.formally_smooth.mv_polynomial (R : Type u) (σ : Type u) :
@[protected, instance]
def algebra.formally_smooth.polynomial (R : Type u)  :
theorem algebra.formally_smooth.comp (R : Type u) (A : Type u) [ A] (B : Type u) [semiring B] [ B] [ B] [ B]  :
theorem algebra.formally_unramified.comp (R : Type u) (A : Type u) [ A] (B : Type u) [semiring B] [ B] [ B] [ B]  :
theorem algebra.formally_unramified.of_comp (R : Type u) (A : Type u) [ A] (B : Type u) [semiring B] [ B] [ B] [ B]  :
theorem algebra.formally_etale.comp (R : Type u) (A : Type u) [ A] (B : Type u) [semiring B] [ B] [ B] [ B]  :
theorem algebra.formally_smooth.of_split {R : Type u} [comm_ring R] {P A : Type u} [comm_ring A] [ A] [comm_ring P] [ P] (f : P →ₐ[R] A) (g : A →ₐ[R] P ) (hg : = A) :
theorem algebra.formally_smooth.iff_split_surjection {R : Type u} [comm_ring R] {P A : Type u} [comm_ring A] [ A] [comm_ring P] [ P] (f : P →ₐ[R] A) (hf : function.surjective f)  :
∃ (g : A →ₐ[R] P , = A

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.

@[protected, instance]
def algebra.formally_unramified.base_change {R : Type u} {A : Type u} [semiring A] [ A] (B : Type u) [ B]  :
@[protected, instance]
def algebra.formally_smooth.base_change {R : Type u} {A : Type u} [semiring A] [ A] (B : Type u) [ B]  :
B A)
@[protected, instance]
def algebra.formally_etale.base_change {R : Type u} {A : Type u} [semiring A] [ A] (B : Type u) [ B]  :
B A)
theorem algebra.formally_smooth.of_is_localization {R Rₘ : Type u} [comm_ring R] [comm_ring Rₘ] (M : submonoid R) [ Rₘ] [ Rₘ] :
theorem algebra.formally_unramified.of_is_localization {R Rₘ : Type u} [comm_ring R] [comm_ring Rₘ] (M : submonoid R) [ Rₘ] [ Rₘ] :

This holds in general for epimorphisms.

theorem algebra.formally_etale.of_is_localization {R Rₘ : Type u} [comm_ring R] [comm_ring Rₘ] (M : submonoid R) [ Rₘ] [ Rₘ] :
theorem algebra.formally_smooth.localization_base {R Rₘ Sₘ : Type u} [comm_ring R] [comm_ring Rₘ] [comm_ring Sₘ] (M : submonoid R) [ Sₘ] [ Rₘ] [algebra Rₘ Sₘ] [ Rₘ Sₘ] [ Rₘ] [ Sₘ] :
@[nolint]
theorem algebra.formally_unramified.localization_base {R Rₘ Sₘ : Type u} [comm_ring R] [comm_ring Rₘ] [comm_ring Sₘ] (M : submonoid R) [ Sₘ] [ Rₘ] [algebra Rₘ Sₘ] [ Rₘ Sₘ] [ Rₘ]  :

This actually does not need the localization instance, and is stated here again for consistency. See algebra.formally_unramified.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.formally_etale.localization_base {R Rₘ Sₘ : Type u} [comm_ring R] [comm_ring Rₘ] [comm_ring Sₘ] (M : submonoid R) [ Sₘ] [ Rₘ] [algebra Rₘ Sₘ] [ Rₘ Sₘ] [ Rₘ] [ Sₘ] :
theorem algebra.formally_smooth.localization_map {R S Rₘ Sₘ : Type u} [comm_ring R] [comm_ring S] [comm_ring Rₘ] [comm_ring Sₘ] (M : submonoid R) [ S] [ Sₘ] [ Sₘ] [ Rₘ] [algebra Rₘ Sₘ] [ Rₘ Sₘ] [ Sₘ] [ Rₘ] [is_localization (submonoid.map S) M) Sₘ]  :
theorem algebra.formally_unramified.localization_map {R S Rₘ Sₘ : Type u} [comm_ring R] [comm_ring S] [comm_ring Rₘ] [comm_ring Sₘ] (M : submonoid R) [ S] [ Sₘ] [ Sₘ] [ Rₘ] [algebra Rₘ Sₘ] [ Rₘ Sₘ] [ Sₘ] [ Rₘ] [is_localization (submonoid.map S) M) Sₘ]  :
theorem algebra.formally_etale.localization_map {R S Rₘ Sₘ : Type u} [comm_ring R] [comm_ring S] [comm_ring Rₘ] [comm_ring Sₘ] (M : submonoid R) [ S] [ Sₘ] [ Sₘ] [ Rₘ] [algebra Rₘ Sₘ] [ Rₘ Sₘ] [ Sₘ] [ Rₘ] [is_localization (submonoid.map S) M) Sₘ]  :