imageIsoRange_inv_image_ι — Mathlib

English

For any f: G ⟶ H, the inverse of the image isomorphism composed with the canonical image injection equals the inclusion of the linear-range into H; i.e., (imageIsoRange f)^{-1} ∘ ι_f = subtype_{range(f.hom)}.

Русский

Для любого f: G ⟶ H обратное изображению изоморфизма, после композиции с каноническим включением образа, совпадает с вложением диапазона в H; то есть (imageIsoRange f)^{-1} ∘ ι_f = subtype_{range(f.hom)}.

LaTeX

$$$$(\\mathrm{imageIsoRange}(f))^{-1} \\circ \\iota_f = \\mathrm{subtype}_{\\mathrm{range}(f.hom)} $$$$

Lean4

@[simp, reassoc, elementwise]
theorem imageIsoRange_inv_image_ι {G H : ModuleCat.{v} R} (f : G ⟶ H) :
    (imageIsoRange f).inv ≫ Limits.image.ι f = ModuleCat.ofHom (LinearMap.range f.hom).subtype :=
  IsImage.isoExt_inv_m _ _

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