Theorems · Definition · category theory

CategoryTheory.Limits.imageSubobjectMap

{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {W X Y Z : C} →
      {f : W ⟶ X} →
        [inst_1 : CategoryTheory.Limits.HasImage f] →
          {g : Y ⟶ Z} →
            [inst_2 : CategoryTheory.Limits.HasImage g] →
              (sq : CategoryTheory.Arrow.mk f ⟶ CategoryTheory.Arrow.mk g) →
                [CategoryTheory.Limits.HasImageMap sq] →
                  CategoryTheory.Subobject.underlying.obj (CategoryTheory.Limits.imageSubobject f) ⟶
                    CategoryTheory.Subobject.underlying.obj (CategoryTheory.Limits.imageSubobject g)

Given a commutative square between morphisms f and g, we have a morphism in the category from imageSubobject f to imageSubobject g.

Defined in

Mathlib.CategoryTheory.Subobject.Limits

Cited by

5 results in Mathlib

Foundations

Depth 39 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.Limits.HasImageCategoryTheory.Limits.HasImageCategoryTheory.Limits.HasImageMap