δ_comp_equiv — Mathlib

English

The connecting morphism δ commutes with the equivalence between H1Cotangent spaces induced by reindexing generators, i.e., composing δ with the equivalence gives the same result as δ on the primed data.

Русский

Соединяющее отображение δ commute с эквивалентностью между пространствами H1Cotangent, полученной перестановкой генераторов; эквивалентность сохраняет δ.

LaTeX

$$$\\delta_{Q,P} \\circ (\\mathrm{equiv}_{Q'Q})^{\\!\\,\\!\\!\\,\\mathrm{toLinearMap}} = \\delta_{Q',P'}.$$$

Lean4

theorem δ_comp_equiv : δ Q P ∘ₗ (H1Cotangent.equiv _ _).toLinearMap = δ Q' P' :=
  by
  ext x
  exact δ_map Q P Q' P' _ _

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