English
For x in the composed cotangent space, the first component of compEquiv(Q,P) applied to x equals Extension.CotangentSpace.map (Q.ofComp P).toExtensionHom applied to x.
Русский
Для x в композиции котант пространства, первая компонента compEquiv(Q,P) примененная к x равна применению Extension.CotangentSpace.map (Q.ofComp P).toExtensionHom к x.
LaTeX
$$$$ (compEquiv(Q,P)\; x).fst = \mathrm{Extension.CotangentSpace.map}(Q.ofComp P).toExtensionHom(x). $$$$
Lean4
theorem fst_compEquiv :
LinearMap.fst T Q.toExtension.CotangentSpace (T ⊗[S] P.toExtension.CotangentSpace) ∘ₗ (compEquiv Q P).toLinearMap =
Extension.CotangentSpace.map (Q.ofComp P).toExtensionHom :=
by
classical
apply (Q.comp P).cotangentSpaceBasis.ext
intro i
apply Q.cotangentSpaceBasis.repr.injective
ext j
simp only [compEquiv, LinearMap.coe_comp, LinearEquiv.coe_coe, Function.comp_apply, ofComp_val,
LinearEquiv.trans_apply, Basis.repr_self, LinearMap.fst_apply, repr_CotangentSpaceMap]
obtain (i | i) := i <;>
simp only [Basis.repr_symm_apply, Finsupp.linearCombination_single, Basis.prod_apply, LinearMap.coe_inl,
LinearMap.coe_inr, Sum.elim_inl, Function.comp_apply, one_smul, Basis.repr_self, Finsupp.single_apply, pderiv_X,
Pi.single_apply, Sum.elim_inr, Function.comp_apply, Basis.baseChange_apply, one_smul,
MonoidWithZeroHom.map_ite_one_zero, map_zero, Finsupp.coe_zero, Pi.zero_apply, derivation_C]
