instHasImageCompOfIsIso — Mathlib

English

If f is an isomorphism and g has an image, then f ≫ g has an image; the construction is given by composing the image of g with inv f.

Русский

Если f является изоморфизмом и g имеет образ, то f ≫ g имеет образ; конструкция достигается композицией образа g с inv f.

LaTeX

$$$\text{HasImage}(f) \Rightarrow \text{HasImage}(f \circ g) \\text{(via isomorphism)}.$$$

Lean4

/-- If `has_image g`, then `has_image (f ≫ g)` when `f` is an isomorphism. -/
instance {X Y Z : C} (f : X ⟶ Y) [IsIso f] (g : Y ⟶ Z) [HasImage g] : HasImage (f ≫ g) where
  exists_image :=
    ⟨{  F :=
          { I := image g
            m := image.ι g
            e := f ≫ factorThruImage g }
        isImage :=
          {
            lift := fun F' =>
              image.lift
                { I := F'.I
                  m := F'.m
                  e := inv f ≫ F'.e } } }⟩

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