compEquiv_symm_inr — Mathlib

English

The left projection of compEquiv_symm_inr coincides with the inr-map composed with the cotangent basis; i.e., fst of the symm-inr map equals the inr-inclusion after applying the base-change map.

Русский

Левый проецирующий компонент compEquiv_symm_inr совпадает с отображением inr после применения базового изменения и взятия котантного базиса.

LaTeX

$$$$ \\text{fst}( (compEquiv(Q,P))^{-1} \circ \\mathrm{inr}_T(Q.toExtension.CotangentSpace, T \\otimes_S P.toExtension.CotangentSpace) ) = \\mathrm{Extension.CotangentSpace.map}(Q.toComp P).toExtensionHom . $$$$

Lean4

theorem compEquiv_symm_inr :
    (compEquiv Q P).symm.toLinearMap ∘ₗ
        LinearMap.inr T Q.toExtension.CotangentSpace (T ⊗[S] P.toExtension.CotangentSpace) =
      (Extension.CotangentSpace.map (Q.toComp P).toExtensionHom).liftBaseChange T :=
  by
  classical
  apply (P.cotangentSpaceBasis.baseChange T).ext
  intro i
  apply (Q.comp P).cotangentSpaceBasis.repr.injective
  ext j
  simp only [compEquiv, LinearEquiv.trans_symm, LinearEquiv.symm_symm, Basis.baseChange_apply, LinearMap.coe_comp,
    LinearEquiv.coe_coe, LinearMap.coe_inr, Function.comp_apply, LinearEquiv.trans_apply, Basis.repr_symm_apply,
    pderiv_X, toComp_val, Basis.repr_linearCombination, LinearMap.liftBaseChange_tmul, one_smul, repr_CotangentSpaceMap]
  obtain (j | j) := j <;>
    simp only [Basis.prod_repr_inr, Basis.baseChange_repr_tmul, Basis.repr_self, Basis.prod_repr_inl, map_zero,
      Finsupp.coe_zero, Pi.zero_apply, ne_eq, not_false_eq_true, Pi.single_eq_of_ne, Pi.single_apply,
      Finsupp.single_apply, ite_smul, one_smul, zero_smul, Sum.inr.injEq, MonoidWithZeroHom.map_ite_one_zero,
      reduceCtorEq]

Похожие утверждения