Loogle!

Result

Found 150 declarations mentioning CategoryTheory.Limits.HasImage.

• CategoryTheory.Limits.HasImage 📋 Mathlib.CategoryTheory.Limits.Shapes.Images
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) : Prop
• 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.HasImages.has_image 📋 Mathlib.CategoryTheory.Limits.Shapes.Images
  {C : Type u} {inst✝ : CategoryTheory.Category.{v, u} C} [self : CategoryTheory.Limits.HasImages C] {X Y : C} (f : X ⟶ Y) : CategoryTheory.Limits.HasImage f
• CategoryTheory.Limits.HasImages.mk 📋 Mathlib.CategoryTheory.Limits.Shapes.Images
  {C : Type u} [CategoryTheory.Category.{v, u} C] (has_image : ∀ {X Y : C} (f : X ⟶ Y), CategoryTheory.Limits.HasImage f) : CategoryTheory.Limits.HasImages C
• CategoryTheory.Limits.mono_hasImage 📋 Mathlib.CategoryTheory.Limits.Shapes.Images
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Mono f] : CategoryTheory.Limits.HasImage f
• CategoryTheory.Limits.HasImage.mk 📋 Mathlib.CategoryTheory.Limits.Shapes.Images
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y} (F : CategoryTheory.Limits.ImageFactorisation f) : CategoryTheory.Limits.HasImage f
• CategoryTheory.Limits.Image.imageFactorisation 📋 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.ImageFactorisation f
• CategoryTheory.Limits.Image.monoFactorisation 📋 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.MonoFactorisation f
• CategoryTheory.Limits.HasImage.exists_image 📋 Mathlib.CategoryTheory.Limits.Shapes.Images
  {C : Type u} {inst✝ : CategoryTheory.Category.{v, u} C} {X Y : C} {f : X ⟶ Y} [self : CategoryTheory.Limits.HasImage f] : Nonempty (CategoryTheory.Limits.ImageFactorisation f)
• CategoryTheory.Limits.HasImage.mk' 📋 Mathlib.CategoryTheory.Limits.Shapes.Images
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y} (exists_image : Nonempty (CategoryTheory.Limits.ImageFactorisation f)) : CategoryTheory.Limits.HasImage f
• CategoryTheory.Limits.Image.isImage 📋 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.IsImage (CategoryTheory.Limits.Image.monoFactorisation f)
• 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.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.imageMapId 📋 Mathlib.CategoryTheory.Limits.Shapes.Images
  {C : Type u} [CategoryTheory.Category.{v, u} C] (f : CategoryTheory.Arrow C) [CategoryTheory.Limits.HasImage f.hom] : CategoryTheory.Limits.ImageMap (CategoryTheory.CategoryStruct.id f)
• CategoryTheory.Limits.inhabitedImageMap 📋 Mathlib.CategoryTheory.Limits.Shapes.Images
  {C : Type u} [CategoryTheory.Category.{v, u} C] {f : CategoryTheory.Arrow C} [CategoryTheory.Limits.HasImage f.hom] : Inhabited (CategoryTheory.Limits.ImageMap (CategoryTheory.CategoryStruct.id 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.HasImageMap 📋 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) : Prop
• CategoryTheory.Limits.ImageMap 📋 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) : Type v
• CategoryTheory.Limits.instHasImageHomMk 📋 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.HasImage (CategoryTheory.Arrow.mk f).hom
• CategoryTheory.Limits.hasImage_comp_iso 📋 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 f] [CategoryTheory.IsIso g] : CategoryTheory.Limits.HasImage (CategoryTheory.CategoryStruct.comp f g)
• CategoryTheory.Limits.hasImage_iso_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) [CategoryTheory.IsIso f] [CategoryTheory.Limits.HasImage g] : CategoryTheory.Limits.HasImage (CategoryTheory.CategoryStruct.comp f g)
• CategoryTheory.Limits.instHasImageCompOfIsIso 📋 Mathlib.CategoryTheory.Limits.Shapes.Images
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z : C} (f : X ⟶ Y) [CategoryTheory.IsIso f] (g : Y ⟶ Z) [CategoryTheory.Limits.HasImage g] : CategoryTheory.Limits.HasImage (CategoryTheory.CategoryStruct.comp f g)
• 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.instSubsingletonImageMap 📋 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) : Subsingleton (CategoryTheory.Limits.ImageMap sq)
• CategoryTheory.Limits.HasImage.of_arrow_iso 📋 Mathlib.CategoryTheory.Limits.Shapes.Images
  {C : Type u} [CategoryTheory.Category.{v, u} C] {f g : CategoryTheory.Arrow C} [h : CategoryTheory.Limits.HasImage f.hom] (sq : f ⟶ g) [CategoryTheory.IsIso sq] : CategoryTheory.Limits.HasImage g.hom
• 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.as_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.Limits.Image.monoFactorisation f).e = CategoryTheory.Limits.factorThruImage 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.as_ι 📋 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.monoFactorisation f).m = CategoryTheory.Limits.image.ι f
• CategoryTheory.Limits.HasImageMap.imageMap 📋 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.ImageMap sq
• CategoryTheory.Limits.HasImageMap.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} (m : CategoryTheory.Limits.ImageMap sq) : CategoryTheory.Limits.HasImageMap sq
• 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.HasImageMap.has_image_map 📋 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} [self : CategoryTheory.Limits.HasImageMap sq] : Nonempty (CategoryTheory.Limits.ImageMap sq)
• CategoryTheory.Limits.HasImageMap.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} (has_image_map : Nonempty (CategoryTheory.Limits.ImageMap sq)) : CategoryTheory.Limits.HasImageMap sq
• CategoryTheory.Limits.hasImageMapOfIsIso 📋 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.IsIso sq] : CategoryTheory.Limits.HasImageMap sq
• 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.isImage_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.isImage f).lift F = CategoryTheory.Limits.image.lift F
• 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.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.IsImage.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} (hF : CategoryTheory.Limits.IsImage F) : CategoryTheory.CategoryStruct.comp (hF.lift (CategoryTheory.Limits.Image.monoFactorisation f)) (CategoryTheory.Limits.image.ι f) = F.m
• CategoryTheory.Limits.imageMapComp 📋 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.ImageMap (CategoryTheory.CategoryStruct.comp sq sq')
• CategoryTheory.Limits.HasImageMap.comp 📋 Mathlib.CategoryTheory.Limits.Shapes.Images
  {C : Type u} [CategoryTheory.Category.{v, u} C] {f g h : CategoryTheory.Arrow C} [CategoryTheory.Limits.HasImage f.hom] [CategoryTheory.Limits.HasImage g.hom] [CategoryTheory.Limits.HasImage h.hom] (sq1 : f ⟶ g) (sq2 : g ⟶ h) [CategoryTheory.Limits.HasImageMap sq1] [CategoryTheory.Limits.HasImageMap sq2] : CategoryTheory.Limits.HasImageMap (CategoryTheory.CategoryStruct.comp sq1 sq2)
• 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.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.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.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.IsImage.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} (hF : CategoryTheory.Limits.IsImage F) {Z : C} (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (hF.lift (CategoryTheory.Limits.Image.monoFactorisation f)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.image.ι f) h) = CategoryTheory.CategoryStruct.comp F.m h
• 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.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.HasImageMap.transport 📋 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 : CategoryTheory.Limits.MonoFactorisation f.hom) {F' : CategoryTheory.Limits.MonoFactorisation g.hom} (hF' : CategoryTheory.Limits.IsImage F') (map : F.I ⟶ F'.I) (map_ι : CategoryTheory.CategoryStruct.comp map F'.m = CategoryTheory.CategoryStruct.comp F.m (CategoryTheory.Arrow.Hom.right sq)) : CategoryTheory.Limits.HasImageMap sq
• CategoryTheory.Limits.ImageMap.transport 📋 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 : CategoryTheory.Limits.MonoFactorisation f.hom) {F' : CategoryTheory.Limits.MonoFactorisation g.hom} (hF' : CategoryTheory.Limits.IsImage F') {map : F.I ⟶ F'.I} (map_ι : CategoryTheory.CategoryStruct.comp map F'.m = CategoryTheory.CategoryStruct.comp F.m (CategoryTheory.Arrow.Hom.right sq)) : CategoryTheory.Limits.ImageMap sq
• 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.hasImage_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.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.Limits.Types.instHasImage 📋 Mathlib.CategoryTheory.Limits.Types.Images
  {α β : Type u} (f : α ⟶ β) : CategoryTheory.Limits.HasImage f
• CategoryTheory.MonoOver.imageMonoOver 📋 Mathlib.CategoryTheory.Subobject.MonoOver
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Limits.HasImage f] : CategoryTheory.MonoOver Y
• CategoryTheory.MonoOver.imageMonoOver_arrow 📋 Mathlib.CategoryTheory.Subobject.MonoOver
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Limits.HasImage f] : (CategoryTheory.MonoOver.imageMonoOver f).arrow = CategoryTheory.Limits.image.ι f
• CategoryTheory.Limits.imageSubobject 📋 Mathlib.CategoryTheory.Subobject.Limits
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Limits.HasImage f] : CategoryTheory.Subobject Y
• CategoryTheory.Limits.imageSubobject_factors_comp_self 📋 Mathlib.CategoryTheory.Subobject.Limits
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Limits.HasImage f] {W : C} (k : W ⟶ X) : (CategoryTheory.Limits.imageSubobject f).Factors (CategoryTheory.CategoryStruct.comp k f)
• CategoryTheory.Limits.factorThruImageSubobject 📋 Mathlib.CategoryTheory.Subobject.Limits
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Limits.HasImage f] : X ⟶ CategoryTheory.Subobject.underlying.obj (CategoryTheory.Limits.imageSubobject 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.instEpiFactorThruImageSubobjectOfHasEqualizers 📋 Mathlib.CategoryTheory.Subobject.Limits
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Limits.HasImage f] [CategoryTheory.Limits.HasEqualizers C] : CategoryTheory.Epi (CategoryTheory.Limits.factorThruImageSubobject f)
• CategoryTheory.Limits.imageSubobject_iso_comp 📋 Mathlib.CategoryTheory.Subobject.Limits
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} [CategoryTheory.Limits.HasEqualizers C] {X' : C} (h : X' ⟶ X) [CategoryTheory.IsIso h] (f : X ⟶ Y) [CategoryTheory.Limits.HasImage f] : CategoryTheory.Limits.imageSubobject (CategoryTheory.CategoryStruct.comp h f) = CategoryTheory.Limits.imageSubobject f
• CategoryTheory.Limits.imageSubobject_comp_le 📋 Mathlib.CategoryTheory.Subobject.Limits
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y X' : C} (h : X' ⟶ X) (f : X ⟶ Y) [CategoryTheory.Limits.HasImage f] [CategoryTheory.Limits.HasImage (CategoryTheory.CategoryStruct.comp h f)] : CategoryTheory.Limits.imageSubobject (CategoryTheory.CategoryStruct.comp h f) ≤ CategoryTheory.Limits.imageSubobject f
• CategoryTheory.Limits.imageSubobject_arrow_comp 📋 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.factorThruImageSubobject f) (CategoryTheory.Limits.imageSubobject f).arrow = f
• CategoryTheory.Limits.imageSubobject_le_mk 📋 Mathlib.CategoryTheory.Subobject.Limits
  {C : Type u} [CategoryTheory.Category.{v, u} C] {A B X : C} (g : X ⟶ B) [CategoryTheory.Mono g] (f : A ⟶ B) [CategoryTheory.Limits.HasImage f] (h : A ⟶ X) (w : CategoryTheory.CategoryStruct.comp h g = f) : CategoryTheory.Limits.imageSubobject f ≤ CategoryTheory.Subobject.mk g
• CategoryTheory.Limits.imageSubobjectCompIso 📋 Mathlib.CategoryTheory.Subobject.Limits
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} [CategoryTheory.Limits.HasEqualizers C] (f : X ⟶ Y) [CategoryTheory.Limits.HasImage f] {Y' : C} (h : Y ⟶ Y') [CategoryTheory.IsIso h] : CategoryTheory.Subobject.underlying.obj (CategoryTheory.Limits.imageSubobject (CategoryTheory.CategoryStruct.comp f h)) ≅ CategoryTheory.Subobject.underlying.obj (CategoryTheory.Limits.imageSubobject f)
• CategoryTheory.Limits.imageSubobject_le 📋 Mathlib.CategoryTheory.Subobject.Limits
  {C : Type u} [CategoryTheory.Category.{v, u} C] {A B : C} {X : CategoryTheory.Subobject B} (f : A ⟶ B) [CategoryTheory.Limits.HasImage f] (h : A ⟶ CategoryTheory.Subobject.underlying.obj X) (w : CategoryTheory.CategoryStruct.comp h X.arrow = f) : CategoryTheory.Limits.imageSubobject f ≤ X
• CategoryTheory.Limits.imageSubobject_arrow_comp_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.factorThruImageSubobject f) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.imageSubobject f).arrow h) = CategoryTheory.CategoryStruct.comp f h
• 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.imageSubobjectMap 📋 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.Subobject.underlying.obj (CategoryTheory.Limits.imageSubobject f) ⟶ CategoryTheory.Subobject.underlying.obj (CategoryTheory.Limits.imageSubobject g)
• CategoryTheory.Limits.factorThruImageSubobject_comp_self 📋 Mathlib.CategoryTheory.Subobject.Limits
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Limits.HasImage f] {W : C} (k : W ⟶ X) (h : (CategoryTheory.Limits.imageSubobject f).Factors (CategoryTheory.CategoryStruct.comp k f)) : (CategoryTheory.Limits.imageSubobject f).factorThru (CategoryTheory.CategoryStruct.comp k f) h = CategoryTheory.CategoryStruct.comp k (CategoryTheory.Limits.factorThruImageSubobject f)
• CategoryTheory.Limits.imageSubobject_comp_le_epi_of_epi 📋 Mathlib.CategoryTheory.Subobject.Limits
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} [CategoryTheory.Limits.HasEqualizers C] {X' : C} (h : X' ⟶ X) [CategoryTheory.Epi h] (f : X ⟶ Y) [CategoryTheory.Limits.HasImage f] [CategoryTheory.Limits.HasImage (CategoryTheory.CategoryStruct.comp h f)] : CategoryTheory.Epi ((CategoryTheory.Limits.imageSubobject (CategoryTheory.CategoryStruct.comp h f)).ofLE (CategoryTheory.Limits.imageSubobject 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.factorThruImageSubobject_comp_self_assoc 📋 Mathlib.CategoryTheory.Subobject.Limits
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Limits.HasImage f] {W W' : C} (k : W ⟶ W') (k' : W' ⟶ X) (h : (CategoryTheory.Limits.imageSubobject f).Factors (CategoryTheory.CategoryStruct.comp k (CategoryTheory.CategoryStruct.comp k' f))) : (CategoryTheory.Limits.imageSubobject f).factorThru (CategoryTheory.CategoryStruct.comp k (CategoryTheory.CategoryStruct.comp k' f)) h = CategoryTheory.CategoryStruct.comp k (CategoryTheory.CategoryStruct.comp k' (CategoryTheory.Limits.factorThruImageSubobject f))
• 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.imageSubobjectMap_arrow 📋 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.imageSubobjectMap sq) (CategoryTheory.Limits.imageSubobject g).arrow = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.imageSubobject f).arrow (CategoryTheory.Arrow.Hom.right sq)
• CategoryTheory.Limits.imageSubobject_arrow_comp_eq_zero 📋 Mathlib.CategoryTheory.Subobject.Limits
  {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.factorThruImageSubobject f)] (h : CategoryTheory.CategoryStruct.comp f g = 0) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.imageSubobject f).arrow g = 0
• CategoryTheory.Limits.imageSubobjectCompIso_inv_arrow 📋 Mathlib.CategoryTheory.Subobject.Limits
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} [CategoryTheory.Limits.HasEqualizers C] (f : X ⟶ Y) [CategoryTheory.Limits.HasImage f] {Y' : C} (h : Y ⟶ Y') [CategoryTheory.IsIso h] : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.imageSubobjectCompIso f h).inv (CategoryTheory.Limits.imageSubobject (CategoryTheory.CategoryStruct.comp f h)).arrow = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.imageSubobject f).arrow h
• CategoryTheory.Limits.imageSubobjectMap_arrow_assoc 📋 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] {Z✝ : C} (h : Z ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.imageSubobjectMap sq) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.imageSubobject g).arrow h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.imageSubobject f).arrow (CategoryTheory.CategoryStruct.comp (CategoryTheory.Arrow.Hom.right sq) h)
• CategoryTheory.Limits.imageSubobjectCompIso_hom_arrow 📋 Mathlib.CategoryTheory.Subobject.Limits
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} [CategoryTheory.Limits.HasEqualizers C] (f : X ⟶ Y) [CategoryTheory.Limits.HasImage f] {Y' : C} (h : Y ⟶ Y') [CategoryTheory.IsIso h] : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.imageSubobjectCompIso f h).hom (CategoryTheory.Limits.imageSubobject f).arrow = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.imageSubobject (CategoryTheory.CategoryStruct.comp f h)).arrow (CategoryTheory.inv h)
• CategoryTheory.Limits.imageSubobject_arrow_comp_apply 📋 Mathlib.CategoryTheory.Subobject.Limits
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Limits.HasImage f] {F : C → C → Type uF} {carrier : C → Type w} {instFunLike : (X Y : C) → FunLike (F X Y) (carrier X) (carrier Y)} [inst : CategoryTheory.ConcreteCategory C F] (x : carrier X) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.imageSubobject f).arrow) ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.factorThruImageSubobject f)) x) = (CategoryTheory.ConcreteCategory.hom f) x
• CategoryTheory.Limits.imageSubobjectCompIso_inv_arrow_assoc 📋 Mathlib.CategoryTheory.Subobject.Limits
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} [CategoryTheory.Limits.HasEqualizers C] (f : X ⟶ Y) [CategoryTheory.Limits.HasImage f] {Y' : C} (h : Y ⟶ Y') [CategoryTheory.IsIso h] {Z : C} (h✝ : Y' ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.imageSubobjectCompIso f h).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.imageSubobject (CategoryTheory.CategoryStruct.comp f h)).arrow h✝) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.imageSubobject f).arrow (CategoryTheory.CategoryStruct.comp h h✝)
• CategoryTheory.Limits.imageSubobjectCompIso_hom_arrow_assoc 📋 Mathlib.CategoryTheory.Subobject.Limits
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} [CategoryTheory.Limits.HasEqualizers C] (f : X ⟶ Y) [CategoryTheory.Limits.HasImage f] {Y' : C} (h : Y ⟶ Y') [CategoryTheory.IsIso h] {Z : C} (h✝ : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.imageSubobjectCompIso f h).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.imageSubobject f).arrow h✝) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.imageSubobject (CategoryTheory.CategoryStruct.comp f h)).arrow (CategoryTheory.CategoryStruct.comp (CategoryTheory.inv h) 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)
• image_le_kernel 📋 Mathlib.Algebra.Homology.ImageToKernel
  {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {A B C : V} (f : A ⟶ B) [CategoryTheory.Limits.HasImage f] (g : B ⟶ C) [CategoryTheory.Limits.HasKernel g] (w : CategoryTheory.CategoryStruct.comp f g = 0) : CategoryTheory.Limits.imageSubobject f ≤ CategoryTheory.Limits.kernelSubobject g
• imageToKernel 📋 Mathlib.Algebra.Homology.ImageToKernel
  {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {A B C : V} (f : A ⟶ B) [CategoryTheory.Limits.HasImage f] (g : B ⟶ C) [CategoryTheory.Limits.HasKernel g] (w : CategoryTheory.CategoryStruct.comp f g = 0) : CategoryTheory.Subobject.underlying.obj (CategoryTheory.Limits.imageSubobject f) ⟶ CategoryTheory.Subobject.underlying.obj (CategoryTheory.Limits.kernelSubobject g)
• instMonoImageToKernel 📋 Mathlib.Algebra.Homology.ImageToKernel
  {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {A B C : V} (f : A ⟶ B) [CategoryTheory.Limits.HasImage f] (g : B ⟶ C) [CategoryTheory.Limits.HasKernel g] (w : CategoryTheory.CategoryStruct.comp f g = 0) : CategoryTheory.Mono (imageToKernel f g w)
• subobject_ofLE_as_imageToKernel 📋 Mathlib.Algebra.Homology.ImageToKernel
  {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {A B C : V} (f : A ⟶ B) [CategoryTheory.Limits.HasImage f] (g : B ⟶ C) [CategoryTheory.Limits.HasKernel g] (w : CategoryTheory.CategoryStruct.comp f g = 0) (h : CategoryTheory.Limits.imageSubobject f ≤ CategoryTheory.Limits.kernelSubobject g) : (CategoryTheory.Limits.imageSubobject f).ofLE (CategoryTheory.Limits.kernelSubobject g) h = imageToKernel f g w
• factorThruImageSubobject_comp_imageToKernel 📋 Mathlib.Algebra.Homology.ImageToKernel
  {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {A B C : V} (f : A ⟶ B) [CategoryTheory.Limits.HasImage f] (g : B ⟶ C) [CategoryTheory.Limits.HasKernel g] (w : CategoryTheory.CategoryStruct.comp f g = 0) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.factorThruImageSubobject f) (imageToKernel f g w) = CategoryTheory.Limits.factorThruKernelSubobject g f w
• imageToKernel_arrow 📋 Mathlib.Algebra.Homology.ImageToKernel
  {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {A B C : V} (f : A ⟶ B) [CategoryTheory.Limits.HasImage f] (g : B ⟶ C) [CategoryTheory.Limits.HasKernel g] (w : CategoryTheory.CategoryStruct.comp f g = 0) : CategoryTheory.CategoryStruct.comp (imageToKernel f g w) (CategoryTheory.Limits.kernelSubobject g).arrow = (CategoryTheory.Limits.imageSubobject f).arrow
• imageToKernel_arrow_assoc 📋 Mathlib.Algebra.Homology.ImageToKernel
  {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {A B C : V} (f : A ⟶ B) [CategoryTheory.Limits.HasImage f] (g : B ⟶ C) [CategoryTheory.Limits.HasKernel g] (w : CategoryTheory.CategoryStruct.comp f g = 0) {Z : V} (h : B ⟶ Z) : CategoryTheory.CategoryStruct.comp (imageToKernel f g w) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernelSubobject g).arrow h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.imageSubobject f).arrow h
• imageToKernel_arrow_apply 📋 Mathlib.Algebra.Homology.ImageToKernel
  {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {A B C : V} (f : A ⟶ B) [CategoryTheory.Limits.HasImage f] (g : B ⟶ C) [CategoryTheory.Limits.HasKernel g] (w : CategoryTheory.CategoryStruct.comp f g = 0) {F : V → V → Type uF} {carrier : V → Type w} {instFunLike : (X Y : V) → FunLike (F X Y) (carrier X) (carrier Y)} [inst : CategoryTheory.ConcreteCategory V F] (x : carrier (CategoryTheory.Subobject.underlying.obj (CategoryTheory.Limits.imageSubobject f))) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.kernelSubobject g).arrow) ((CategoryTheory.ConcreteCategory.hom (imageToKernel f g w)) x) = (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.imageSubobject f).arrow) x
• ModuleCat.cokernel_π_imageSubobject_ext 📋 Mathlib.Algebra.Category.ModuleCat.Subobject
  {R : Type u} [Ring R] {L M N : ModuleCat R} (f : L ⟶ M) [CategoryTheory.Limits.HasImage f] (g : CategoryTheory.Subobject.underlying.obj (CategoryTheory.Limits.imageSubobject f) ⟶ N) [CategoryTheory.Limits.HasCokernel g] {x y : ↑N} (l : ↑L) (w : x = y + (CategoryTheory.ConcreteCategory.hom g) ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.factorThruImageSubobject f)) l)) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.cokernel.π g)) x = (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.cokernel.π g)) y
• CategoryTheory.epi_of_nonzero_to_simple 📋 Mathlib.CategoryTheory.Simple
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasEqualizers C] {X Y : C} [CategoryTheory.Simple Y] {f : X ⟶ Y} [CategoryTheory.Limits.HasImage f] (w : f ≠ 0) : CategoryTheory.Epi 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