English
For morphisms f:P→Q, the weight and coweight maps intertwine with the index equivalence; specifically, weight and coweight maps respect the induced permutation on roots and coroots.
Русский
Для морфизмов f:P→Q веса и противвеса совместимы с индексным эквивалентом; отображения весов и противвесов сохраняют полученную перестановку корней и кор-весов.
LaTeX
$$f.weightMap ∘ P.root i = Q.root (f.indexEquiv i) и f.coweightMap ∘ Q.coroot i = P.coroot (f.indexEquiv.symm i)$$
Lean4
@[simp]
theorem comp_assoc {ι₁ M₁ N₁ ι₂ M₂ N₂ ι₃ M₃ N₃ : Type*} [AddCommGroup M₁] [Module R M₁] [AddCommGroup N₁] [Module R N₁]
[AddCommGroup M₂] [Module R M₂] [AddCommGroup N₂] [Module R N₂] [AddCommGroup M₃] [Module R M₃] [AddCommGroup N₃]
[Module R N₃] {P : RootPairing ι R M N} {P₁ : RootPairing ι₁ R M₁ N₁} {P₂ : RootPairing ι₂ R M₂ N₂}
{P₃ : RootPairing ι₃ R M₃ N₃} (h : Hom P₂ P₃) (g : Hom P₁ P₂) (f : Hom P P₁) :
comp (comp h g) f = comp h (comp g f) := by ext <;> simp
