English
If e is a Lie-module equivalence, then the image of posFittingComp under e equals posFittingComp in the target.
Русский
Если e — эквивалент модуля Ли, то образ posFittingComp под e равен posFittingComp у целевого модуля.
LaTeX
$$$\operatorname{map} e(\operatorname{posFittingComp}(R,L,M)) = \operatorname{posFittingComp}(R,L,M_2)$$$
Lean4
theorem posFittingComp_map_incl_sup_of_codisjoint [IsNoetherian R M] [IsArtinian R M] {N₁ N₂ : LieSubmodule R L M}
(h : Codisjoint N₁ N₂) :
(posFittingComp R L N₁).map N₁.incl ⊔ (posFittingComp R L N₂).map N₂.incl = posFittingComp R L M :=
by
obtain ⟨l, hl⟩ :=
Filter.eventually_atTop.mp <|
(eventually_iInf_lowerCentralSeries_eq R L N₁).and <|
(eventually_iInf_lowerCentralSeries_eq R L N₂).and (eventually_iInf_lowerCentralSeries_eq R L M)
obtain ⟨hl₁, hl₂, hl₃⟩ := hl l (le_refl _)
simp_rw [← iInf_lowerCentralSeries_eq_posFittingComp, hl₁, hl₂, hl₃, LieSubmodule.lowerCentralSeries_map_eq_lcs, ←
LieSubmodule.lcs_sup, lowerCentralSeries, h.eq_top]
