Theorems · Definition · category theory

CategoryTheory.Limits.ImageMap.transport

{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {f g : CategoryTheory.Arrow C} →
      [inst_1 : CategoryTheory.Limits.HasImage f.hom] →
        [inst_2 : CategoryTheory.Limits.HasImage g.hom] →
          (sq : f ⟶ g) →
            (F : CategoryTheory.Limits.MonoFactorisation f.hom) →
              {F' : CategoryTheory.Limits.MonoFactorisation g.hom} →
                CategoryTheory.Limits.IsImage F' →
                  {map : F.I ⟶ F'.I} →
                    CategoryTheory.CategoryStruct.comp map F'.m =
                        CategoryTheory.CategoryStruct.comp F.m (CategoryTheory.Arrow.Hom.right sq) →
                      CategoryTheory.Limits.ImageMap sq

To give an image map for a commutative square with f at the top and g at the bottom, it suffices to give a map between any mono factorisation of f and any image factorisation of g.

Defined in

Mathlib.CategoryTheory.Limits.Shapes.Images

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.Limits.HasImageCategoryTheory.Limits.HasImage