Formally étale morphisms #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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
- comp_injective : ∀ ⦃B : Type ?⦄ [_inst_6 : comm_ring B] [_inst_7 : algebra R B] (I : ideal B), I ^ 2 = ⊥ → function.injective (ideal.quotient.mkₐ R I).comp
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
- comp_surjective : ∀ ⦃B : Type ?⦄ [_inst_6 : comm_ring B] [_inst_7 : algebra R B] (I : ideal B), I ^ 2 = ⊥ → function.surjective (ideal.quotient.mkₐ R I).comp
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.
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
- comp_bijective : ∀ ⦃B : Type ?⦄ [_inst_6 : comm_ring B] [_inst_7 : algebra R B] (I : ideal B), I ^ 2 = ⊥ → function.bijective (ideal.quotient.mkₐ R I).comp
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}
[comm_semiring R]
{A : Type u}
[semiring A]
[algebra R A] :
@[protected, instance]
def
algebra.formally_etale.to_unramified
{R : Type u}
[comm_semiring R]
{A : Type u}
[semiring A]
[algebra R A]
[h : algebra.formally_etale R A] :
@[protected, instance]
def
algebra.formally_etale.to_smooth
{R : Type u}
[comm_semiring R]
{A : Type u}
[semiring A]
[algebra R A]
[h : algebra.formally_etale R A] :
theorem
algebra.formally_etale.of_unramified_and_smooth
{R : Type u}
[comm_semiring R]
{A : Type u}
[semiring A]
[algebra R A]
[h₁ : algebra.formally_unramified R A]
[h₂ : algebra.formally_smooth R A] :
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_unramified.lift_unique_of_ring_hom
{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]
{C : Type u}
[comm_ring C]
(f : B →+* C)
(hf : is_nilpotent (ring_hom.ker f))
(g₁ g₂ : A →ₐ[R] B)
(h : f.comp ↑g₁ = f.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]
[algebra.formally_unramified R A]
{C : Type u}
[comm_ring C]
(f : B →+* C)
(hf : is_nilpotent (ring_hom.ker f))
(g₁ g₂ : A →ₐ[R] B)
(h : ∀ (x : A), ⇑f (⇑g₁ x) = ⇑f (⇑g₂ x)) :
g₁ = g₂
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]
{C : Type u}
[comm_ring C]
[algebra R C]
(f : B →ₐ[R] C)
(hf : is_nilpotent (ring_hom.ker ↑f))
(g₁ g₂ : A →ₐ[R] B)
(h : f.comp g₁ = f.comp g₂) :
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) :
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
- algebra.formally_smooth.lift I hI g = _.some
@[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) :
(ideal.quotient.mkₐ R I).comp (algebra.formally_smooth.lift I hI g) = g
@[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) :
⇑(ideal.quotient.mk I) (⇑(algebra.formally_smooth.lift I hI g) x) = ⇑g x
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) :
⇑g (⇑(algebra.formally_smooth.lift_of_surjective f g hg hg') x) = ⇑f x
@[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)) :
g.comp (algebra.formally_smooth.lift_of_surjective f g hg hg') = f
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_unramified.of_equiv
{R : Type u}
[comm_semiring R]
{A B : Type u}
[semiring A]
[algebra R A]
[semiring B]
[algebra R B]
[algebra.formally_unramified 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]
def
algebra.formally_smooth.mv_polynomial
(R : Type u)
[comm_semiring R]
(σ : Type u) :
algebra.formally_smooth R (mv_polynomial σ R)
@[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.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 A]
[algebra.formally_unramified 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) :
theorem
algebra.formally_smooth.iff_split_surjection
{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)
(hf : function.surjective ⇑f)
[algebra.formally_smooth R P] :
algebra.formally_smooth R A ↔ ∃ (g : A →ₐ[R] P ⧸ ring_hom.ker f.to_ring_hom ^ 2), 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]
def
algebra.formally_unramified.subsingleton_kaehler_differential
{R S : Type u}
[comm_ring R]
[comm_ring S]
[algebra R S]
[algebra.formally_unramified R S] :
theorem
algebra.formally_unramified.iff_subsingleton_kaehler_differential
{R S : Type u}
[comm_ring R]
[comm_ring S]
[algebra R S] :
@[protected, instance]
def
algebra.formally_unramified.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_unramified R A] :
algebra.formally_unramified B (tensor_product R B A)
@[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] :
algebra.formally_smooth B (tensor_product R B 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] :
algebra.formally_etale B (tensor_product R B 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ₘ] :
theorem
algebra.formally_unramified.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ₘ] :
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ₘ] :
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] :
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] :
algebra.formally_etale Rₘ Sₘ