English
There is a linear section from the cotangent space back into the cotangent module, given by projecting to σ-summands and composing with the inverse of the cotangent equivalence.
Русский
Существует линейная секция из касательного пространства обратно в модуль касательной, заданная проецированием на сомножители σ и композицией с обратной связью касательности.
LaTeX
$$sectionCotangent : P.toExtension.CotangentSpace →ₗ[S] P.toExtension.Cotangent$$
Lean4
/-- If `P` is a submersive presentation, this is the section of the map
`I ⧸ I ^ 2 → ⊕ S dxᵢ` given by projecting to the summands indexed by `σ` and composing with the
inverse of `P.cotangentEquiv`.
By `SubmersivePresentation.sectionCotangent_comp` this is indeed a section.
-/
noncomputable def sectionCotangent : P.toExtension.CotangentSpace →ₗ[S] P.toExtension.Cotangent :=
(cotangentEquiv P).symm ∘ₗ
(Finsupp.linearEquivFunOnFinite S S σ).toLinearMap ∘ₗ
Finsupp.lcomapDomain _ P.map_inj ∘ₗ P.cotangentSpaceBasis.repr.toLinearMap
