sectionCotangent_eq_iff — Mathlib

English

A section equality holds if and only if the coordinate equalities hold with respect to the cotangent basis and the cotangent map.

Русский

Уравнение секции выполняется тогда и только тогда, когда координатные равенства выполняются относительно базиса касательной и отображения касательной.

LaTeX

$$sectionCotangent x = y iff ∀ i, P.cotangentSpaceBasis.repr x (P.map i) = (P.cotangentComplexAux y) i$$

Lean4

theorem sectionCotangent_eq_iff [Finite σ] (x : P.toExtension.CotangentSpace) (y : P.toExtension.Cotangent) :
    sectionCotangent P x = y ↔ ∀ i : σ, P.cotangentSpaceBasis.repr x (P.map i) = (P.cotangentComplexAux y) i :=
  by
  simp only [sectionCotangent, LinearMap.coe_comp, LinearEquiv.coe_coe, Function.comp_apply]
  rw [← (cotangentEquiv P).injective.eq_iff, funext_iff, LinearEquiv.apply_symm_apply]
  simp

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