English
There is a linear equivalence between the cotangent module and the function space σ → S, given by mapping basis elements to derivatives of relations.
Русский
Существует линейное эквивалентное отображение между касательным модулем и пространством функций σ → S, задаваемое отправлением базисных элементов к частным производным отношений.
LaTeX
$$cotangentEquiv : P.toExtension.Cotangent ≃ₗ[S] σ → S$$
Lean4
/-- Given a submersive presentation of `S` as `R`-algebra, any indexing type `κ` complementary to
the `σ` in `ι` indexes a basis of `Ω[S⁄R]`.
See `SubmersivePresentation.basisKaehler` for the special case `κ = (Set.range P.map)ᶜ`.
-/
noncomputable def basisKaehlerOfIsCompl {κ : Type*} {f : κ → ι} (hf : Function.Injective f)
(hcompl : IsCompl (Set.range f) (Set.range P.map)) : Basis κ S Ω[S⁄R] :=
by
apply
P.cotangentSpaceBasis.ofSplitExact (sectionCotangent_comp P) Extension.exact_cotangentComplex_toKaehler
Extension.toKaehler_surjective hf (b := P.map)
· intro i
apply sectionCotangent_zero_of_notMem_range _ _
simp [← hcompl.compl_eq]
· simp only [sectionCotangent, LinearMap.coe_comp, Function.comp_assoc, LinearEquiv.coe_coe]
apply LinearIndependent.map' _ _ P.cotangentEquiv.symm.ker
convert (Pi.basisFun S σ).linearIndependent
classical
ext i j
simp only [Function.comp_apply, Basis.repr_self, Finsupp.linearEquivFunOnFinite_apply, Pi.basisFun_apply]
simp [Finsupp.single_eq_pi_single]
· exact hcompl.2
