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)
[CommSemiring R]
(A : Type u)
[Semiring A]
[Algebra R A]
:
Algebra.FormallyUnramified R A ↔ ∀ ⦃B : Type u⦄ [inst : CommRing B] [inst_1 : Algebra R B] (I : Ideal B),
I ^ 2 = ⊥ → Function.Injective (AlgHom.comp (Ideal.Quotient.mkₐ R I))
class
Algebra.FormallyUnramified
(R : Type u)
[CommSemiring R]
(A : Type u)
[Semiring A]
[Algebra R A]
:
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.
- comp_injective : ∀ ⦃B : Type u⦄ [inst : CommRing B] [inst_1 : Algebra R B] (I : Ideal B), I ^ 2 = ⊥ → Function.Injective (AlgHom.comp (Ideal.Quotient.mkₐ R I))
Instances
theorem
Algebra.formallySmooth_iff
(R : Type u)
[CommSemiring R]
(A : Type u)
[Semiring A]
[Algebra R A]
:
Algebra.FormallySmooth R A ↔ ∀ ⦃B : Type u⦄ [inst : CommRing B] [inst_1 : Algebra R B] (I : Ideal B),
I ^ 2 = ⊥ → Function.Surjective (AlgHom.comp (Ideal.Quotient.mkₐ R I))
class
Algebra.FormallySmooth
(R : Type u)
[CommSemiring R]
(A : Type u)
[Semiring A]
[Algebra R A]
:
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.
- comp_surjective : ∀ ⦃B : Type u⦄ [inst : CommRing B] [inst_1 : Algebra R B] (I : Ideal B), I ^ 2 = ⊥ → Function.Surjective (AlgHom.comp (Ideal.Quotient.mkₐ R I))
Instances
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))
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))
Instances
theorem
Algebra.FormallyEtale.iff_unramified_and_smooth
{R : Type u}
[CommSemiring R]
{A : Type u}
[Semiring A]
[Algebra 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]
:
Equations
- (_ : Algebra.FormallyUnramified R A) = (_ : Algebra.FormallyUnramified R A)
instance
Algebra.FormallyEtale.to_smooth
{R : Type u}
[CommSemiring R]
{A : Type u}
[Semiring A]
[Algebra R A]
[h : Algebra.FormallyEtale R A]
:
Equations
- (_ : Algebra.FormallySmooth R A) = (_ : Algebra.FormallySmooth R A)
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]
:
theorem
Algebra.FormallyUnramified.lift_unique
{R : Type u}
[CommSemiring R]
{A : Type u}
[Semiring A]
[Algebra R A]
{B : Type u}
[CommRing B]
[_RB : Algebra R B]
[Algebra.FormallyUnramified R A]
(I : Ideal B)
(hI : IsNilpotent I)
(g₁ : A →ₐ[R] B)
(g₂ : A →ₐ[R] B)
(h : AlgHom.comp (Ideal.Quotient.mkₐ R I) g₁ = AlgHom.comp (Ideal.Quotient.mkₐ R I) g₂)
:
g₁ = g₂
theorem
Algebra.FormallyUnramified.ext
{R : Type u}
[CommSemiring R]
{A : Type u}
[Semiring A]
[Algebra R A]
{B : Type u}
[CommRing B]
[Algebra R B]
(I : Ideal B)
[Algebra.FormallyUnramified R A]
(hI : IsNilpotent I)
{g₁ : A →ₐ[R] B}
{g₂ : A →ₐ[R] B}
(H : ∀ (x : A), (Ideal.Quotient.mk I) (g₁ x) = (Ideal.Quotient.mk I) (g₂ x))
:
g₁ = g₂
theorem
Algebra.FormallyUnramified.lift_unique_of_ringHom
{R : Type u}
[CommSemiring R]
{A : Type u}
[Semiring A]
[Algebra R A]
{B : Type u}
[CommRing B]
[Algebra R B]
[Algebra.FormallyUnramified R A]
{C : Type u}
[CommRing C]
(f : B →+* C)
(hf : IsNilpotent (RingHom.ker f))
(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}
[CommSemiring R]
{A : Type u}
[Semiring A]
[Algebra R A]
{B : Type u}
[CommRing B]
[Algebra R B]
[Algebra.FormallyUnramified R A]
{C : Type u}
[CommRing C]
(f : B →+* C)
(hf : IsNilpotent (RingHom.ker f))
(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}
[CommSemiring R]
{A : Type u}
[Semiring A]
[Algebra R A]
{B : Type u}
[CommRing B]
[Algebra R B]
[Algebra.FormallyUnramified R A]
{C : Type u}
[CommRing C]
[Algebra R C]
(f : B →ₐ[R] C)
(hf : IsNilpotent (RingHom.ker ↑f))
(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}
[CommSemiring R]
{A : Type u}
[Semiring A]
[Algebra R A]
{B : Type u}
[CommRing B]
[_RB : Algebra R B]
[Algebra.FormallySmooth R A]
(I : Ideal B)
(hI : IsNilpotent I)
(g : A →ₐ[R] B ⧸ I)
:
∃ (f : A →ₐ[R] B), AlgHom.comp (Ideal.Quotient.mkₐ R I) f = g
noncomputable def
Algebra.FormallySmooth.lift
{R : Type u}
[CommSemiring R]
{A : Type u}
[Semiring A]
[Algebra R A]
{B : Type u}
[CommRing B]
[Algebra R B]
[Algebra.FormallySmooth R A]
(I : Ideal B)
(hI : IsNilpotent 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.FormallySmooth.lift I hI g = Exists.choose (_ : ∃ (f : A →ₐ[R] B), AlgHom.comp (Ideal.Quotient.mkₐ R I) f = g)
Instances For
@[simp]
theorem
Algebra.FormallySmooth.comp_lift
{R : Type u}
[CommSemiring R]
{A : Type u}
[Semiring A]
[Algebra R A]
{B : Type u}
[CommRing B]
[Algebra R B]
[Algebra.FormallySmooth R A]
(I : Ideal B)
(hI : IsNilpotent I)
(g : A →ₐ[R] B ⧸ I)
:
AlgHom.comp (Ideal.Quotient.mkₐ R I) (Algebra.FormallySmooth.lift I hI g) = g
@[simp]
theorem
Algebra.FormallySmooth.mk_lift
{R : Type u}
[CommSemiring R]
{A : Type u}
[Semiring A]
[Algebra R A]
{B : Type u}
[CommRing B]
[Algebra R B]
[Algebra.FormallySmooth R A]
(I : Ideal B)
(hI : IsNilpotent I)
(g : A →ₐ[R] B ⧸ I)
(x : A)
:
(Ideal.Quotient.mk I) ((Algebra.FormallySmooth.lift I hI g) x) = g x
noncomputable def
Algebra.FormallySmooth.liftOfSurjective
{R : Type u}
[CommSemiring R]
{A : Type u}
[Semiring A]
[Algebra R A]
{B : Type u}
[CommRing B]
[Algebra R B]
{C : Type u}
[CommRing C]
[Algebra R C]
[Algebra.FormallySmooth R A]
(f : A →ₐ[R] C)
(g : B →ₐ[R] C)
(hg : Function.Surjective ⇑g)
(hg' : IsNilpotent (RingHom.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
- Algebra.FormallySmooth.liftOfSurjective f g hg hg' = Algebra.FormallySmooth.lift (RingHom.ker ↑g) hg' (AlgHom.comp (↑(AlgEquiv.symm (Ideal.quotientKerAlgEquivOfSurjective hg))) f)
Instances For
@[simp]
theorem
Algebra.FormallySmooth.liftOfSurjective_apply
{R : Type u}
[CommSemiring R]
{A : Type u}
[Semiring A]
[Algebra R A]
{B : Type u}
[CommRing B]
[Algebra R B]
{C : Type u}
[CommRing C]
[Algebra R C]
[Algebra.FormallySmooth R A]
(f : A →ₐ[R] C)
(g : B →ₐ[R] C)
(hg : Function.Surjective ⇑g)
(hg' : IsNilpotent (RingHom.ker ↑g))
(x : A)
:
g ((Algebra.FormallySmooth.liftOfSurjective f g hg hg') x) = f x
@[simp]
theorem
Algebra.FormallySmooth.comp_liftOfSurjective
{R : Type u}
[CommSemiring R]
{A : Type u}
[Semiring A]
[Algebra R A]
{B : Type u}
[CommRing B]
[Algebra R B]
{C : Type u}
[CommRing C]
[Algebra R C]
[Algebra.FormallySmooth R A]
(f : A →ₐ[R] C)
(g : B →ₐ[R] C)
(hg : Function.Surjective ⇑g)
(hg' : IsNilpotent (RingHom.ker ↑g))
:
AlgHom.comp g (Algebra.FormallySmooth.liftOfSurjective f g hg hg') = f
theorem
Algebra.FormallySmooth.of_equiv
{R : Type u}
[CommSemiring R]
{A : Type u}
{B : Type u}
[Semiring A]
[Algebra R A]
[Semiring B]
[Algebra R B]
[Algebra.FormallySmooth R A]
(e : A ≃ₐ[R] B)
:
theorem
Algebra.FormallyUnramified.of_equiv
{R : Type u}
[CommSemiring R]
{A : Type u}
{B : Type u}
[Semiring A]
[Algebra R A]
[Semiring B]
[Algebra R B]
[Algebra.FormallyUnramified R A]
(e : A ≃ₐ[R] B)
:
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)
:
instance
Algebra.FormallySmooth.mvPolynomial
(R : Type u)
[CommSemiring R]
(σ : Type u)
:
Algebra.FormallySmooth R (MvPolynomial σ R)
Equations
- (_ : Algebra.FormallySmooth R (MvPolynomial σ R)) = (_ : Algebra.FormallySmooth R (MvPolynomial σ R))
Equations
- (_ : Algebra.FormallySmooth R (Polynomial R)) = (_ : Algebra.FormallySmooth R (Polynomial R))
theorem
Algebra.FormallySmooth.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.FormallySmooth R A]
[Algebra.FormallySmooth A B]
:
theorem
Algebra.FormallyUnramified.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.FormallyUnramified R A]
[Algebra.FormallyUnramified A B]
:
theorem
Algebra.FormallyUnramified.of_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.FormallyUnramified 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]
:
theorem
Algebra.FormallySmooth.of_split
{R : Type u}
[CommRing R]
{P : Type u}
{A : Type u}
[CommRing A]
[Algebra R A]
[CommRing P]
[Algebra R P]
(f : P →ₐ[R] A)
[Algebra.FormallySmooth R P]
(g : A →ₐ[R] P ⧸ RingHom.ker ↑f ^ 2)
(hg : AlgHom.comp (AlgHom.kerSquareLift f) g = AlgHom.id R A)
:
theorem
Algebra.FormallySmooth.iff_split_surjection
{R : Type u}
[CommRing R]
{P : Type u}
{A : Type u}
[CommRing A]
[Algebra R A]
[CommRing P]
[Algebra R P]
(f : P →ₐ[R] A)
(hf : Function.Surjective ⇑f)
[Algebra.FormallySmooth R P]
:
Algebra.FormallySmooth R A ↔ ∃ (g : A →ₐ[R] P ⧸ RingHom.ker ↑f ^ 2), AlgHom.comp (AlgHom.kerSquareLift f) g = AlgHom.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.
instance
Algebra.FormallyUnramified.subsingleton_kaehlerDifferential
{R : Type u}
{S : Type u}
[CommRing R]
[CommRing S]
[Algebra R S]
[Algebra.FormallyUnramified R S]
:
Subsingleton (Ω[S⁄R])
Equations
- (_ : Subsingleton (Ω[S⁄R])) = (_ : Subsingleton (Ω[S⁄R]))
theorem
Algebra.FormallyUnramified.iff_subsingleton_kaehlerDifferential
{R : Type u}
{S : Type u}
[CommRing R]
[CommRing S]
[Algebra R S]
:
Algebra.FormallyUnramified R S ↔ Subsingleton (Ω[S⁄R])
instance
Algebra.FormallyUnramified.base_change
{R : Type u}
[CommSemiring R]
{A : Type u}
[Semiring A]
[Algebra R A]
(B : Type u)
[CommSemiring B]
[Algebra R B]
[Algebra.FormallyUnramified R A]
:
Algebra.FormallyUnramified B (TensorProduct R B A)
Equations
- (_ : Algebra.FormallyUnramified B (TensorProduct R B A)) = (_ : Algebra.FormallyUnramified B (TensorProduct R B A))
instance
Algebra.FormallySmooth.base_change
{R : Type u}
[CommSemiring R]
{A : Type u}
[Semiring A]
[Algebra R A]
(B : Type u)
[CommSemiring B]
[Algebra R B]
[Algebra.FormallySmooth R A]
:
Algebra.FormallySmooth B (TensorProduct R B A)
Equations
- (_ : Algebra.FormallySmooth B (TensorProduct R B A)) = (_ : Algebra.FormallySmooth B (TensorProduct R B A))
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
- (_ : Algebra.FormallyEtale B (TensorProduct R B A)) = (_ : Algebra.FormallyEtale B (TensorProduct R B A))
theorem
Algebra.FormallySmooth.of_isLocalization
{R : Type u}
{Rₘ : Type u}
[CommRing R]
[CommRing Rₘ]
(M : Submonoid R)
[Algebra R Rₘ]
[IsLocalization M Rₘ]
:
theorem
Algebra.FormallyUnramified.of_isLocalization
{R : Type u}
{Rₘ : Type u}
[CommRing R]
[CommRing Rₘ]
(M : Submonoid R)
[Algebra R Rₘ]
[IsLocalization M Rₘ]
:
This holds in general for epimorphisms.
theorem
Algebra.FormallyEtale.of_isLocalization
{R : Type u}
{Rₘ : Type u}
[CommRing R]
[CommRing Rₘ]
(M : Submonoid R)
[Algebra R Rₘ]
[IsLocalization M Rₘ]
:
theorem
Algebra.FormallySmooth.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.FormallySmooth R Sₘ]
:
Algebra.FormallySmooth Rₘ Sₘ
theorem
Algebra.FormallyUnramified.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ₘ]
[Algebra.FormallyUnramified 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 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.FormallySmooth.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.FormallySmooth R S]
:
Algebra.FormallySmooth Rₘ Sₘ
theorem
Algebra.FormallyUnramified.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 (Submonoid.map (algebraMap R S) M) Sₘ]
[Algebra.FormallyUnramified 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ₘ