imageSubobject_iso_comp — Mathlib

English

Precomposition by an isomorphism does not change the image subobject of a morphism f: X → Y.

Русский

Предобразование по изоморфизму не изменяет образ подобъекта морфизма f: X → Y.

LaTeX

$$$\mathrm{imageSubobject}(h \circ f) = \mathrm{imageSubobject}(f)$, for any isomorphism $h$.$$

Lean4

/-- Precomposing by an isomorphism does not change the image subobject. -/
theorem imageSubobject_iso_comp [HasEqualizers C] {X' : C} (h : X' ⟶ X) [IsIso h] (f : X ⟶ Y) [HasImage f] :
    imageSubobject (h ≫ f) = imageSubobject f :=
  le_antisymm (imageSubobject_comp_le h f) (Subobject.mk_le_mk_of_comm (inv (image.preComp h f)) (by simp))

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