English
Composition of root-pairing morphisms is associative: (h ∘ g) ∘ f = h ∘ (g ∘ f).
Русский
Сочетание морфизмов между парой корней ассоциативно: (h ∘ g) ∘ f = h ∘ (g ∘ f).
LaTeX
$$$(h\\circ g)\\circ f = h\\circ (g\\circ f)$$$
Lean4
/-- Composition of morphisms -/
@[simps!]
def comp {ι₁ 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₂] {P : RootPairing ι R M N} {P₁ : RootPairing ι₁ R M₁ N₁}
{P₂ : RootPairing ι₂ R M₂ N₂} (g : Hom P₁ P₂) (f : Hom P P₁) : Hom P P₂
where
weightMap := g.weightMap ∘ₗ f.weightMap
coweightMap := f.coweightMap ∘ₗ g.coweightMap
indexEquiv := f.indexEquiv.trans g.indexEquiv
weight_coweight_transpose := by
ext φ x
rw [← LinearMap.dualMap_comp_dualMap, ← LinearMap.comp_assoc _ f.coweightMap, ← f.weight_coweight_transpose,
LinearMap.comp_assoc g.coweightMap, ← g.weight_coweight_transpose, ← LinearMap.comp_assoc]
root_weightMap := by
ext i
simp only [LinearMap.coe_comp, Equiv.coe_trans]
rw [comp_assoc, f.root_weightMap, ← comp_assoc, g.root_weightMap, comp_assoc]
coroot_coweightMap := by
ext i
simp only [LinearMap.coe_comp]
rw [comp_assoc, g.coroot_coweightMap, ← comp_assoc, f.coroot_coweightMap, comp_assoc]
simp
