mathlib documentation

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) [comm_semiring R] (A : Type u) [semiring A] [algebra R A] :
algebra.formally_unramified R A ∀ ⦃B : Type u⦄ [_inst_6 : comm_ring B] [_inst_7 : algebra R B] (I : ideal B), I ^ 2 = function.injective (ideal.quotient.mkₐ R I).comp
@[class]
structure algebra.formally_unramified (R : Type u) [comm_semiring R] (A : Type u) [semiring A] [algebra R A] :
Prop

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) [comm_semiring R] (A : Type u) [semiring A] [algebra R A] :
algebra.formally_smooth R A ∀ ⦃B : Type u⦄ [_inst_6 : comm_ring B] [_inst_7 : algebra R B] (I : ideal B), I ^ 2 = function.surjective (ideal.quotient.mkₐ R I).comp
@[class]
structure algebra.formally_smooth (R : Type u) [comm_semiring R] (A : Type u) [semiring A] [algebra R A] :
Prop

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) [comm_semiring R] (A : Type u) [semiring A] [algebra R A] :
algebra.formally_etale R A ∀ ⦃B : Type u⦄ [_inst_6 : comm_ring B] [_inst_7 : algebra R B] (I : ideal B), I ^ 2 = function.bijective (ideal.quotient.mkₐ R I).comp
@[class]
structure algebra.formally_etale (R : Type u) [comm_semiring 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.

Instances of this typeclass
@[protected, instance]
@[protected, instance]
theorem algebra.formally_unramified.lift_unique {R : Type u} [comm_semiring R] {A : Type u} [semiring A] [algebra R A] {B : Type u} [comm_ring B] [algebra R B] [algebra.formally_unramified R A] (I : ideal B) (hI : is_nilpotent I) (g₁ g₂ : A →ₐ[R] B) (h : (ideal.quotient.mkₐ R I).comp g₁ = (ideal.quotient.mkₐ R I).comp g₂) :
g₁ = g₂
theorem algebra.formally_unramified.ext {R : Type u} [comm_semiring R] {A : Type u} [semiring A] [algebra R A] {B : Type u} [comm_ring B] [algebra R B] (I : ideal B) [algebra.formally_unramified R A] (hI : is_nilpotent I) {g₁ g₂ : A →ₐ[R] B} (H : ∀ (x : A), (ideal.quotient.mk I) (g₁ x) = (ideal.quotient.mk I) (g₂ x)) :
g₁ = g₂
theorem algebra.formally_smooth.exists_lift {R : Type u} [comm_semiring R] {A : Type u} [semiring A] [algebra R A] {B : Type u} [comm_ring B] [algebra R B] [algebra.formally_smooth R A] (I : ideal B) (hI : is_nilpotent I) (g : A →ₐ[R] B I) :
∃ (f : A →ₐ[R] B), (ideal.quotient.mkₐ R I).comp f = g
noncomputable def algebra.formally_smooth.lift {R : Type u} [comm_semiring R] {A : Type u} [semiring A] [algebra R A] {B : Type u} [comm_ring B] [algebra R B] [algebra.formally_smooth R A] (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} [comm_semiring R] {A : Type u} [semiring A] [algebra R A] {B : Type u} [comm_ring B] [algebra R B] [algebra.formally_smooth R A] (I : ideal B) (hI : is_nilpotent I) (g : A →ₐ[R] B I) :
@[simp]
theorem algebra.formally_smooth.mk_lift {R : Type u} [comm_semiring R] {A : Type u} [semiring A] [algebra R A] {B : Type u} [comm_ring B] [algebra R B] [algebra.formally_smooth R A] (I : ideal B) (hI : is_nilpotent I) (g : A →ₐ[R] B I) (x : A) :
noncomputable def algebra.formally_smooth.lift_of_surjective {R : Type u} [comm_semiring R] {A : Type u} [semiring A] [algebra R A] {B : Type u} [comm_ring B] [algebra R B] {C : Type u} [comm_ring C] [algebra R C] [algebra.formally_smooth R A] (f : A →ₐ[R] C) (g : B →ₐ[R] C) (hg : function.surjective g) (hg' : is_nilpotent (ring_hom.ker g)) :

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} [comm_semiring R] {A : Type u} [semiring A] [algebra R A] {B : Type u} [comm_ring B] [algebra R B] {C : Type u} [comm_ring C] [algebra R C] [algebra.formally_smooth R A] (f : A →ₐ[R] C) (g : B →ₐ[R] C) (hg : function.surjective g) (hg' : is_nilpotent (ring_hom.ker g)) (x : A) :
@[simp]
theorem algebra.formally_smooth.comp_lift_of_surjective {R : Type u} [comm_semiring R] {A : Type u} [semiring A] [algebra R A] {B : Type u} [comm_ring B] [algebra R B] {C : Type u} [comm_ring C] [algebra R C] [algebra.formally_smooth R A] (f : A →ₐ[R] C) (g : B →ₐ[R] C) (hg : function.surjective g) (hg' : is_nilpotent (ring_hom.ker g)) :
theorem algebra.formally_smooth.of_equiv {R : Type u} [comm_semiring R] {A B : Type u} [semiring A] [algebra R A] [semiring B] [algebra R B] [algebra.formally_smooth R A] (e : A ≃ₐ[R] B) :
theorem algebra.formally_etale.of_equiv {R : Type u} [comm_semiring R] {A B : Type u} [semiring A] [algebra R A] [semiring B] [algebra R B] [algebra.formally_etale R A] (e : A ≃ₐ[R] B) :
@[protected, instance]
@[protected, instance]
theorem algebra.formally_smooth.comp (R : Type u) [comm_semiring R] (A : Type u) [comm_semiring A] [algebra R A] (B : Type u) [semiring B] [algebra R B] [algebra A B] [is_scalar_tower R A B] [algebra.formally_smooth R A] [algebra.formally_smooth A B] :
theorem algebra.formally_unramified.of_comp (R : Type u) [comm_semiring R] (A : Type u) [comm_semiring A] [algebra R A] (B : Type u) [semiring B] [algebra R B] [algebra A B] [is_scalar_tower R A B] [algebra.formally_unramified R B] :
theorem algebra.formally_etale.comp (R : Type u) [comm_semiring R] (A : Type u) [comm_semiring A] [algebra R A] (B : Type u) [semiring B] [algebra R B] [algebra A B] [is_scalar_tower R A B] [algebra.formally_etale R A] [algebra.formally_etale A B] :
theorem algebra.formally_smooth.of_split {R : Type u} [comm_ring R] {P A : Type u} [comm_ring A] [algebra R A] [comm_ring P] [algebra R P] (f : P →ₐ[R] A) [algebra.formally_smooth R P] (g : A →ₐ[R] P ring_hom.ker f.to_ring_hom ^ 2) (hg : f.ker_square_lift.comp g = alg_hom.id R 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]
@[protected, instance]
def algebra.formally_smooth.base_change {R : Type u} [comm_semiring R] {A : Type u} [semiring A] [algebra R A] (B : Type u) [comm_semiring B] [algebra R B] [algebra.formally_smooth R A] :
@[protected, instance]
def algebra.formally_etale.base_change {R : Type u} [comm_semiring R] {A : Type u} [semiring A] [algebra R A] (B : Type u) [comm_semiring B] [algebra R B] [algebra.formally_etale R A] :
theorem algebra.formally_smooth.of_is_localization {R Rₘ : Type u} [comm_ring R] [comm_ring Rₘ] (M : submonoid R) [algebra R Rₘ] [is_localization M 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) [algebra R Rₘ] [is_localization M Rₘ] :
theorem algebra.formally_smooth.localization_base {R Rₘ Sₘ : Type u} [comm_ring R] [comm_ring Rₘ] [comm_ring Sₘ] (M : submonoid R) [algebra R Sₘ] [algebra R Rₘ] [algebra Rₘ Sₘ] [is_scalar_tower R Rₘ Sₘ] [is_localization M Rₘ] [algebra.formally_smooth 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) [algebra R Sₘ] [algebra R Rₘ] [algebra Rₘ Sₘ] [is_scalar_tower R Rₘ Sₘ] [is_localization M Rₘ] [algebra.formally_unramified R Sₘ] :

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) [algebra R Sₘ] [algebra R Rₘ] [algebra Rₘ Sₘ] [is_scalar_tower R Rₘ Sₘ] [is_localization M Rₘ] [algebra.formally_etale 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) [algebra R S] [algebra R Sₘ] [algebra S Sₘ] [algebra R Rₘ] [algebra Rₘ Sₘ] [is_scalar_tower R Rₘ Sₘ] [is_scalar_tower R S Sₘ] [is_localization M Rₘ] [is_localization (submonoid.map (algebra_map R S) M) Sₘ] [algebra.formally_smooth R 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) [algebra R S] [algebra R Sₘ] [algebra S Sₘ] [algebra R Rₘ] [algebra Rₘ Sₘ] [is_scalar_tower R Rₘ Sₘ] [is_scalar_tower R S Sₘ] [is_localization M Rₘ] [is_localization (submonoid.map (algebra_map R S) M) Sₘ] [algebra.formally_unramified R 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) [algebra R S] [algebra R Sₘ] [algebra S Sₘ] [algebra R Rₘ] [algebra Rₘ Sₘ] [is_scalar_tower R Rₘ Sₘ] [is_scalar_tower R S Sₘ] [is_localization M Rₘ] [is_localization (submonoid.map (algebra_map R S) M) Sₘ] [algebra.formally_etale R S] :