basisCotangent_apply — Mathlib

English

The value of the basis element corresponding to r is equal to the corresponding cotangent element of the relation r.

Русский

Значение элемента базы, соответствующего r, равно соответствующему элементу касательной для отношения r.

LaTeX

$$P.basisCotangent r = Extension.Cotangent.mk ⟨P.relation r, P.relation_mem_ker r⟩$$

Lean4

theorem basisCotangent_apply (r : σ) :
    P.basisCotangent r = Extension.Cotangent.mk ⟨P.relation r, P.relation_mem_ker r⟩ :=
  by
  symm
  apply P.cotangentEquiv.injective
  ext
  simp_rw [basisCotangent, Basis.map_apply, LinearEquiv.apply_symm_apply, basisDeriv_apply]
  apply P.toPreSubmersivePresentation.cotangentComplexAux_apply _ _

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