English
If f is injective, then comap f of genWeightSpace M2 χ equals genWeightSpace M χ.
Русский
Если f инъективен, то предобразная подмодуля genWeightSpace(M2, χ) по f равна genWeightSpace(M, χ).
LaTeX
$$$\text{inj}(f) \Rightarrow (\operatorname{comap} f (\operatorname{genWeightSpace}(M2,χ)) = \operatorname{genWeightSpace}(M,χ))$$$
Lean4
theorem comap_genWeightSpace_eq_of_injective (hf : Injective f) : (genWeightSpace M₂ χ).comap f = genWeightSpace M χ :=
by
refine le_antisymm (fun m hm ↦ ?_) ?_
· simp only [LieSubmodule.mem_comap, mem_genWeightSpace] at hm
simp only [mem_genWeightSpace]
intro x
have h : (toEnd R L M₂ x - χ x • ↑1) ∘ₗ f = f ∘ₗ (toEnd R L M x - χ x • ↑1) := by ext; simp
obtain ⟨k, hk⟩ := hm x
use k
suffices f (((toEnd R L M x - χ x • ↑1) ^ k) m) = 0 by rw [← f.map_zero] at this; exact hf this
simpa [hk] using (LinearMap.congr_fun (Module.End.commute_pow_left_of_commute h k) m).symm
· rw [← LieSubmodule.map_le_iff_le_comap]
exact map_genWeightSpace_le f
