map_genWeightSpace_eq_of_injective

English

If f is injective, then the image of genWeightSpace M χ is the intersection of genWeightSpace M2 χ with the range of f.

Русский

Если f инъективен, образ genWeightSpace(M, χ) равен genWeightSpace(M2, χ) ∩ range(f).

LaTeX

$$$\operatorname{map} f (\operatorname{genWeightSpace}(M,χ)) = \operatorname{genWeightSpace}(M2,χ) \cap \operatorname{range}(f)$$$

Lean4

theorem map_genWeightSpace_eq_of_injective (hf : Injective f) :
    (genWeightSpace M χ).map f = genWeightSpace M₂ χ ⊓ f.range :=
  by
  refine le_antisymm (le_inf_iff.mpr ⟨map_genWeightSpace_le f, LieSubmodule.map_le_range f⟩) ?_
  rintro - ⟨hm, ⟨m, rfl⟩⟩
  simp only [← comap_genWeightSpace_eq_of_injective hf, LieSubmodule.mem_map, LieSubmodule.mem_comap]
  exact ⟨m, hm, rfl⟩

Похожие утверждения