English
For formally smooth extensions P and Q of S over R, there is a linear equivalence between P.H1Cotangent and Q.H1Cotangent as S-modules, compatible with the canonical maps and the extension structure.
Русский
Для формально гладких расширений P и Q над S над R существует линейное эквивалентное отображение между P.H1Cotangent и Q.H1Cotangent как модули над S, совместимое с каноническими отображениями и структурой расширения.
LaTeX
$$$P.H1Cotangent \\simeq_S Q.H1Cotangent$$$
Lean4
/-- Given a formally smooth `R`-algebra `P` and a surjective algebra homomorphism `f : P →ₐ[R] S`
with kernel `I` (typically a presentation `R[X] → S`),
then `S` is formally smooth iff `I/I² → S ⊗[P] Ω[P⁄R]` is injective and `Ω[S/R]` is projective.
-/
theorem iff_injective_and_projective :
Algebra.FormallySmooth R S ↔ Function.Injective (kerCotangentToTensor R P S) ∧ Module.Projective S Ω[S⁄R] :=
by
rw [Algebra.FormallySmooth.iff_injective_and_split hf, ← Module.Projective.iff_split_of_projective]
exact KaehlerDifferential.mapBaseChange_surjective _ _ _ hf
