English
For an injective LieModuleHom f, the image of genWeightSpace M χ under f equals the genWeightSpace of M2 χ restricted to the range of f.
Русский
Для инъективного гомоморфизма Ли-модуля f образ genWeightSpace(M, χ) равен genWeightSpace(M2, χ) пересечение с образом f.
LaTeX
$$$\operatorname{map} f (\operatorname{genWeightSpace}(M,χ)) = \operatorname{genWeightSpace}(M2,χ) \cap \operatorname{range}(f)$$$
Lean4
theorem map_posFittingComp_eq (e : M ≃ₗ⁅R,L⁆ M₂) : (posFittingComp R L M).map e = posFittingComp R L M₂ :=
by
refine le_antisymm (map_posFittingComp_le _) ?_
suffices posFittingComp R L M₂ = ((posFittingComp R L M₂).map (e.symm : M₂ →ₗ⁅R,L⁆ M)).map e
by
rw [this]
exact LieSubmodule.map_mono (map_posFittingComp_le _)
rw [← LieSubmodule.map_comp]
convert LieSubmodule.map_id
ext
simp
