Loogle!

Result

Found 149 declarations mentioning CategoryTheory.Limits.image.

• CategoryTheory.Limits.image 📋 Mathlib.CategoryTheory.Limits.Shapes.Images
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Limits.HasImage f] : C
• CategoryTheory.Limits.factorThruImage 📋 Mathlib.CategoryTheory.Limits.Shapes.Images
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Limits.HasImage f] : X ⟶ CategoryTheory.Limits.image f
• CategoryTheory.Limits.image.ι 📋 Mathlib.CategoryTheory.Limits.Shapes.Images
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Limits.HasImage f] : CategoryTheory.Limits.image f ⟶ Y
• CategoryTheory.Limits.imageMonoIsoSource 📋 Mathlib.CategoryTheory.Limits.Shapes.Images
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Mono f] : CategoryTheory.Limits.image f ≅ X
• CategoryTheory.Limits.instMonoι 📋 Mathlib.CategoryTheory.Limits.Shapes.Images
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Limits.HasImage f] : CategoryTheory.Mono (CategoryTheory.Limits.image.ι f)
• CategoryTheory.Limits.epi_image_of_epi 📋 Mathlib.CategoryTheory.Limits.Shapes.Images
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Limits.HasImage f] [E : CategoryTheory.Epi f] : CategoryTheory.Epi (CategoryTheory.Limits.image.ι f)
• CategoryTheory.Limits.strongEpi_factorThruImage_of_strongEpiMonoFactorisation 📋 Mathlib.CategoryTheory.Limits.Shapes.Images
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y} [CategoryTheory.Limits.HasImage f] (F : CategoryTheory.Limits.StrongEpiMonoFactorisation f) : CategoryTheory.StrongEpi (CategoryTheory.Limits.factorThruImage f)
• CategoryTheory.Limits.image.lift 📋 Mathlib.CategoryTheory.Limits.Shapes.Images
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y} [CategoryTheory.Limits.HasImage f] (F' : CategoryTheory.Limits.MonoFactorisation f) : CategoryTheory.Limits.image f ⟶ F'.I
• CategoryTheory.Limits.im_obj 📋 Mathlib.CategoryTheory.Limits.Shapes.Images
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasImages C] [CategoryTheory.Limits.HasImageMaps C] (f : CategoryTheory.Arrow C) : CategoryTheory.Limits.im.obj f = CategoryTheory.Limits.image f.hom
• CategoryTheory.Limits.HasStrongEpiImages.mk 📋 Mathlib.CategoryTheory.Limits.Shapes.Images
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasImages C] (strong_factorThruImage : ∀ {X Y : C} (f : X ⟶ Y), CategoryTheory.StrongEpi (CategoryTheory.Limits.factorThruImage f)) : CategoryTheory.Limits.HasStrongEpiImages C
• CategoryTheory.Limits.HasStrongEpiImages.strong_factorThruImage 📋 Mathlib.CategoryTheory.Limits.Shapes.Images
  {C : Type u} {inst✝ : CategoryTheory.Category.{v, u} C} {inst✝¹ : CategoryTheory.Limits.HasImages C} [self : CategoryTheory.Limits.HasStrongEpiImages C] {X Y : C} (f : X ⟶ Y) : CategoryTheory.StrongEpi (CategoryTheory.Limits.factorThruImage f)
• CategoryTheory.Limits.image.lift_mono 📋 Mathlib.CategoryTheory.Limits.Shapes.Images
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y} [CategoryTheory.Limits.HasImage f] (F' : CategoryTheory.Limits.MonoFactorisation f) : CategoryTheory.Mono (CategoryTheory.Limits.image.lift F')
• CategoryTheory.Limits.image.fac 📋 Mathlib.CategoryTheory.Limits.Shapes.Images
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Limits.HasImage f] : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.factorThruImage f) (CategoryTheory.Limits.image.ι f) = f
• CategoryTheory.Limits.epi_of_epi_image 📋 Mathlib.CategoryTheory.Limits.Shapes.Images
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Limits.HasImage f] [CategoryTheory.Epi (CategoryTheory.Limits.image.ι f)] [CategoryTheory.Epi (CategoryTheory.Limits.factorThruImage f)] : CategoryTheory.Epi f
• CategoryTheory.Limits.image.eqToIso 📋 Mathlib.CategoryTheory.Limits.Shapes.Images
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {f f' : X ⟶ Y} [CategoryTheory.Limits.HasImage f] [CategoryTheory.Limits.HasImage f'] (h : f = f') : CategoryTheory.Limits.image f ≅ CategoryTheory.Limits.image f'
• CategoryTheory.Limits.image.eqToHom 📋 Mathlib.CategoryTheory.Limits.Shapes.Images
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {f f' : X ⟶ Y} [CategoryTheory.Limits.HasImage f] [CategoryTheory.Limits.HasImage f'] (h : f = f') : CategoryTheory.Limits.image f ⟶ CategoryTheory.Limits.image f'
• CategoryTheory.Limits.instIsIsoEqToHom 📋 Mathlib.CategoryTheory.Limits.Shapes.Images
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {f f' : X ⟶ Y} [CategoryTheory.Limits.HasImage f] [CategoryTheory.Limits.HasImage f'] (h : f = f') : CategoryTheory.IsIso (CategoryTheory.Limits.image.eqToHom h)
• CategoryTheory.Limits.image.compIso 📋 Mathlib.CategoryTheory.Limits.Shapes.Images
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) {Z : C} (g : Y ⟶ Z) [CategoryTheory.Limits.HasEqualizers C] [CategoryTheory.Limits.HasImage f] [CategoryTheory.IsIso g] : CategoryTheory.Limits.image f ≅ CategoryTheory.Limits.image (CategoryTheory.CategoryStruct.comp f g)
• CategoryTheory.Limits.image.preComp 📋 Mathlib.CategoryTheory.Limits.Shapes.Images
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) {Z : C} (g : Y ⟶ Z) [CategoryTheory.Limits.HasImage g] [CategoryTheory.Limits.HasImage (CategoryTheory.CategoryStruct.comp f g)] : CategoryTheory.Limits.image (CategoryTheory.CategoryStruct.comp f g) ⟶ CategoryTheory.Limits.image g
• CategoryTheory.Limits.image.preComp_mono 📋 Mathlib.CategoryTheory.Limits.Shapes.Images
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) {Z : C} (g : Y ⟶ Z) [CategoryTheory.Limits.HasImage g] [CategoryTheory.Limits.HasImage (CategoryTheory.CategoryStruct.comp f g)] : CategoryTheory.Mono (CategoryTheory.Limits.image.preComp f g)
• CategoryTheory.Limits.image.fac_lift 📋 Mathlib.CategoryTheory.Limits.Shapes.Images
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y} [CategoryTheory.Limits.HasImage f] (F' : CategoryTheory.Limits.MonoFactorisation f) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.factorThruImage f) (CategoryTheory.Limits.image.lift F') = F'.e
• CategoryTheory.Limits.image.lift_fac 📋 Mathlib.CategoryTheory.Limits.Shapes.Images
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y} [CategoryTheory.Limits.HasImage f] (F' : CategoryTheory.Limits.MonoFactorisation f) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.image.lift F') F'.m = CategoryTheory.Limits.image.ι f
• CategoryTheory.Limits.instEpiFactorThruImageOfHasLimitWalkingParallelPairParallelPair 📋 Mathlib.CategoryTheory.Limits.Shapes.Images
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Limits.HasImage f] [∀ {Z : C} (g h : CategoryTheory.Limits.image f ⟶ Z), CategoryTheory.Limits.HasLimit (CategoryTheory.Limits.parallelPair g h)] : CategoryTheory.Epi (CategoryTheory.Limits.factorThruImage f)
• CategoryTheory.Limits.imageMonoIsoSource_inv_ι 📋 Mathlib.CategoryTheory.Limits.Shapes.Images
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Mono f] : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.imageMonoIsoSource f).inv (CategoryTheory.Limits.image.ι f) = f
• CategoryTheory.Limits.image.isoStrongEpiMono 📋 Mathlib.CategoryTheory.Limits.Shapes.Images
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasStrongEpiMonoFactorisations C] {X Y : C} {f : X ⟶ Y} {I' : C} (e : X ⟶ I') (m : I' ⟶ Y) (comm : CategoryTheory.CategoryStruct.comp e m = f) [CategoryTheory.StrongEpi e] [CategoryTheory.Mono m] : I' ≅ CategoryTheory.Limits.image f
• CategoryTheory.Limits.image.preComp_epi_of_epi 📋 Mathlib.CategoryTheory.Limits.Shapes.Images
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) {Z : C} (g : Y ⟶ Z) [CategoryTheory.Limits.HasEqualizers C] [CategoryTheory.Limits.HasImage g] [CategoryTheory.Limits.HasImage (CategoryTheory.CategoryStruct.comp f g)] [CategoryTheory.Epi f] : CategoryTheory.Epi (CategoryTheory.Limits.image.preComp f g)
• CategoryTheory.Limits.image.fac_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.Images
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Limits.HasImage f] {Z : C} (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.factorThruImage f) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.image.ι f) h) = CategoryTheory.CategoryStruct.comp f h
• CategoryTheory.Limits.image.isIso_precomp_iso 📋 Mathlib.CategoryTheory.Limits.Shapes.Images
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z : C} (g : Y ⟶ Z) [CategoryTheory.Limits.HasEqualizers C] (f : X ⟶ Y) [CategoryTheory.IsIso f] [CategoryTheory.Limits.HasImage g] : CategoryTheory.IsIso (CategoryTheory.Limits.image.preComp f g)
• CategoryTheory.Limits.ImageMap.map 📋 Mathlib.CategoryTheory.Limits.Shapes.Images
  {C : Type u} [CategoryTheory.Category.{v, u} C] {f g : CategoryTheory.Arrow C} [CategoryTheory.Limits.HasImage f.hom] [CategoryTheory.Limits.HasImage g.hom] {sq : f ⟶ g} (self : CategoryTheory.Limits.ImageMap sq) : CategoryTheory.Limits.image f.hom ⟶ CategoryTheory.Limits.image g.hom
• CategoryTheory.Limits.image.map 📋 Mathlib.CategoryTheory.Limits.Shapes.Images
  {C : Type u} [CategoryTheory.Category.{v, u} C] {f g : CategoryTheory.Arrow C} [CategoryTheory.Limits.HasImage f.hom] [CategoryTheory.Limits.HasImage g.hom] (sq : f ⟶ g) [CategoryTheory.Limits.HasImageMap sq] : CategoryTheory.Limits.image f.hom ⟶ CategoryTheory.Limits.image g.hom
• CategoryTheory.Limits.imageMonoIsoSource_hom_self 📋 Mathlib.CategoryTheory.Limits.Shapes.Images
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Mono f] : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.imageMonoIsoSource f).hom f = CategoryTheory.Limits.image.ι f
• CategoryTheory.Limits.image.map_id 📋 Mathlib.CategoryTheory.Limits.Shapes.Images
  {C : Type u} [CategoryTheory.Category.{v, u} C] (f : CategoryTheory.Arrow C) [CategoryTheory.Limits.HasImage f.hom] [CategoryTheory.Limits.HasImageMap (CategoryTheory.CategoryStruct.id f)] : CategoryTheory.Limits.image.map (CategoryTheory.CategoryStruct.id f) = CategoryTheory.CategoryStruct.id (CategoryTheory.Limits.image f.hom)
• CategoryTheory.Limits.im_map 📋 Mathlib.CategoryTheory.Limits.Shapes.Images
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasImages C] [CategoryTheory.Limits.HasImageMaps C] {X✝ Y✝ : CategoryTheory.Arrow C} (st : X✝ ⟶ Y✝) : CategoryTheory.Limits.im.map st = CategoryTheory.Limits.image.map st
• CategoryTheory.Limits.ImageMap.map_uniq 📋 Mathlib.CategoryTheory.Limits.Shapes.Images
  {C : Type u} [CategoryTheory.Category.{v, u} C] {f g : CategoryTheory.Arrow C} [CategoryTheory.Limits.HasImage f.hom] [CategoryTheory.Limits.HasImage g.hom] {sq : f ⟶ g} (F G : CategoryTheory.Limits.ImageMap sq) : F.map = G.map
• CategoryTheory.Limits.image.fac_lift_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.Images
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y} [CategoryTheory.Limits.HasImage f] (F' : CategoryTheory.Limits.MonoFactorisation f) {Z : C} (h : F'.I ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.factorThruImage f) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.image.lift F') h) = CategoryTheory.CategoryStruct.comp F'.e h
• CategoryTheory.Limits.image.lift_fac_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.Images
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y} [CategoryTheory.Limits.HasImage f] (F' : CategoryTheory.Limits.MonoFactorisation f) {Z : C} (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.image.lift F') (CategoryTheory.CategoryStruct.comp F'.m h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.image.ι f) h
• CategoryTheory.Limits.image.eq_fac 📋 Mathlib.CategoryTheory.Limits.Shapes.Images
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {f f' : X ⟶ Y} [CategoryTheory.Limits.HasImage f] [CategoryTheory.Limits.HasImage f'] [CategoryTheory.Limits.HasEqualizers C] (h : f = f') : CategoryTheory.Limits.image.ι f = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.image.eqToIso h).hom (CategoryTheory.Limits.image.ι f')
• CategoryTheory.Limits.imageMonoIsoSource_inv_ι_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.Images
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Mono f] {Z : C} (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.imageMonoIsoSource f).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.image.ι f) h) = CategoryTheory.CategoryStruct.comp f h
• CategoryTheory.Limits.HasImage.uniq 📋 Mathlib.CategoryTheory.Limits.Shapes.Images
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y} [CategoryTheory.Limits.HasImage f] (F' : CategoryTheory.Limits.MonoFactorisation f) (l : CategoryTheory.Limits.image f ⟶ F'.I) (w : CategoryTheory.CategoryStruct.comp l F'.m = CategoryTheory.Limits.image.ι f) : l = CategoryTheory.Limits.image.lift F'
• CategoryTheory.Limits.image.preComp_ι 📋 Mathlib.CategoryTheory.Limits.Shapes.Images
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) {Z : C} (g : Y ⟶ Z) [CategoryTheory.Limits.HasImage g] [CategoryTheory.Limits.HasImage (CategoryTheory.CategoryStruct.comp f g)] : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.image.preComp f g) (CategoryTheory.Limits.image.ι g) = CategoryTheory.Limits.image.ι (CategoryTheory.CategoryStruct.comp f g)
• CategoryTheory.Limits.ImageMap.ext 📋 Mathlib.CategoryTheory.Limits.Shapes.Images
  {C : Type u} {inst✝ : CategoryTheory.Category.{v, u} C} {f g : CategoryTheory.Arrow C} {inst✝¹ : CategoryTheory.Limits.HasImage f.hom} {inst✝² : CategoryTheory.Limits.HasImage g.hom} {sq : f ⟶ g} {x y : CategoryTheory.Limits.ImageMap sq} (map : x.map = y.map) : x = y
• CategoryTheory.Limits.ImageMap.ext_iff 📋 Mathlib.CategoryTheory.Limits.Shapes.Images
  {C : Type u} {inst✝ : CategoryTheory.Category.{v, u} C} {f g : CategoryTheory.Arrow C} {inst✝¹ : CategoryTheory.Limits.HasImage f.hom} {inst✝² : CategoryTheory.Limits.HasImage g.hom} {sq : f ⟶ g} {x y : CategoryTheory.Limits.ImageMap sq} : x = y ↔ x.map = y.map
• CategoryTheory.Limits.image.factorThruImage_preComp 📋 Mathlib.CategoryTheory.Limits.Shapes.Images
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) {Z : C} (g : Y ⟶ Z) [CategoryTheory.Limits.HasImage g] [CategoryTheory.Limits.HasImage (CategoryTheory.CategoryStruct.comp f g)] : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.factorThruImage (CategoryTheory.CategoryStruct.comp f g)) (CategoryTheory.Limits.image.preComp f g) = CategoryTheory.CategoryStruct.comp f (CategoryTheory.Limits.factorThruImage g)
• CategoryTheory.Limits.imageMonoIsoSource_hom_self_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.Images
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Mono f] {Z : C} (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.imageMonoIsoSource f).hom (CategoryTheory.CategoryStruct.comp f h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.image.ι f) h
• CategoryTheory.Limits.image.ext 📋 Mathlib.CategoryTheory.Limits.Shapes.Images
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Limits.HasImage f] {W : C} {g h : CategoryTheory.Limits.image f ⟶ W} [CategoryTheory.Limits.HasLimit (CategoryTheory.Limits.parallelPair g h)] (w : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.factorThruImage f) g = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.factorThruImage f) h) : g = h
• CategoryTheory.Limits.image.isoStrongEpiMono_hom_comp_ι 📋 Mathlib.CategoryTheory.Limits.Shapes.Images
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasStrongEpiMonoFactorisations C] {X Y : C} {f : X ⟶ Y} {I' : C} (e : X ⟶ I') (m : I' ⟶ Y) (comm : CategoryTheory.CategoryStruct.comp e m = f) [CategoryTheory.StrongEpi e] [CategoryTheory.Mono m] : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.image.isoStrongEpiMono e m comm).hom (CategoryTheory.Limits.image.ι f) = m
• CategoryTheory.Limits.image.lift_mk_factorThruImage 📋 Mathlib.CategoryTheory.Limits.Shapes.Images
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y} [CategoryTheory.Limits.HasImage f] : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.image.lift { I := CategoryTheory.Limits.image f, m := CategoryTheory.Limits.image.ι f, m_mono := ⋯, e := CategoryTheory.Limits.factorThruImage f, fac := ⋯ }) (CategoryTheory.Limits.image.ι f) = CategoryTheory.Limits.image.ι f
• CategoryTheory.Limits.image.lift_mk_factorThruImage_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.Images
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y} [CategoryTheory.Limits.HasImage f] {Z : C} (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.image.lift { I := CategoryTheory.Limits.image f, m := CategoryTheory.Limits.image.ι f, m_mono := ⋯, e := CategoryTheory.Limits.factorThruImage f, fac := ⋯ }) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.image.ι f) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.image.ι f) h
• CategoryTheory.Limits.image.isoStrongEpiMono_inv_comp_mono 📋 Mathlib.CategoryTheory.Limits.Shapes.Images
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasStrongEpiMonoFactorisations C] {X Y : C} {f : X ⟶ Y} {I' : C} (e : X ⟶ I') (m : I' ⟶ Y) (comm : CategoryTheory.CategoryStruct.comp e m = f) [CategoryTheory.StrongEpi e] [CategoryTheory.Mono m] : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.image.isoStrongEpiMono e m comm).inv m = CategoryTheory.Limits.image.ι f
• CategoryTheory.Limits.image.factorThruImage_preComp_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.Images
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) {Z : C} (g : Y ⟶ Z) [CategoryTheory.Limits.HasImage g] [CategoryTheory.Limits.HasImage (CategoryTheory.CategoryStruct.comp f g)] {Z✝ : C} (h : CategoryTheory.Limits.image g ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.factorThruImage (CategoryTheory.CategoryStruct.comp f g)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.image.preComp f g) h) = CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.factorThruImage g) h)
• CategoryTheory.Limits.image.preComp_ι_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.Images
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) {Z : C} (g : Y ⟶ Z) [CategoryTheory.Limits.HasImage g] [CategoryTheory.Limits.HasImage (CategoryTheory.CategoryStruct.comp f g)] {Z✝ : C} (h : Z ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.image.preComp f g) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.image.ι g) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.image.ι (CategoryTheory.CategoryStruct.comp f g)) h
• CategoryTheory.Limits.image.compIso_hom_comp_image_ι 📋 Mathlib.CategoryTheory.Limits.Shapes.Images
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) {Z : C} (g : Y ⟶ Z) [CategoryTheory.Limits.HasEqualizers C] [CategoryTheory.Limits.HasImage f] [CategoryTheory.IsIso g] : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.image.compIso f g).hom (CategoryTheory.Limits.image.ι (CategoryTheory.CategoryStruct.comp f g)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.image.ι f) g
• CategoryTheory.Limits.ImageMap.factor_map 📋 Mathlib.CategoryTheory.Limits.Shapes.Images
  {C : Type u} [CategoryTheory.Category.{v, u} C] {f g : CategoryTheory.Arrow C} [CategoryTheory.Limits.HasImage f.hom] [CategoryTheory.Limits.HasImage g.hom] (sq : f ⟶ g) (m : CategoryTheory.Limits.ImageMap sq) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.factorThruImage f.hom) m.map = CategoryTheory.CategoryStruct.comp (CategoryTheory.Arrow.Hom.left sq) (CategoryTheory.Limits.factorThruImage g.hom)
• CategoryTheory.Limits.ImageMap.map_ι 📋 Mathlib.CategoryTheory.Limits.Shapes.Images
  {C : Type u} [CategoryTheory.Category.{v, u} C] {f g : CategoryTheory.Arrow C} [CategoryTheory.Limits.HasImage f.hom] [CategoryTheory.Limits.HasImage g.hom] {sq : f ⟶ g} (self : CategoryTheory.Limits.ImageMap sq) : CategoryTheory.CategoryStruct.comp self.map (CategoryTheory.Limits.image.ι g.hom) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.image.ι f.hom) (CategoryTheory.Arrow.Hom.right sq)
• CategoryTheory.Limits.image.factor_map 📋 Mathlib.CategoryTheory.Limits.Shapes.Images
  {C : Type u} [CategoryTheory.Category.{v, u} C] {f g : CategoryTheory.Arrow C} [CategoryTheory.Limits.HasImage f.hom] [CategoryTheory.Limits.HasImage g.hom] (sq : f ⟶ g) [CategoryTheory.Limits.HasImageMap sq] : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.factorThruImage f.hom) (CategoryTheory.Limits.image.map sq) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Arrow.Hom.left sq) (CategoryTheory.Limits.factorThruImage g.hom)
• CategoryTheory.Limits.image.map_ι 📋 Mathlib.CategoryTheory.Limits.Shapes.Images
  {C : Type u} [CategoryTheory.Category.{v, u} C] {f g : CategoryTheory.Arrow C} [CategoryTheory.Limits.HasImage f.hom] [CategoryTheory.Limits.HasImage g.hom] (sq : f ⟶ g) [CategoryTheory.Limits.HasImageMap sq] : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.image.map sq) (CategoryTheory.Limits.image.ι g.hom) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.image.ι f.hom) (CategoryTheory.Arrow.Hom.right sq)
• CategoryTheory.Limits.image.compIso_inv_comp_image_ι 📋 Mathlib.CategoryTheory.Limits.Shapes.Images
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) {Z : C} (g : Y ⟶ Z) [CategoryTheory.Limits.HasEqualizers C] [CategoryTheory.Limits.HasImage f] [CategoryTheory.IsIso g] : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.image.compIso f g).inv (CategoryTheory.Limits.image.ι f) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.image.ι (CategoryTheory.CategoryStruct.comp f g)) (CategoryTheory.inv g)
• CategoryTheory.Limits.ImageMap.mk 📋 Mathlib.CategoryTheory.Limits.Shapes.Images
  {C : Type u} [CategoryTheory.Category.{v, u} C] {f g : CategoryTheory.Arrow C} [CategoryTheory.Limits.HasImage f.hom] [CategoryTheory.Limits.HasImage g.hom] {sq : f ⟶ g} (map : CategoryTheory.Limits.image f.hom ⟶ CategoryTheory.Limits.image g.hom) (map_ι : CategoryTheory.CategoryStruct.comp map (CategoryTheory.Limits.image.ι g.hom) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.image.ι f.hom) (CategoryTheory.Arrow.Hom.right sq) := by aesop) : CategoryTheory.Limits.ImageMap sq
• CategoryTheory.Limits.image.compIso_hom_comp_image_ι_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.Images
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) {Z : C} (g : Y ⟶ Z) [CategoryTheory.Limits.HasEqualizers C] [CategoryTheory.Limits.HasImage f] [CategoryTheory.IsIso g] {Z✝ : C} (h : Z ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.image.compIso f g).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.image.ι (CategoryTheory.CategoryStruct.comp f g)) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.image.ι f) (CategoryTheory.CategoryStruct.comp g h)
• CategoryTheory.Limits.ImageMap.factor_map_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.Images
  {C : Type u} [CategoryTheory.Category.{v, u} C] {f g : CategoryTheory.Arrow C} [CategoryTheory.Limits.HasImage f.hom] [CategoryTheory.Limits.HasImage g.hom] (sq : f ⟶ g) (m : CategoryTheory.Limits.ImageMap sq) {Z : C} (h : CategoryTheory.Limits.image g.hom ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.factorThruImage f.hom) (CategoryTheory.CategoryStruct.comp m.map h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Arrow.Hom.left sq) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.factorThruImage g.hom) h)
• CategoryTheory.Limits.ImageMap.map_ι_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.Images
  {C : Type u} [CategoryTheory.Category.{v, u} C] {f g : CategoryTheory.Arrow C} [CategoryTheory.Limits.HasImage f.hom] [CategoryTheory.Limits.HasImage g.hom] {sq : f ⟶ g} (self : CategoryTheory.Limits.ImageMap sq) {Z : C} (h : g.right ⟶ Z) : CategoryTheory.CategoryStruct.comp self.map (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.image.ι g.hom) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.image.ι f.hom) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Arrow.Hom.right sq) h)
• CategoryTheory.Limits.image.map_comp 📋 Mathlib.CategoryTheory.Limits.Shapes.Images
  {C : Type u} [CategoryTheory.Category.{v, u} C] {f g : CategoryTheory.Arrow C} [CategoryTheory.Limits.HasImage f.hom] [CategoryTheory.Limits.HasImage g.hom] (sq : f ⟶ g) [CategoryTheory.Limits.HasImageMap sq] {h : CategoryTheory.Arrow C} [CategoryTheory.Limits.HasImage h.hom] (sq' : g ⟶ h) [CategoryTheory.Limits.HasImageMap sq'] [CategoryTheory.Limits.HasImageMap (CategoryTheory.CategoryStruct.comp sq sq')] : CategoryTheory.Limits.image.map (CategoryTheory.CategoryStruct.comp sq sq') = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.image.map sq) (CategoryTheory.Limits.image.map sq')
• CategoryTheory.Limits.image.compIso_inv_comp_image_ι_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.Images
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) {Z : C} (g : Y ⟶ Z) [CategoryTheory.Limits.HasEqualizers C] [CategoryTheory.Limits.HasImage f] [CategoryTheory.IsIso g] {Z✝ : C} (h : Y ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.image.compIso f g).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.image.ι f) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.image.ι (CategoryTheory.CategoryStruct.comp f g)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.inv g) h)
• CategoryTheory.Limits.image.lift_mk_comp_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.Images
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) [CategoryTheory.Limits.HasImage g] [CategoryTheory.Limits.HasImage (CategoryTheory.CategoryStruct.comp f g)] (h : Y ⟶ CategoryTheory.Limits.image g) (H : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f h) (CategoryTheory.Limits.image.ι g) = CategoryTheory.CategoryStruct.comp f g) {Z✝ : C} (h✝ : Z ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.image.lift { I := CategoryTheory.Limits.image g, m := CategoryTheory.Limits.image.ι g, m_mono := ⋯, e := CategoryTheory.CategoryStruct.comp f h, fac := ⋯ }) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.image.ι g) h✝) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.image.ι (CategoryTheory.CategoryStruct.comp f g)) h✝
• CategoryTheory.Limits.image.map_homMk'_ι 📋 Mathlib.CategoryTheory.Limits.Shapes.Images
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y P Q : C} {k : X ⟶ Y} [CategoryTheory.Limits.HasImage k] {l : P ⟶ Q} [CategoryTheory.Limits.HasImage l] {m : X ⟶ P} {n : Y ⟶ Q} (w : CategoryTheory.CategoryStruct.comp m l = CategoryTheory.CategoryStruct.comp k n) [CategoryTheory.Limits.HasImageMap (CategoryTheory.Arrow.homMk' m n w)] : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.image.map (CategoryTheory.Arrow.homMk' m n w)) (CategoryTheory.Limits.image.ι l) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.image.ι k) n
• CategoryTheory.Limits.image.lift_mk_comp 📋 Mathlib.CategoryTheory.Limits.Shapes.Images
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) [CategoryTheory.Limits.HasImage g] [CategoryTheory.Limits.HasImage (CategoryTheory.CategoryStruct.comp f g)] (h : Y ⟶ CategoryTheory.Limits.image g) (H : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f h) (CategoryTheory.Limits.image.ι g) = CategoryTheory.CategoryStruct.comp f g) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.image.lift { I := CategoryTheory.Limits.image g, m := CategoryTheory.Limits.image.ι g, m_mono := ⋯, e := CategoryTheory.CategoryStruct.comp f h, fac := ⋯ }) (CategoryTheory.Limits.image.ι g) = CategoryTheory.Limits.image.ι (CategoryTheory.CategoryStruct.comp f g)
• CategoryTheory.Limits.image.preComp_comp 📋 Mathlib.CategoryTheory.Limits.Shapes.Images
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) {Z : C} (g : Y ⟶ Z) {W : C} (h : Z ⟶ W) [CategoryTheory.Limits.HasImage (CategoryTheory.CategoryStruct.comp g h)] [CategoryTheory.Limits.HasImage (CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp g h))] [CategoryTheory.Limits.HasImage h] [CategoryTheory.Limits.HasImage (CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g) h)] : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.image.preComp f (CategoryTheory.CategoryStruct.comp g h)) (CategoryTheory.Limits.image.preComp g h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.image.eqToHom ⋯) (CategoryTheory.Limits.image.preComp (CategoryTheory.CategoryStruct.comp f g) h)
• CategoryTheory.Limits.ImageMap.map_uniq_aux 📋 Mathlib.CategoryTheory.Limits.Shapes.Images
  {C : Type u} [CategoryTheory.Category.{v, u} C] {f g : CategoryTheory.Arrow C} [CategoryTheory.Limits.HasImage f.hom] [CategoryTheory.Limits.HasImage g.hom] {sq : f ⟶ g} (map : CategoryTheory.Limits.image f.hom ⟶ CategoryTheory.Limits.image g.hom) (map_ι : CategoryTheory.CategoryStruct.comp map (CategoryTheory.Limits.image.ι g.hom) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.image.ι f.hom) (CategoryTheory.Arrow.Hom.right sq) := by cat_disch) (map' : CategoryTheory.Limits.image f.hom ⟶ CategoryTheory.Limits.image g.hom) (map_ι' : CategoryTheory.CategoryStruct.comp map' (CategoryTheory.Limits.image.ι g.hom) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.image.ι f.hom) (CategoryTheory.Arrow.Hom.right sq)) : map = map'
• CategoryTheory.Limits.ImageMap.mk.injEq' 📋 Mathlib.CategoryTheory.Limits.Shapes.Images
  {C : Type u} [CategoryTheory.Category.{v, u} C] {f g : CategoryTheory.Arrow C} [CategoryTheory.Limits.HasImage f.hom] [CategoryTheory.Limits.HasImage g.hom] {sq : f ⟶ g} (map : CategoryTheory.Limits.image f.hom ⟶ CategoryTheory.Limits.image g.hom) (map_ι : CategoryTheory.CategoryStruct.comp map (CategoryTheory.Limits.image.ι g.hom) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.image.ι f.hom) (CategoryTheory.Arrow.Hom.right sq) := by aesop) (map✝ : CategoryTheory.Limits.image f.hom ⟶ CategoryTheory.Limits.image g.hom) (map_ι✝ : CategoryTheory.CategoryStruct.comp map✝ (CategoryTheory.Limits.image.ι g.hom) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.image.ι f.hom) (CategoryTheory.Arrow.Hom.right sq) := by aesop) : ({ map := map, map_ι := map_ι } = { map := map✝, map_ι := map_ι✝ }) = (map = map✝)
• CategoryTheory.Limits.imageZero 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] {X Y : C} : CategoryTheory.Limits.image 0 ≅ 0
• CategoryTheory.Limits.imageZero' 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] {X Y : C} {f : X ⟶ Y} (h : f = 0) [CategoryTheory.Limits.HasImage f] : CategoryTheory.Limits.image f ≅ 0
• CategoryTheory.Limits.eq_zero_of_image_eq_zero 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} {f : X ⟶ Y} [CategoryTheory.Limits.HasImage f] (w : CategoryTheory.Limits.image.ι f = 0) : f = 0
• CategoryTheory.Limits.nonzero_image_of_nonzero 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} {f : X ⟶ Y} [CategoryTheory.Limits.HasImage f] (w : f ≠ 0) : CategoryTheory.Limits.image.ι f ≠ 0
• CategoryTheory.Limits.image.ι_zero' 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasEqualizers C] {X Y : C} {f : X ⟶ Y} (h : f = 0) [CategoryTheory.Limits.HasImage f] : CategoryTheory.Limits.image.ι f = 0
• CategoryTheory.Limits.comp_factorThruImage_eq_zero 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {X Y Z : C} {f : X ⟶ Y} {g : Y ⟶ Z} [CategoryTheory.Limits.HasImage g] (h : CategoryTheory.CategoryStruct.comp f g = 0) : CategoryTheory.CategoryStruct.comp f (CategoryTheory.Limits.factorThruImage g) = 0
• CategoryTheory.Limits.image_ι_comp_eq_zero 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {X Y Z : C} {f : X ⟶ Y} {g : Y ⟶ Z} [CategoryTheory.Limits.HasImage f] [CategoryTheory.Epi (CategoryTheory.Limits.factorThruImage f)] (h : CategoryTheory.CategoryStruct.comp f g = 0) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.image.ι f) g = 0
• CategoryTheory.Limits.image.ι_zero 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] {X Y : C} [CategoryTheory.Limits.HasImage 0] : CategoryTheory.Limits.image.ι 0 = 0
• CategoryTheory.Limits.kernelFactorThruImage 📋 Mathlib.CategoryTheory.Limits.Shapes.Kernels
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Limits.HasKernel f] [CategoryTheory.Limits.HasImage f] [CategoryTheory.Limits.HasKernel (CategoryTheory.Limits.factorThruImage f)] : CategoryTheory.Limits.kernel (CategoryTheory.Limits.factorThruImage f) ≅ CategoryTheory.Limits.kernel f
• CategoryTheory.Limits.cokernelImageι 📋 Mathlib.CategoryTheory.Limits.Shapes.Kernels
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Limits.HasImage f] [CategoryTheory.Limits.HasCokernel (CategoryTheory.Limits.image.ι f)] [CategoryTheory.Limits.HasCokernel f] [CategoryTheory.Epi (CategoryTheory.Limits.factorThruImage f)] : CategoryTheory.Limits.cokernel (CategoryTheory.Limits.image.ι f) ≅ CategoryTheory.Limits.cokernel f
• CategoryTheory.Limits.kernelFactorThruImage_inv_comp_ι 📋 Mathlib.CategoryTheory.Limits.Shapes.Kernels
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Limits.HasKernel f] [CategoryTheory.Limits.HasImage f] [CategoryTheory.Limits.HasKernel (CategoryTheory.Limits.factorThruImage f)] : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernelFactorThruImage f).inv (CategoryTheory.Limits.kernel.ι (CategoryTheory.Limits.factorThruImage f)) = CategoryTheory.Limits.kernel.ι f
• CategoryTheory.Limits.kernelFactorThruImage_hom_comp_ι 📋 Mathlib.CategoryTheory.Limits.Shapes.Kernels
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Limits.HasKernel f] [CategoryTheory.Limits.HasImage f] [CategoryTheory.Limits.HasKernel (CategoryTheory.Limits.factorThruImage f)] : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernelFactorThruImage f).hom (CategoryTheory.Limits.kernel.ι f) = CategoryTheory.Limits.kernel.ι (CategoryTheory.Limits.factorThruImage f)
• CategoryTheory.Limits.cokernelImageι_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.Kernels
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Limits.HasImage f] [CategoryTheory.Limits.HasCokernel (CategoryTheory.Limits.image.ι f)] [CategoryTheory.Limits.HasCokernel f] [CategoryTheory.Epi (CategoryTheory.Limits.factorThruImage f)] : (CategoryTheory.Limits.cokernelImageι f).hom = CategoryTheory.Limits.cokernel.desc (CategoryTheory.Limits.image.ι f) (CategoryTheory.Limits.cokernel.π f) ⋯
• CategoryTheory.Limits.cokernelImageι_inv 📋 Mathlib.CategoryTheory.Limits.Shapes.Kernels
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Limits.HasImage f] [CategoryTheory.Limits.HasCokernel (CategoryTheory.Limits.image.ι f)] [CategoryTheory.Limits.HasCokernel f] [CategoryTheory.Epi (CategoryTheory.Limits.factorThruImage f)] : (CategoryTheory.Limits.cokernelImageι f).inv = CategoryTheory.Limits.cokernel.desc f (CategoryTheory.Limits.cokernel.π (CategoryTheory.Limits.image.ι f)) ⋯
• CategoryTheory.Limits.kernelFactorThruImage_inv_comp_ι_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.Kernels
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Limits.HasKernel f] [CategoryTheory.Limits.HasImage f] [CategoryTheory.Limits.HasKernel (CategoryTheory.Limits.factorThruImage f)] {Z : C} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernelFactorThruImage f).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.ι (CategoryTheory.Limits.factorThruImage f)) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.ι f) h
• CategoryTheory.Limits.kernelFactorThruImage_hom_comp_ι_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.Kernels
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Limits.HasKernel f] [CategoryTheory.Limits.HasImage f] [CategoryTheory.Limits.HasKernel (CategoryTheory.Limits.factorThruImage f)] {Z : C} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernelFactorThruImage f).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.ι f) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.ι (CategoryTheory.Limits.factorThruImage f)) h
• CategoryTheory.Abelian.coimageIsoImage' 📋 Mathlib.CategoryTheory.Abelian.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {X Y : C} (f : X ⟶ Y) : CategoryTheory.Abelian.coimage f ≅ CategoryTheory.Limits.image f
• CategoryTheory.Abelian.imageIsoImage 📋 Mathlib.CategoryTheory.Abelian.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {X Y : C} (f : X ⟶ Y) : CategoryTheory.Abelian.image f ≅ CategoryTheory.Limits.image f
• CategoryTheory.Abelian.coimageIsoImage'_hom 📋 Mathlib.CategoryTheory.Abelian.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {X Y : C} (f : X ⟶ Y) : (CategoryTheory.Abelian.coimageIsoImage' f).hom = CategoryTheory.Limits.cokernel.desc (CategoryTheory.Limits.kernel.ι f) (CategoryTheory.Limits.factorThruImage f) ⋯
• CategoryTheory.Abelian.imageIsoImage_inv 📋 Mathlib.CategoryTheory.Abelian.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {X Y : C} (f : X ⟶ Y) : (CategoryTheory.Abelian.imageIsoImage f).inv = CategoryTheory.Limits.kernel.lift (CategoryTheory.Limits.cokernel.π f) (CategoryTheory.Limits.image.ι f) ⋯
• CategoryTheory.Abelian.factorThruImage_comp_coimageIsoImage'_inv 📋 Mathlib.CategoryTheory.Abelian.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {X Y : C} (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.factorThruImage f) (CategoryTheory.Abelian.coimageIsoImage' f).inv = CategoryTheory.Limits.cokernel.π (CategoryTheory.Limits.kernel.ι f)
• CategoryTheory.Abelian.imageIsoImage_hom_comp_image_ι 📋 Mathlib.CategoryTheory.Abelian.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {X Y : C} (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Abelian.imageIsoImage f).hom (CategoryTheory.Limits.image.ι f) = CategoryTheory.Limits.kernel.ι (CategoryTheory.Limits.cokernel.π f)
• CategoryTheory.ShortComplex.homologyIsoImageICyclesCompPOpcycles 📋 Mathlib.Algebra.Homology.ShortComplex.Abelian
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex C) : S.homology ≅ CategoryTheory.Limits.image (CategoryTheory.CategoryStruct.comp S.iCycles S.pOpcycles)
• CategoryTheory.ShortComplex.homologyIsoImageICyclesCompPOpcycles_ι 📋 Mathlib.Algebra.Homology.ShortComplex.Abelian
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex C) : CategoryTheory.CategoryStruct.comp S.homologyIsoImageICyclesCompPOpcycles.hom (CategoryTheory.Limits.image.ι (CategoryTheory.CategoryStruct.comp S.iCycles S.pOpcycles)) = S.homologyι
• CategoryTheory.ShortComplex.homologyIsoImageICyclesCompPOpcycles_ι_assoc 📋 Mathlib.Algebra.Homology.ShortComplex.Abelian
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex C) {Z : C} (h : S.opcycles ⟶ Z) : CategoryTheory.CategoryStruct.comp S.homologyIsoImageICyclesCompPOpcycles.hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.image.ι (CategoryTheory.CategoryStruct.comp S.iCycles S.pOpcycles)) h) = CategoryTheory.CategoryStruct.comp S.homologyι h
• CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.isoImage 📋 Mathlib.Algebra.Homology.ShortComplex.Abelian
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex C) {kf : CategoryTheory.Limits.KernelFork S.g} {cc : CategoryTheory.Limits.CokernelCofork S.f} (hkf : CategoryTheory.Limits.IsLimit kf) (hcc : CategoryTheory.Limits.IsColimit cc) {H : C} {π : kf.pt ⟶ H} {ι : H ⟶ cc.pt} (fac : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Fork.ι kf) (CategoryTheory.Limits.Cofork.π cc) = CategoryTheory.CategoryStruct.comp π ι) [CategoryTheory.Epi π] [CategoryTheory.Mono ι] : H ≅ CategoryTheory.Limits.image (CategoryTheory.CategoryStruct.comp S.iCycles S.pOpcycles)
• CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.isoImage_ι 📋 Mathlib.Algebra.Homology.ShortComplex.Abelian
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex C) {kf : CategoryTheory.Limits.KernelFork S.g} {cc : CategoryTheory.Limits.CokernelCofork S.f} (hkf : CategoryTheory.Limits.IsLimit kf) (hcc : CategoryTheory.Limits.IsColimit cc) {H : C} {π : kf.pt ⟶ H} {ι : H ⟶ cc.pt} (fac : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Fork.ι kf) (CategoryTheory.Limits.Cofork.π cc) = CategoryTheory.CategoryStruct.comp π ι) [CategoryTheory.Epi π] [CategoryTheory.Mono ι] : CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.isoImage S hkf hcc fac).hom (CategoryTheory.Limits.image.ι (CategoryTheory.CategoryStruct.comp S.iCycles S.pOpcycles)) = CategoryTheory.CategoryStruct.comp ι (S.isoOpcyclesOfIsColimit hcc).hom
• CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.isoImage_ι_assoc 📋 Mathlib.Algebra.Homology.ShortComplex.Abelian
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex C) {kf : CategoryTheory.Limits.KernelFork S.g} {cc : CategoryTheory.Limits.CokernelCofork S.f} (hkf : CategoryTheory.Limits.IsLimit kf) (hcc : CategoryTheory.Limits.IsColimit cc) {H : C} {π : kf.pt ⟶ H} {ι : H ⟶ cc.pt} (fac : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Fork.ι kf) (CategoryTheory.Limits.Cofork.π cc) = CategoryTheory.CategoryStruct.comp π ι) [CategoryTheory.Epi π] [CategoryTheory.Mono ι] {Z : C} (h : S.opcycles ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.isoImage S hkf hcc fac).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.image.ι (CategoryTheory.CategoryStruct.comp S.iCycles S.pOpcycles)) h) = CategoryTheory.CategoryStruct.comp ι (CategoryTheory.CategoryStruct.comp (S.isoOpcyclesOfIsColimit hcc).hom h)
• CategoryTheory.imageOpUnop 📋 Mathlib.CategoryTheory.Abelian.Opposite
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {X Y : C} (f : X ⟶ Y) : Opposite.unop (CategoryTheory.Limits.image f.op) ≅ CategoryTheory.Limits.image f
• CategoryTheory.imageOpOp 📋 Mathlib.CategoryTheory.Abelian.Opposite
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {X Y : C} (f : X ⟶ Y) : Opposite.op (CategoryTheory.Limits.image f) ≅ CategoryTheory.Limits.image f.op
• CategoryTheory.imageUnopUnop 📋 Mathlib.CategoryTheory.Abelian.Opposite
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {A B : Cᵒᵖ} (g : A ⟶ B) : Opposite.unop (CategoryTheory.Limits.image g) ≅ CategoryTheory.Limits.image g.unop
• CategoryTheory.imageUnopOp 📋 Mathlib.CategoryTheory.Abelian.Opposite
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {A B : Cᵒᵖ} (g : A ⟶ B) : Opposite.op (CategoryTheory.Limits.image g.unop) ≅ CategoryTheory.Limits.image g
• CategoryTheory.imageUnopOp_inv_comp_op_factorThruImage 📋 Mathlib.CategoryTheory.Abelian.Opposite
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {A B : Cᵒᵖ} (g : A ⟶ B) : CategoryTheory.CategoryStruct.comp (CategoryTheory.imageUnopOp g).inv (CategoryTheory.Limits.factorThruImage g.unop).op = CategoryTheory.Limits.image.ι g
• CategoryTheory.image_ι_op_comp_imageUnopOp_hom 📋 Mathlib.CategoryTheory.Abelian.Opposite
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {A B : Cᵒᵖ} (g : A ⟶ B) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.image.ι g.unop).op (CategoryTheory.imageUnopOp g).hom = CategoryTheory.Limits.factorThruImage g
• CategoryTheory.factorThruImage_comp_imageUnopOp_inv 📋 Mathlib.CategoryTheory.Abelian.Opposite
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {A B : Cᵒᵖ} (g : A ⟶ B) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.factorThruImage g) (CategoryTheory.imageUnopOp g).inv = (CategoryTheory.Limits.image.ι g.unop).op
• CategoryTheory.imageUnopOp_hom_comp_image_ι 📋 Mathlib.CategoryTheory.Abelian.Opposite
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {A B : Cᵒᵖ} (g : A ⟶ B) : CategoryTheory.CategoryStruct.comp (CategoryTheory.imageUnopOp g).hom (CategoryTheory.Limits.image.ι g) = (CategoryTheory.Limits.factorThruImage g.unop).op
• CategoryTheory.MonoOver.image_map 📋 Mathlib.CategoryTheory.Subobject.MonoOver
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} [CategoryTheory.Limits.HasImages C] {f g : CategoryTheory.Over X} (k : f ⟶ g) : CategoryTheory.MonoOver.image.map k = (CategoryTheory.MonoOver.forget X).preimage (CategoryTheory.Over.homMk (CategoryTheory.Limits.image.lift { I := CategoryTheory.Limits.image g.hom, m := CategoryTheory.Limits.image.ι g.hom, m_mono := ⋯, e := CategoryTheory.CategoryStruct.comp (CategoryTheory.Over.Hom.left k) (CategoryTheory.Limits.factorThruImage g.hom), fac := ⋯ }) ⋯)
• CategoryTheory.Subobject.existsIsoImage 📋 Mathlib.CategoryTheory.Subobject.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} [CategoryTheory.Limits.HasImages C] (f : X ⟶ Y) (x : CategoryTheory.Subobject X) : CategoryTheory.Subobject.underlying.obj ((CategoryTheory.Subobject.exists f).obj x) ≅ CategoryTheory.Limits.image (CategoryTheory.CategoryStruct.comp x.arrow f)
• CategoryTheory.Limits.imageSubobjectIso 📋 Mathlib.CategoryTheory.Subobject.Limits
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Limits.HasImage f] : CategoryTheory.Subobject.underlying.obj (CategoryTheory.Limits.imageSubobject f) ≅ CategoryTheory.Limits.image f
• CategoryTheory.Limits.imageSubobject_arrow' 📋 Mathlib.CategoryTheory.Subobject.Limits
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Limits.HasImage f] : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.imageSubobjectIso f).inv (CategoryTheory.Limits.imageSubobject f).arrow = CategoryTheory.Limits.image.ι f
• CategoryTheory.Limits.imageSubobject_arrow 📋 Mathlib.CategoryTheory.Subobject.Limits
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Limits.HasImage f] : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.imageSubobjectIso f).hom (CategoryTheory.Limits.image.ι f) = (CategoryTheory.Limits.imageSubobject f).arrow
• CategoryTheory.Limits.imageSubobject_arrow'_assoc 📋 Mathlib.CategoryTheory.Subobject.Limits
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Limits.HasImage f] {Z : C} (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.imageSubobjectIso f).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.imageSubobject f).arrow h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.image.ι f) h
• CategoryTheory.Limits.imageSubobject_arrow_assoc 📋 Mathlib.CategoryTheory.Subobject.Limits
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Limits.HasImage f] {Z : C} (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.imageSubobjectIso f).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.image.ι f) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.imageSubobject f).arrow h
• CategoryTheory.Limits.imageSubobjectIso_comp_image_map 📋 Mathlib.CategoryTheory.Subobject.Limits
  {C : Type u} [CategoryTheory.Category.{v, u} C] {W X Y Z : C} {f : W ⟶ X} [CategoryTheory.Limits.HasImage f] {g : Y ⟶ Z} [CategoryTheory.Limits.HasImage g] (sq : CategoryTheory.Arrow.mk f ⟶ CategoryTheory.Arrow.mk g) [CategoryTheory.Limits.HasImageMap sq] : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.imageSubobjectIso (CategoryTheory.Arrow.mk f).hom).hom (CategoryTheory.Limits.image.map sq) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.imageSubobjectMap sq) (CategoryTheory.Limits.imageSubobjectIso g).hom
• CategoryTheory.Limits.image_map_comp_imageSubobjectIso_inv 📋 Mathlib.CategoryTheory.Subobject.Limits
  {C : Type u} [CategoryTheory.Category.{v, u} C] {W X Y Z : C} {f : W ⟶ X} [CategoryTheory.Limits.HasImage f] {g : Y ⟶ Z} [CategoryTheory.Limits.HasImage g] (sq : CategoryTheory.Arrow.mk f ⟶ CategoryTheory.Arrow.mk g) [CategoryTheory.Limits.HasImageMap sq] : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.image.map sq) (CategoryTheory.Limits.imageSubobjectIso (CategoryTheory.Arrow.mk g).hom).inv = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.imageSubobjectIso f).inv (CategoryTheory.Limits.imageSubobjectMap sq)
• imageToKernel' 📋 Mathlib.Algebra.Homology.ImageToKernel
  {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {A B C : V} (f : A ⟶ B) (g : B ⟶ C) [CategoryTheory.Limits.HasKernels V] [CategoryTheory.Limits.HasImages V] (w : CategoryTheory.CategoryStruct.comp f g = 0) : CategoryTheory.Limits.image f ⟶ CategoryTheory.Limits.kernel g
• imageSubobjectIso_imageToKernel' 📋 Mathlib.Algebra.Homology.ImageToKernel
  {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {A B C : V} (f : A ⟶ B) (g : B ⟶ C) [CategoryTheory.Limits.HasKernels V] [CategoryTheory.Limits.HasImages V] (w : CategoryTheory.CategoryStruct.comp f g = 0) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.imageSubobjectIso f).hom (imageToKernel' f g w) = CategoryTheory.CategoryStruct.comp (imageToKernel f g w) (CategoryTheory.Limits.kernelSubobjectIso g).hom
• imageToKernel'_kernelSubobjectIso 📋 Mathlib.Algebra.Homology.ImageToKernel
  {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {A B C : V} (f : A ⟶ B) (g : B ⟶ C) [CategoryTheory.Limits.HasKernels V] [CategoryTheory.Limits.HasImages V] (w : CategoryTheory.CategoryStruct.comp f g = 0) : CategoryTheory.CategoryStruct.comp (imageToKernel' f g w) (CategoryTheory.Limits.kernelSubobjectIso g).inv = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.imageSubobjectIso f).inv (imageToKernel f g w)
• CategoryTheory.ShortComplex.Exact.isIso_imageToKernel' 📋 Mathlib.CategoryTheory.Abelian.Exact
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex C) (hS : S.Exact) : CategoryTheory.IsIso (imageToKernel' S.f S.g ⋯)
• CategoryTheory.ShortComplex.exact_iff_epi_imageToKernel' 📋 Mathlib.CategoryTheory.Abelian.Exact
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex C) : S.Exact ↔ CategoryTheory.Epi (imageToKernel' S.f S.g ⋯)
• CategoryTheory.ShortComplex.exact_iff_isIso_imageToKernel' 📋 Mathlib.CategoryTheory.Abelian.Exact
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex C) : S.Exact ↔ CategoryTheory.IsIso (imageToKernel' S.f S.g ⋯)
• CategoryTheory.ShortComplex.Exact.isColimitImage 📋 Mathlib.CategoryTheory.Abelian.Exact
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Abelian C] {S : CategoryTheory.ShortComplex C} (h : S.Exact) : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ (CategoryTheory.Limits.factorThruImage S.g) ⋯)
• CategoryTheory.ShortComplex.Exact.isLimitImage' 📋 Mathlib.CategoryTheory.Abelian.Exact
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Abelian C] {S : CategoryTheory.ShortComplex C} (h : S.Exact) : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.KernelFork.ofι (CategoryTheory.Limits.image.ι S.f) ⋯)
• AddCommGrpCat.imageIsoRange 📋 Mathlib.Algebra.Category.Grp.Images
  {G H : AddCommGrpCat} (f : G ⟶ H) : CategoryTheory.Limits.image f ≅ AddCommGrpCat.of ↥(AddCommGrpCat.Hom.hom f).range
• imageToKernel_unop 📋 Mathlib.Algebra.Homology.Opposite
  {V : Type u_1} [CategoryTheory.Category.{v_1, u_1} V] [CategoryTheory.Abelian V] {X Y Z : Vᵒᵖ} (f : X ⟶ Y) (g : Y ⟶ Z) (w : CategoryTheory.CategoryStruct.comp f g = 0) : imageToKernel g.unop f.unop ⋯ = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.imageSubobjectIso g.unop ≪≫ (CategoryTheory.imageUnopUnop g).symm).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.cokernel.desc f (CategoryTheory.Limits.factorThruImage g) ⋯).unop (CategoryTheory.Limits.kernelSubobjectIso f.unop ≪≫ CategoryTheory.kernelUnopUnop f).inv)
• imageToKernel_op 📋 Mathlib.Algebra.Homology.Opposite
  {V : Type u_1} [CategoryTheory.Category.{v_1, u_1} V] [CategoryTheory.Abelian V] {X Y Z : V} (f : X ⟶ Y) (g : Y ⟶ Z) (w : CategoryTheory.CategoryStruct.comp f g = 0) : imageToKernel g.op f.op ⋯ = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.imageSubobjectIso g.op ≪≫ (CategoryTheory.imageOpOp g).symm).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.cokernel.desc f (CategoryTheory.Limits.factorThruImage g) ⋯).op (CategoryTheory.Limits.kernelSubobjectIso f.op ≪≫ CategoryTheory.kernelOpOp f).inv)
• ModuleCat.imageIsoRange 📋 Mathlib.Algebra.Category.ModuleCat.Images
  {R : Type u} [Ring R] {G H : ModuleCat R} (f : G ⟶ H) : CategoryTheory.Limits.image f ≅ ModuleCat.of R ↥(ModuleCat.Hom.hom f).range
• ModuleCat.imageIsoRange_hom_subtype 📋 Mathlib.Algebra.Category.ModuleCat.Images
  {R : Type u} [Ring R] {G H : ModuleCat R} (f : G ⟶ H) : CategoryTheory.CategoryStruct.comp (ModuleCat.imageIsoRange f).hom (ModuleCat.ofHom (ModuleCat.Hom.hom f).range.subtype) = CategoryTheory.Limits.image.ι f
• ModuleCat.imageIsoRange_inv_image_ι 📋 Mathlib.Algebra.Category.ModuleCat.Images
  {R : Type u} [Ring R] {G H : ModuleCat R} (f : G ⟶ H) : CategoryTheory.CategoryStruct.comp (ModuleCat.imageIsoRange f).inv (CategoryTheory.Limits.image.ι f) = ModuleCat.ofHom (ModuleCat.Hom.hom f).range.subtype
• ModuleCat.imageIsoRange_hom_subtype_assoc 📋 Mathlib.Algebra.Category.ModuleCat.Images
  {R : Type u} [Ring R] {G H : ModuleCat R} (f : G ⟶ H) {Z : ModuleCat R} (h : ModuleCat.of R ↑H ⟶ Z) : CategoryTheory.CategoryStruct.comp (ModuleCat.imageIsoRange f).hom (CategoryTheory.CategoryStruct.comp (ModuleCat.ofHom (ModuleCat.Hom.hom f).range.subtype) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.image.ι f) h
• ModuleCat.imageIsoRange_inv_image_ι_assoc 📋 Mathlib.Algebra.Category.ModuleCat.Images
  {R : Type u} [Ring R] {G H : ModuleCat R} (f : G ⟶ H) {Z : ModuleCat R} (h : H ⟶ Z) : CategoryTheory.CategoryStruct.comp (ModuleCat.imageIsoRange f).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.image.ι f) h) = CategoryTheory.CategoryStruct.comp (ModuleCat.ofHom (ModuleCat.Hom.hom f).range.subtype) h
• ModuleCat.imageIsoRange_hom_subtype_apply 📋 Mathlib.Algebra.Category.ModuleCat.Images
  {R : Type u} [Ring R] {G H : ModuleCat R} (f : G ⟶ H) (x : ↑(CategoryTheory.Limits.image f)) : ↑((CategoryTheory.ConcreteCategory.hom (ModuleCat.imageIsoRange f).hom) x) = (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.image.ι f)) x
• ModuleCat.imageIsoRange_inv_image_ι_apply 📋 Mathlib.Algebra.Category.ModuleCat.Images
  {R : Type u} [Ring R] {G H : ModuleCat R} (f : G ⟶ H) (x : ↥(ModuleCat.Hom.hom f).range) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.image.ι f)) ((CategoryTheory.ConcreteCategory.hom (ModuleCat.imageIsoRange f).inv) x) = ↑x
• SimplexCategory.instEpiFactorThruImage 📋 Mathlib.AlgebraicTopology.SimplexCategory.Basic
  (Δ Δ' : SimplexCategory) (θ : Δ ⟶ Δ') : CategoryTheory.Epi (CategoryTheory.Limits.factorThruImage θ)
• SimplexCategory.image_eq 📋 Mathlib.AlgebraicTopology.SimplexCategory.Basic
  {Δ Δ' Δ'' : SimplexCategory} {φ : Δ ⟶ Δ''} {e : Δ ⟶ Δ'} [CategoryTheory.Epi e] {i : Δ' ⟶ Δ''} [CategoryTheory.Mono i] (fac : CategoryTheory.CategoryStruct.comp e i = φ) : CategoryTheory.Limits.image φ = Δ'
• SimplexCategory.factorThruImage_eq 📋 Mathlib.AlgebraicTopology.SimplexCategory.Basic
  {Δ Δ'' : SimplexCategory} {φ : Δ ⟶ Δ''} {e : Δ ⟶ CategoryTheory.Limits.image φ} [CategoryTheory.Epi e] {i : CategoryTheory.Limits.image φ ⟶ Δ''} [CategoryTheory.Mono i] (fac : CategoryTheory.CategoryStruct.comp e i = φ) : CategoryTheory.Limits.factorThruImage φ = e
• SimplexCategory.image_ι_eq 📋 Mathlib.AlgebraicTopology.SimplexCategory.Basic
  {Δ Δ'' : SimplexCategory} {φ : Δ ⟶ Δ''} {e : Δ ⟶ CategoryTheory.Limits.image φ} [CategoryTheory.Epi e] {i : CategoryTheory.Limits.image φ ⟶ Δ''} [CategoryTheory.Mono i] (fac : CategoryTheory.CategoryStruct.comp e i = φ) : CategoryTheory.Limits.image.ι φ = i
• AlgebraicTopology.DoldKan.Γ₀.Obj.map_on_summand₀' 📋 Mathlib.AlgebraicTopology.DoldKan.FunctorGamma
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] (K : ChainComplex C ℕ) [CategoryTheory.Limits.HasFiniteCoproducts C] {Δ Δ' : SimplexCategoryᵒᵖ} (A : CategoryTheory.SimplicialObject.Splitting.IndexSet Δ) (θ : Δ ⟶ Δ') : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι (AlgebraicTopology.DoldKan.Γ₀.Obj.summand K Δ) A) (AlgebraicTopology.DoldKan.Γ₀.Obj.map K θ) = CategoryTheory.CategoryStruct.comp (AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono K (CategoryTheory.Limits.image.ι (CategoryTheory.CategoryStruct.comp θ.unop A.e))) (CategoryTheory.Limits.Sigma.ι (AlgebraicTopology.DoldKan.Γ₀.Obj.summand K Δ') (A.pull θ))
• AlgebraicTopology.DoldKan.Γ₀.Obj.map_on_summand' 📋 Mathlib.AlgebraicTopology.DoldKan.FunctorGamma
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] (K : ChainComplex C ℕ) [CategoryTheory.Limits.HasFiniteCoproducts C] {Δ Δ' : SimplexCategoryᵒᵖ} (A : CategoryTheory.SimplicialObject.Splitting.IndexSet Δ) (θ : Δ ⟶ Δ') : CategoryTheory.CategoryStruct.comp (((AlgebraicTopology.DoldKan.Γ₀.splitting K).cofan Δ).inj A) ((AlgebraicTopology.DoldKan.Γ₀.obj K).map θ) = CategoryTheory.CategoryStruct.comp (AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono K (CategoryTheory.Limits.image.ι (CategoryTheory.CategoryStruct.comp θ.unop A.e))) (((AlgebraicTopology.DoldKan.Γ₀.splitting K).cofan Δ').inj (A.pull θ))
• AlgebraicTopology.DoldKan.Γ₀.Obj.map_on_summand'_assoc 📋 Mathlib.AlgebraicTopology.DoldKan.FunctorGamma
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] (K : ChainComplex C ℕ) [CategoryTheory.Limits.HasFiniteCoproducts C] {Δ Δ' : SimplexCategoryᵒᵖ} (A : CategoryTheory.SimplicialObject.Splitting.IndexSet Δ) (θ : Δ ⟶ Δ') {Z : C} (h : (AlgebraicTopology.DoldKan.Γ₀.obj K).obj Δ' ⟶ Z) : CategoryTheory.CategoryStruct.comp (((AlgebraicTopology.DoldKan.Γ₀.splitting K).cofan Δ).inj A) (CategoryTheory.CategoryStruct.comp ((AlgebraicTopology.DoldKan.Γ₀.obj K).map θ) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono K (CategoryTheory.Limits.image.ι (CategoryTheory.CategoryStruct.comp θ.unop A.e))) (((AlgebraicTopology.DoldKan.Γ₀.splitting K).cofan Δ').inj (A.pull θ))) h
• AlgebraicTopology.DoldKan.Γ₀.Obj.map_on_summand₀'_assoc 📋 Mathlib.AlgebraicTopology.DoldKan.FunctorGamma
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] (K : ChainComplex C ℕ) [CategoryTheory.Limits.HasFiniteCoproducts C] {Δ Δ' : SimplexCategoryᵒᵖ} (A : CategoryTheory.SimplicialObject.Splitting.IndexSet Δ) (θ : Δ ⟶ Δ') {Z : C} (h : AlgebraicTopology.DoldKan.Γ₀.Obj.obj₂ K Δ' ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι (AlgebraicTopology.DoldKan.Γ₀.Obj.summand K Δ) A) (CategoryTheory.CategoryStruct.comp (AlgebraicTopology.DoldKan.Γ₀.Obj.map K θ) h) = CategoryTheory.CategoryStruct.comp (AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono K (CategoryTheory.Limits.image.ι (CategoryTheory.CategoryStruct.comp θ.unop A.e))) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι (AlgebraicTopology.DoldKan.Γ₀.Obj.summand K Δ') (A.pull θ)) h)
• CategoryTheory.PreservesImage.iso 📋 Mathlib.CategoryTheory.Limits.Preserves.Shapes.Images
  {A : Type u₁} {B : Type u₂} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Limits.HasEqualizers A] [CategoryTheory.Limits.HasImages A] [CategoryTheory.StrongEpiCategory B] [CategoryTheory.Limits.HasImages B] (L : CategoryTheory.Functor A B) [∀ {X Y Z : A} (f : X ⟶ Z) (g : Y ⟶ Z), CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan f g) L] [∀ {X Y Z : A} (f : X ⟶ Y) (g : X ⟶ Z), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.span f g) L] {X Y : A} (f : X ⟶ Y) : CategoryTheory.Limits.image (L.map f) ≅ L.obj (CategoryTheory.Limits.image f)
• CategoryTheory.PreservesImage.factorThruImage_comp_hom 📋 Mathlib.CategoryTheory.Limits.Preserves.Shapes.Images
  {A : Type u₁} {B : Type u₂} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Limits.HasEqualizers A] [CategoryTheory.Limits.HasImages A] [CategoryTheory.StrongEpiCategory B] [CategoryTheory.Limits.HasImages B] (L : CategoryTheory.Functor A B) [∀ {X Y Z : A} (f : X ⟶ Z) (g : Y ⟶ Z), CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan f g) L] [∀ {X Y Z : A} (f : X ⟶ Y) (g : X ⟶ Z), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.span f g) L] {X Y : A} (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.factorThruImage (L.map f)) (CategoryTheory.PreservesImage.iso L f).hom = L.map (CategoryTheory.Limits.factorThruImage f)
• CategoryTheory.PreservesImage.inv_comp_image_ι_map 📋 Mathlib.CategoryTheory.Limits.Preserves.Shapes.Images
  {A : Type u₁} {B : Type u₂} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Limits.HasEqualizers A] [CategoryTheory.Limits.HasImages A] [CategoryTheory.StrongEpiCategory B] [CategoryTheory.Limits.HasImages B] (L : CategoryTheory.Functor A B) [∀ {X Y Z : A} (f : X ⟶ Z) (g : Y ⟶ Z), CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan f g) L] [∀ {X Y Z : A} (f : X ⟶ Y) (g : X ⟶ Z), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.span f g) L] {X Y : A} (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp (CategoryTheory.PreservesImage.iso L f).inv (CategoryTheory.Limits.image.ι (L.map f)) = L.map (CategoryTheory.Limits.image.ι f)
• CategoryTheory.PreservesImage.hom_comp_map_image_ι 📋 Mathlib.CategoryTheory.Limits.Preserves.Shapes.Images
  {A : Type u₁} {B : Type u₂} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Limits.HasEqualizers A] [CategoryTheory.Limits.HasImages A] [CategoryTheory.StrongEpiCategory B] [CategoryTheory.Limits.HasImages B] (L : CategoryTheory.Functor A B) [∀ {X Y Z : A} (f : X ⟶ Z) (g : Y ⟶ Z), CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan f g) L] [∀ {X Y Z : A} (f : X ⟶ Y) (g : X ⟶ Z), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.span f g) L] {X Y : A} (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp (CategoryTheory.PreservesImage.iso L f).hom (L.map (CategoryTheory.Limits.image.ι f)) = CategoryTheory.Limits.image.ι (L.map f)
• CategoryTheory.PreservesImage.factorThruImage_comp_hom_assoc 📋 Mathlib.CategoryTheory.Limits.Preserves.Shapes.Images
  {A : Type u₁} {B : Type u₂} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Limits.HasEqualizers A] [CategoryTheory.Limits.HasImages A] [CategoryTheory.StrongEpiCategory B] [CategoryTheory.Limits.HasImages B] (L : CategoryTheory.Functor A B) [∀ {X Y Z : A} (f : X ⟶ Z) (g : Y ⟶ Z), CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan f g) L] [∀ {X Y Z : A} (f : X ⟶ Y) (g : X ⟶ Z), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.span f g) L] {X Y : A} (f : X ⟶ Y) {Z : B} (h : L.obj (CategoryTheory.Limits.image f) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.factorThruImage (L.map f)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.PreservesImage.iso L f).hom h) = CategoryTheory.CategoryStruct.comp (L.map (CategoryTheory.Limits.factorThruImage f)) h
• CategoryTheory.PreservesImage.inv_comp_image_ι_map_assoc 📋 Mathlib.CategoryTheory.Limits.Preserves.Shapes.Images
  {A : Type u₁} {B : Type u₂} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Limits.HasEqualizers A] [CategoryTheory.Limits.HasImages A] [CategoryTheory.StrongEpiCategory B] [CategoryTheory.Limits.HasImages B] (L : CategoryTheory.Functor A B) [∀ {X Y Z : A} (f : X ⟶ Z) (g : Y ⟶ Z), CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan f g) L] [∀ {X Y Z : A} (f : X ⟶ Y) (g : X ⟶ Z), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.span f g) L] {X Y : A} (f : X ⟶ Y) {Z : B} (h : L.obj Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.PreservesImage.iso L f).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.image.ι (L.map f)) h) = CategoryTheory.CategoryStruct.comp (L.map (CategoryTheory.Limits.image.ι f)) h
• CategoryTheory.PreservesImage.hom_comp_map_image_ι_assoc 📋 Mathlib.CategoryTheory.Limits.Preserves.Shapes.Images
  {A : Type u₁} {B : Type u₂} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Limits.HasEqualizers A] [CategoryTheory.Limits.HasImages A] [CategoryTheory.StrongEpiCategory B] [CategoryTheory.Limits.HasImages B] (L : CategoryTheory.Functor A B) [∀ {X Y Z : A} (f : X ⟶ Z) (g : Y ⟶ Z), CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan f g) L] [∀ {X Y Z : A} (f : X ⟶ Y) (g : X ⟶ Z), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.span f g) L] {X Y : A} (f : X ⟶ Y) {Z : B} (h : L.obj Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.PreservesImage.iso L f).hom (CategoryTheory.CategoryStruct.comp (L.map (CategoryTheory.Limits.image.ι f)) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.image.ι (L.map f)) h
• CategoryTheory.PreservesImage.iso_hom 📋 Mathlib.CategoryTheory.Limits.Preserves.Shapes.Images
  {A : Type u₁} {B : Type u₂} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Limits.HasEqualizers A] [CategoryTheory.Limits.HasImages A] [CategoryTheory.StrongEpiCategory B] [CategoryTheory.Limits.HasImages B] (L : CategoryTheory.Functor A B) [∀ {X Y Z : A} (f : X ⟶ Z) (g : Y ⟶ Z), CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan f g) L] [∀ {X Y Z : A} (f : X ⟶ Y) (g : X ⟶ Z), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.span f g) L] {X Y : A} (f : X ⟶ Y) : (CategoryTheory.PreservesImage.iso L f).hom = CategoryTheory.Limits.image.lift { I := L.obj (CategoryTheory.Limits.image f), m := L.map (CategoryTheory.Limits.image.ι f), m_mono := ⋯, e := L.map (CategoryTheory.Limits.factorThruImage f), fac := ⋯ }
• CategoryTheory.PreservesImage.iso_inv 📋 Mathlib.CategoryTheory.Limits.Preserves.Shapes.Images
  {A : Type u₁} {B : Type u₂} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Limits.HasEqualizers A] [CategoryTheory.Limits.HasImages A] [CategoryTheory.StrongEpiCategory B] [CategoryTheory.Limits.HasImages B] (L : CategoryTheory.Functor A B) [∀ {X Y Z : A} (f : X ⟶ Z) (g : Y ⟶ Z), CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan f g) L] [∀ {X Y Z : A} (f : X ⟶ Y) (g : X ⟶ Z), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.span f g) L] {X Y : A} (f : X ⟶ Y) : (CategoryTheory.PreservesImage.iso L f).inv = { I := L.obj (CategoryTheory.Limits.image f), m := L.map (CategoryTheory.Limits.image.ι f), m_mono := ⋯, e := L.map (CategoryTheory.Limits.factorThruImage f), fac := ⋯, e_strong_epi := ⋯ }.toMonoIsImage.lift (CategoryTheory.Limits.Image.monoFactorisation (L.map f))

About

Loogle searches Lean and Mathlib definitions and theorems.

You can use Loogle from within the Lean4 VSCode language extension using the Loogle command from the command palette. You can also try the #loogle command from LeanSearchClient, the CLI version, the Loogle VS Code extension, the lean.nvim integration or the Zulip bot.

Usage

Loogle finds definitions and lemmas in various ways:

1. By constant:
   🔍 Real.sin
   finds all lemmas whose statement somehow mentions the sine function.

2. By lemma name substring:
   🔍 "differ"
   finds all lemmas that have "differ" somewhere in their lemma name.

3. By subexpression:
   🔍 _ * (_ ^ _)
   finds all lemmas whose statements somewhere include a product where the second argument is raised to some power.

   The pattern can also be non-linear, as in
   🔍 Real.sqrt ?a * Real.sqrt ?a

   If the pattern has parameters, they are matched in any order. Both of these will find List.map:
   🔍 (?a -> ?b) -> List ?a -> List ?b
   🔍 List ?a -> (?a -> ?b) -> List ?b

4. By main conclusion:
   🔍 |- tsum _ = _ * tsum _
   finds all lemmas where the conclusion (the subexpression to the right of all → and ∀) has the given shape.

   As before, if the pattern has parameters, they are matched against the hypotheses of the lemma in any order; for example,
   🔍 |- _ < _ → tsum _ < tsum _
   will find tsum_lt_tsum even though the hypothesis f i < g i is not the last.

5. You can filter for definitions vs theorems: Using ⊢ (_ : Type _) finds all definitions which provide data while ⊢ (_ : Prop) finds all theorems (and definitions of proofs).

If you pass more than one such search filter, separated by commas Loogle will return lemmas which match all of them. The search
🔍 Real.sin, "two", tsum, _ * _, _ ^ _, |- _ < _ → _
would find all lemmas which mention the constants Real.sin and tsum, have "two" as a substring of the lemma name, include a product and a power somewhere in the type, and have a hypothesis of the form _ < _ (if there were any such lemmas). Metavariables (?a) are assigned independently in each filter.

The #lucky button will directly send you to the documentation of the first hit.

Source code

You can find the source code for this service at https://github.com/nomeata/loogle. The https://loogle.lean-lang.org/ service is provided by the Lean FRO. Please review the Lean FRO Terms of Use and Privacy Policy.

This is Loogle revision 9f11169 serving mathlib revision ce5dd8c