English
If S → T is a formally étale algebra over a base ring R, then the canonical base-change map for Kahler differentials induces a linear isomorphism T ⊗_S Ω_{S/R} ≅ Ω_{T/R}. This expresses that Kahler differentials behave well under étale (indeed, formally étale) base change.
Русский
Пусть S → T является формально этиальным алгеброй над основанием R. Тогда каноническое отображение при базовом изменении вызывает изо-л′иную для дифференциалов Каэлера: T ⊗_S Ω_{S/R} ≅ Ω_{T/R}. Это утверждение о том, что дифференциалы Каэльера сохраняются при эталe базовом изменении.
LaTeX
$$$T \\otimes_S \\Omega_{S/R} \\;\\cong_\\text{linear}_T \\; \\Omega_{T/R}.$$$
Lean4
/-- The canonical isomorphism `T ⊗[S] Ω[S⁄R] ≃ₗ[T] Ω[T⁄R]` for `T` a formally étale `S`-algebra.
Also see `S ⊗[R] Ω[A⁄R] ≃ₗ[S] Ω[S ⊗[R] A⁄S]` at `KaehlerDifferential.tensorKaehlerEquiv`.
-/
@[simps! apply]
noncomputable def tensorKaehlerEquivOfFormallyEtale [Algebra.FormallyEtale S T] : T ⊗[S] Ω[S⁄R] ≃ₗ[T] Ω[T⁄R] :=
by
refine
LinearEquiv.ofBijective (mapBaseChange R S T)
⟨?_, fun x ↦ (KaehlerDifferential.exact_mapBaseChange_map R S T x).mp (Subsingleton.elim _ _)⟩
rw [injective_iff_map_eq_zero]
intro x hx
obtain ⟨x, rfl⟩ := (Algebra.H1Cotangent.exact_δ_mapBaseChange R S T x).mp hx
rw [Subsingleton.elim x 0, map_zero]
