English
The construction sectionOfRetractionKerToTensorAux provides a section S → P with the property that composing with kerToTensor yields identity and interacts with σ, hσ consistently.
Русский
Конструкция sectionOfRetractionKerToTensorAux задаёт секцию S → P, такая что композиция с kerToTensor даёт тождество и согласуется с σ, hσ.
LaTeX
$$sectionOfRetractionKerToTensorAux : S →ₐ[R] P with properties$$
Lean4
/-- Given a surjective algebra hom `f : P →ₐ[R] S` with square-zero kernel `I`,
and a section `g : S →ₐ[R] P` (as algebra homs),
we get a retraction of the injection `I → S ⊗[P] Ω[P/R]`.
-/
noncomputable def retractionOfSectionOfKerSqZero : S ⊗[P] Ω[P⁄R] →ₗ[P] RingHom.ker (algebraMap P S) :=
letI := g.toRingHom.toAlgebra
haveI := isScalarTower_of_section_of_ker_sqZero g hf' hg
letI f : _ →ₗ[P] RingHom.ker (algebraMap P S) :=
(derivationOfSectionOfKerSqZero (IsScalarTower.toAlgHom R P S) hf' g hg).liftKaehlerDifferential
(f.liftBaseChange S).restrictScalars P
