English
If f is an ideal morphism, then map f (comap f J) = idealRange(f) ∩ J for any LieIdeal J of L'.
Русский
Пусть f — гомоморфизм идеалов. Тогда map f (comap f J) = range(f) ∩ J для любого LieIdeal J в L'.
LaTeX
$$$f.IsIdealMorphism \Rightarrow \operatorname{map} f (\operatorname{comap} f J) = f.idealRange \cap J$$$
Lean4
@[simp]
theorem map_comap_eq (h : f.IsIdealMorphism) : map f (comap f J) = f.idealRange ⊓ J :=
by
apply le_antisymm
· rw [le_inf_iff]; exact ⟨f.map_le_idealRange _, map_comap_le⟩
· rw [f.isIdealMorphism_def] at h
rw [← SetLike.coe_subset_coe, LieSubmodule.coe_inf, ← coe_toLieSubalgebra, h]
rintro y ⟨⟨x, h₁⟩, h₂⟩; rw [← h₁] at h₂ ⊢; exact mem_map h₂
