English
The cotangent complex of a pre-submersive presentation can be expressed as a composition of Finsupp maps, yielding a linear map from the cotangent to finite index functions on σ.
Русский
Комплекс котантов для пред-подмёрсивного представления задаётся как композиция отображений Finsupp, что даёт линейное отображение котантанта к конечному индексу функциям на σ.
LaTeX
$${R,S,ι,σ} → [Finite σ] (P : Algebra.PreSubmersivePresentation R S ι σ) → LinearMap (RingHom.id S) P.toExtension.Cotangent (σ → S)$$
Lean4
/-- Given a pre-submersive presentation, this is the composition
`I ⧸ I ^ 2 → ⊕ S dxᵢ → ⊕ S dxᵢ` where the second direct sum runs over
all `i : σ` induced by the injection `P.map : σ → ι`.
If `P` is submersive, this is an isomorphism. See `SubmersivePresentation.cotangentEquiv`.
-/
noncomputable def cotangentComplexAux [Finite σ] (P : PreSubmersivePresentation R S ι σ) :
P.toExtension.Cotangent →ₗ[S] σ → S :=
Finsupp.linearEquivFunOnFinite S S σ ∘ₗ
Finsupp.lcomapDomain _ P.map_inj ∘ₗ P.cotangentSpaceBasis.repr.toLinearMap ∘ₗ P.toExtension.cotangentComplex
