English
The simp lemma expresses that the algebraMap algebra respects the section evaluation: sectionOfRetractionKerToTensor_algebraMap x equals x minus the derivation term.
Русский
Лемма упрощения показывает, что algebraMap сохраняет секцию: sectionOfRetractionKerToTensor_algebraMap x = x − л (1 ⊗ D x).
LaTeX
$$theorem sectionOfRetractionKerToTensor_algebraMap (x : P) : sectionOfRetractionKerToTensor l hl hf' hf (algebraMap P S x) = x - l (1 ⊗ₜ .D _ _ x)$$
Lean4
/-- Given a surjective algebra homomorphism `f : P →ₐ[R] S` with square-zero kernel `I`.
Suppose we have a retraction `l` of the injection `I →ₗ[P] S ⊗[P] Ω[P/R]`, then
`x ↦ σ x - l (1 ⊗ D (σ x))` is an algebra homomorphism and a section to `f`,
where `σ` is an arbitrary (set-theoretic) section of `f`
-/
noncomputable def sectionOfRetractionKerToTensor : S →ₐ[R] P :=
sectionOfRetractionKerToTensorAux l hl _ (fun x ↦ (hf x).choose_spec) hf'
