English
For a Lie module hom f, the image of genWeightSpace M χ lies inside genWeightSpace M2 χ for the same χ.
Русский
Образ пространства весов genWeightSpace(M, χ) при гомоморфизме f лежит внутри genWeightSpace(M2, χ).
LaTeX
$$$\operatorname{Im}(\operatorname{genWeightSpace}(M,χ) \xrightarrow{f} M2) \subseteq \operatorname{genWeightSpace}(M2,χ)$$$
Lean4
theorem map_genWeightSpace_le : (genWeightSpace M χ).map f ≤ genWeightSpace M₂ χ :=
by
rw [LieSubmodule.map_le_iff_le_comap]
intro m hm
simp only [LieSubmodule.mem_comap, mem_genWeightSpace]
intro x
have : (toEnd R L M₂ x - χ x • ↑1) ∘ₗ f = f ∘ₗ (toEnd R L M x - χ x • ↑1) := by ext; simp
obtain ⟨k, h⟩ := (mem_genWeightSpace _ _ _).mp hm x
refine ⟨k, ?_⟩
simpa [h] using LinearMap.congr_fun (Module.End.commute_pow_left_of_commute this k) m
