root_weightMap_apply — Mathlib

English

For a morphism f: P → Q between root pairings, the weight map sends the root P.root i to the root Q.root (f.indexEquiv i).

Русский

Для гомоморфизма f: P → Q между парными корнями весовой отображает корень P.root i в корень Q.root (f.indexEquiv i).

LaTeX

$$$f.weightMap\\bigl(P.root\\,i\\bigr)=Q.root\\bigl(f.indexEquiv\\,i\\bigr)$$

Lean4

theorem root_weightMap_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.weightMap (P.root i) = Q.root (f.indexEquiv i) :=
  Eq.mp (propext funext_iff) f.root_weightMap i

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