coroot_coweightMap_apply — Mathlib

English

For a morphism f: P → Q, the coroot coweight maps satisfy f.coweightMap (Q.coroot i) = P.coroot (f.indexEquiv.symm i).

Русский

Для гомоморфизма f: P → Q выполняется coweightMap(f)(Q.coroot i) = P.coroot(f.indexEquiv.symm i).

LaTeX

$$$f.coweightMap\\bigl(Q.coroot i\\bigr)=P.coroot\\bigl(f.indexEquiv^{-1} i\\bigr)$$$

Lean4

theorem coroot_coweightMap_apply {ι₂ M₂ N₂ : Type*} [AddCommGroup M₂] [Module R M₂] [AddCommGroup N₂] [Module R N₂]
    (P : RootPairing ι R M N) (Q : RootPairing ι₂ R M₂ N₂) (i : ι₂) (f : Hom P Q) :
    f.coweightMap (Q.coroot i) = P.coroot (f.indexEquiv.symm i) :=
  Eq.mp (propext funext_iff) f.coroot_coweightMap i

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