Theorems · Theorem · category theory

CategoryTheory.Limits.ImageMap.mk.inj

∀ {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}
  {map : CategoryTheory.Limits.image f.hom ⟶ CategoryTheory.Limits.image g.hom}
  {map_ι :
    autoParam
      (CategoryTheory.CategoryStruct.comp map (CategoryTheory.Limits.image.ι g.hom) =
        CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.image.ι f.hom) (CategoryTheory.Arrow.Hom.right sq))
      CategoryTheory.Limits.ImageMap.map_ι._autoParam}
  {map_1 : CategoryTheory.Limits.image f.hom ⟶ CategoryTheory.Limits.image g.hom}
  {map_ι_1 :
    autoParam
      (CategoryTheory.CategoryStruct.comp map_1 (CategoryTheory.Limits.image.ι g.hom) =
        CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.image.ι f.hom) (CategoryTheory.Arrow.Hom.right sq))
      CategoryTheory.Limits.ImageMap.map_ι._autoParam},
  { map := map, map_ι := map_ι } = { map := map_1, map_ι := map_ι_1 } → map = map_1

Defined in

Mathlib.CategoryTheory.Limits.Shapes.Images

Cited by

1 results in Mathlib

Foundations

Depth 21 from the axioms · uses Classical.choice