English
For any Lie module hom f : M → M2, the image of posFittingComp(R,L,M) under f is contained in posFittingComp(R,L,M2).
Русский
Для всякого гомоморфизма модуля Ли f: M → M2 образ posFittingComp(R,L,M) содержится в posFittingComp(R,L,M2).
LaTeX
$$$\operatorname{Im}(f|_{\operatorname{posFittingComp}(R,L,M)}) \leq \operatorname{posFittingComp}(R,L,M2)$$$
Lean4
theorem map_posFittingComp_le : (posFittingComp R L M).map f ≤ posFittingComp R L M₂ :=
by
rw [posFittingComp, posFittingComp, LieSubmodule.map_iSup]
refine iSup_mono fun y ↦ LieSubmodule.map_le_iff_le_comap.mpr fun m hm ↦ ?_
simp only [mem_posFittingCompOf] at hm
simp only [LieSubmodule.mem_comap, mem_posFittingCompOf]
intro k
obtain ⟨n, hn⟩ := hm k
use f n
rw [LieModule.toEnd_pow_apply_map, hn]
