Kähler differentials along a formally étale extension

For a tower R → S → T with T formally étale over S, Mathlib's KaehlerDifferential.tensorKaehlerEquivOfFormallyEtale identifies T ⊗[S] Ω[S⁄R] with Ω[T⁄R]. This file records what that says about bases, and proves a converse.

An S-basis of Ω[S⁄R] becomes a T-basis of Ω[T⁄R] on the same index type, each basis vector going to its image under KaehlerDifferential.map. The motivating application is a tower of fields k → K → F with F/K separable algebraic, so that Algebra.FormallyEtale.of_isSeparable supplies the hypothesis: the differentials of F over k are then computed by those of K over k.

Conversely, if T is formally smooth over R and T ⊗[S] Ω[S⁄R] → Ω[T⁄R] is bijective, then T is formally étale over S. By the Jacobi–Zariski sequence

H¹(L_{T/R}) → H¹(L_{T/S}) → T ⊗[S] Ω[S⁄R] → Ω[T⁄R] → Ω[T⁄S] → 0,

Ω[T⁄S] vanishes when the middle map is surjective, and H¹(L_{T/S}) vanishes when it is injective, since H¹(L_{T/R}) = 0 by formal smoothness. The typical use is with S a polynomial ring over R: if the differentials d aᵢ of elements aᵢ of a formally smooth R-algebra T form a basis of Ω[T⁄R], then T is formally étale over R[Xᵢ] via Xᵢ ↦ aᵢ.

Main declarations

• TauCeti.kaehlerBasisOfFormallyEtale: the induced basis of Ω[T⁄R];
• TauCeti.formallyEtale_of_bijective_mapBaseChange and TauCeti.formallyEtale_iff_bijective_mapBaseChange: formal étaleness of T over S when T is formally smooth over R;
• TauCeti.bijective_mapBaseChange_of_basis: T ⊗[S] Ω[S⁄R] → Ω[T⁄R] is bijective when it carries a basis to a basis.

References

• The Stacks Project, Tag 00S2, for the Jacobi–Zariski sequence.

noncomputable def TauCeti.kaehlerBasisOfFormallyEtale (R : Type u_1) (S : Type u_2) (T : Type u_3) [CommRing R] [CommRing S] [CommRing T] [Algebra R S] [Algebra R T] [Algebra S T] [IsScalarTower R S T] [Algebra.FormallyEtale S T] {ι : Type u_4} (b : Module.Basis ι S Ω[S⁄R]) : Module.Basis ι T Ω[T⁄R]

The T-basis of Ω[T⁄R] induced by an S-basis of Ω[S⁄R], when T is formally étale over S. Its vectors are the images of the given ones under KaehlerDifferential.map, as recorded in TauCeti.kaehlerBasisOfFormallyEtale_apply.

Equations

• TauCeti.kaehlerBasisOfFormallyEtale R S T b = (Module.Basis.baseChange T b).map (KaehlerDifferential.tensorKaehlerEquivOfFormallyEtale R S T)

@[simp]

theorem TauCeti.kaehlerBasisOfFormallyEtale_apply (R : Type u_1) (S : Type u_2) (T : Type u_3) [CommRing R] [CommRing S] [CommRing T] [Algebra R S] [Algebra R T] [Algebra S T] [IsScalarTower R S T] [Algebra.FormallyEtale S T] {ι : Type u_4} (b : Module.Basis ι S Ω[S⁄R]) (i : ι) : (kaehlerBasisOfFormallyEtale R S T b) i = (KaehlerDifferential.map R R S T) (b i)

theorem TauCeti.formallyEtale_of_bijective_mapBaseChange {R : Type u_1} {S : Type u_2} {T : Type u_3} [CommRing R] [CommRing S] [CommRing T] [Algebra R S] [Algebra R T] [Algebra S T] [IsScalarTower R S T] [Algebra.FormallySmooth R T] (h : Function.Bijective ⇑(KaehlerDifferential.mapBaseChange R S T)) : Algebra.FormallyEtale S T

If T is formally smooth over R and T ⊗[S] Ω[S⁄R] → Ω[T⁄R] is bijective, then T is formally étale over S.

theorem TauCeti.formallyEtale_iff_bijective_mapBaseChange {R : Type u_1} {S : Type u_2} {T : Type u_3} [CommRing R] [CommRing S] [CommRing T] [Algebra R S] [Algebra R T] [Algebra S T] [IsScalarTower R S T] [Algebra.FormallySmooth R T] : Algebra.FormallyEtale S T ↔ Function.Bijective ⇑(KaehlerDifferential.mapBaseChange R S T)

For T formally smooth over R, T is formally étale over S exactly when T ⊗[S] Ω[S⁄R] → Ω[T⁄R] is bijective.

theorem TauCeti.bijective_mapBaseChange_of_basis {R : Type u_1} {S : Type u_2} {T : Type u_3} [CommRing R] [CommRing S] [CommRing T] [Algebra R S] [Algebra R T] [Algebra S T] [IsScalarTower R S T] {ι : Type u_4} (bS : Module.Basis ι S Ω[S⁄R]) (bT : Module.Basis ι T Ω[T⁄R]) (h : ∀ (i : ι), (KaehlerDifferential.map R R S T) (bS i) = bT i) : Function.Bijective ⇑(KaehlerDifferential.mapBaseChange R S T)

The map T ⊗[S] Ω[S⁄R] → Ω[T⁄R] is bijective when it carries the base change of a basis of Ω[S⁄R] to a basis of Ω[T⁄R].