Loogle!

Result

Found 97 declarations mentioning CategoryTheory.Limits.MonoFactorisation.I.

• CategoryTheory.Limits.MonoFactorisation.I 📋 Mathlib.CategoryTheory.Limits.Shapes.Images
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y} (self : CategoryTheory.Limits.MonoFactorisation f) : C
• CategoryTheory.Limits.MonoFactorisation.e 📋 Mathlib.CategoryTheory.Limits.Shapes.Images
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y} (self : CategoryTheory.Limits.MonoFactorisation f) : X ⟶ self.I
• CategoryTheory.Limits.MonoFactorisation.m 📋 Mathlib.CategoryTheory.Limits.Shapes.Images
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y} (self : CategoryTheory.Limits.MonoFactorisation f) : self.I ⟶ Y
• CategoryTheory.Limits.MonoFactorisation.m_mono 📋 Mathlib.CategoryTheory.Limits.Shapes.Images
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y} (self : CategoryTheory.Limits.MonoFactorisation f) : CategoryTheory.Mono self.m
• CategoryTheory.Limits.MonoFactorisation.ofIsoI 📋 Mathlib.CategoryTheory.Limits.Shapes.Images
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y} (F : CategoryTheory.Limits.MonoFactorisation f) {I' : C} (e : F.I ≅ I') : CategoryTheory.Limits.MonoFactorisation f
• CategoryTheory.Limits.ImageFactorisation.ofIsoI 📋 Mathlib.CategoryTheory.Limits.Shapes.Images
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y} (F : CategoryTheory.Limits.ImageFactorisation f) {I' : C} (e : F.F.I ≅ I') : CategoryTheory.Limits.ImageFactorisation f
• CategoryTheory.Limits.StrongEpiMonoFactorisation.mk 📋 Mathlib.CategoryTheory.Limits.Shapes.Images
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y} (toMonoFactorisation : CategoryTheory.Limits.MonoFactorisation f) [e_strong_epi : CategoryTheory.StrongEpi toMonoFactorisation.e] : CategoryTheory.Limits.StrongEpiMonoFactorisation 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.MonoFactorisation.ofIsoI_I 📋 Mathlib.CategoryTheory.Limits.Shapes.Images
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y} (F : CategoryTheory.Limits.MonoFactorisation f) {I' : C} (e : F.I ≅ I') : (F.ofIsoI e).I = I'
• CategoryTheory.Limits.StrongEpiMonoFactorisation.e_strong_epi 📋 Mathlib.CategoryTheory.Limits.Shapes.Images
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y} (self : CategoryTheory.Limits.StrongEpiMonoFactorisation f) : CategoryTheory.StrongEpi self.e
• CategoryTheory.Limits.strongEpi_of_strongEpiMonoFactorisation 📋 Mathlib.CategoryTheory.Limits.Shapes.Images
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y} (F : CategoryTheory.Limits.StrongEpiMonoFactorisation f) {F' : CategoryTheory.Limits.MonoFactorisation f} (hF' : CategoryTheory.Limits.IsImage F') : CategoryTheory.StrongEpi F'.e
• 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.IsImage.lift 📋 Mathlib.CategoryTheory.Limits.Shapes.Images
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y} {F : CategoryTheory.Limits.MonoFactorisation f} (self : CategoryTheory.Limits.IsImage F) (F' : CategoryTheory.Limits.MonoFactorisation f) : F.I ⟶ F'.I
• CategoryTheory.Limits.IsImage.ofIsoI 📋 Mathlib.CategoryTheory.Limits.Shapes.Images
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y} {F : CategoryTheory.Limits.MonoFactorisation f} (hF : CategoryTheory.Limits.IsImage F) {I' : C} (e : F.I ≅ I') : CategoryTheory.Limits.IsImage (F.ofIsoI e)
• CategoryTheory.Limits.IsImage.isoExt 📋 Mathlib.CategoryTheory.Limits.Shapes.Images
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y} {F F' : CategoryTheory.Limits.MonoFactorisation f} (hF : CategoryTheory.Limits.IsImage F) (hF' : CategoryTheory.Limits.IsImage F') : F.I ≅ F'.I
• CategoryTheory.Limits.MonoFactorisation.fac 📋 Mathlib.CategoryTheory.Limits.Shapes.Images
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y} (self : CategoryTheory.Limits.MonoFactorisation f) : CategoryTheory.CategoryStruct.comp self.e self.m = 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.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.MonoFactorisation.isoComp_I 📋 Mathlib.CategoryTheory.Limits.Shapes.Images
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y} (F : CategoryTheory.Limits.MonoFactorisation f) {X' : C} (g : X' ⟶ X) : (F.isoComp g).I = F.I
• CategoryTheory.Limits.IsImage.self_lift 📋 Mathlib.CategoryTheory.Limits.Shapes.Images
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Mono f] (F' : CategoryTheory.Limits.MonoFactorisation f) : (CategoryTheory.Limits.IsImage.self f).lift F' = F'.e
• CategoryTheory.Limits.MonoFactorisation.compMono_I 📋 Mathlib.CategoryTheory.Limits.Shapes.Images
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y} (F : CategoryTheory.Limits.MonoFactorisation f) {Y' : C} (g : Y ⟶ Y') [CategoryTheory.Mono g] : (F.compMono g).I = F.I
• CategoryTheory.Limits.ImageFactorisation.ofIsoI_F 📋 Mathlib.CategoryTheory.Limits.Shapes.Images
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y} (F : CategoryTheory.Limits.ImageFactorisation f) {I' : C} (e : F.F.I ≅ I') : (F.ofIsoI e).F = F.F.ofIsoI e
• CategoryTheory.Limits.MonoFactorisation.isoComp_m 📋 Mathlib.CategoryTheory.Limits.Shapes.Images
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y} (F : CategoryTheory.Limits.MonoFactorisation f) {X' : C} (g : X' ⟶ X) : (F.isoComp g).m = F.m
• CategoryTheory.Limits.MonoFactorisation.ofCompIso_I 📋 Mathlib.CategoryTheory.Limits.Shapes.Images
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y} {Y' : C} {g : Y ⟶ Y'} [CategoryTheory.IsIso g] (F : CategoryTheory.Limits.MonoFactorisation (CategoryTheory.CategoryStruct.comp f g)) : F.ofCompIso.I = F.I
• CategoryTheory.Limits.MonoFactorisation.ofIsoComp_I 📋 Mathlib.CategoryTheory.Limits.Shapes.Images
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y} {X' : C} (g : X' ⟶ X) [CategoryTheory.IsIso g] (F : CategoryTheory.Limits.MonoFactorisation (CategoryTheory.CategoryStruct.comp g f)) : (CategoryTheory.Limits.MonoFactorisation.ofIsoComp g F).I = F.I
• 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.MonoFactorisation.compMono_e 📋 Mathlib.CategoryTheory.Limits.Shapes.Images
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y} (F : CategoryTheory.Limits.MonoFactorisation f) {Y' : C} (g : Y ⟶ Y') [CategoryTheory.Mono g] : (F.compMono g).e = F.e
• CategoryTheory.Limits.MonoFactorisation.ofArrowIso_I 📋 Mathlib.CategoryTheory.Limits.Shapes.Images
  {C : Type u} [CategoryTheory.Category.{v, u} C] {f g : CategoryTheory.Arrow C} (F : CategoryTheory.Limits.MonoFactorisation f.hom) (sq : f ⟶ g) [CategoryTheory.IsIso sq] : (F.ofArrowIso sq).I = F.I
• 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.MonoFactorisation.ofIsoI_e 📋 Mathlib.CategoryTheory.Limits.Shapes.Images
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y} (F : CategoryTheory.Limits.MonoFactorisation f) {I' : C} (e : F.I ≅ I') : (F.ofIsoI e).e = CategoryTheory.CategoryStruct.comp F.e e.hom
• CategoryTheory.Limits.MonoFactorisation.ofIsoI_m 📋 Mathlib.CategoryTheory.Limits.Shapes.Images
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y} (F : CategoryTheory.Limits.MonoFactorisation f) {I' : C} (e : F.I ≅ I') : (F.ofIsoI e).m = CategoryTheory.CategoryStruct.comp e.inv F.m
• CategoryTheory.Limits.IsImage.fac_lift 📋 Mathlib.CategoryTheory.Limits.Shapes.Images
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y} {F : CategoryTheory.Limits.MonoFactorisation f} (hF : CategoryTheory.Limits.IsImage F) (F' : CategoryTheory.Limits.MonoFactorisation f) : CategoryTheory.CategoryStruct.comp F.e (hF.lift F') = F'.e
• CategoryTheory.Limits.IsImage.lift_fac 📋 Mathlib.CategoryTheory.Limits.Shapes.Images
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y} {F : CategoryTheory.Limits.MonoFactorisation f} (self : CategoryTheory.Limits.IsImage F) (F' : CategoryTheory.Limits.MonoFactorisation f) : CategoryTheory.CategoryStruct.comp (self.lift F') F'.m = F.m
• CategoryTheory.Limits.MonoFactorisation.isoComp_e 📋 Mathlib.CategoryTheory.Limits.Shapes.Images
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y} (F : CategoryTheory.Limits.MonoFactorisation f) {X' : C} (g : X' ⟶ X) : (F.isoComp g).e = CategoryTheory.CategoryStruct.comp g F.e
• CategoryTheory.Limits.MonoFactorisation.fac_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.Images
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y} (self : CategoryTheory.Limits.MonoFactorisation f) {Z : C} (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp self.e (CategoryTheory.CategoryStruct.comp self.m h) = CategoryTheory.CategoryStruct.comp f h
• CategoryTheory.Limits.ImageFactorisation.ofIsoI_isImage 📋 Mathlib.CategoryTheory.Limits.Shapes.Images
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y} (F : CategoryTheory.Limits.ImageFactorisation f) {I' : C} (e : F.F.I ≅ I') : (F.ofIsoI e).isImage = F.isImage.ofIsoI e
• CategoryTheory.Limits.IsImage.isoExt_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.Images
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y} {F F' : CategoryTheory.Limits.MonoFactorisation f} (hF : CategoryTheory.Limits.IsImage F) (hF' : CategoryTheory.Limits.IsImage F') : (hF.isoExt hF').hom = hF.lift F'
• CategoryTheory.Limits.IsImage.isoExt_inv 📋 Mathlib.CategoryTheory.Limits.Shapes.Images
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y} {F F' : CategoryTheory.Limits.MonoFactorisation f} (hF : CategoryTheory.Limits.IsImage F) (hF' : CategoryTheory.Limits.IsImage F') : (hF.isoExt hF').inv = hF'.lift F
• CategoryTheory.Limits.MonoFactorisation.compMono_m 📋 Mathlib.CategoryTheory.Limits.Shapes.Images
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y} (F : CategoryTheory.Limits.MonoFactorisation f) {Y' : C} (g : Y ⟶ Y') [CategoryTheory.Mono g] : (F.compMono g).m = CategoryTheory.CategoryStruct.comp F.m g
• CategoryTheory.Limits.MonoFactorisation.ofCompIso_e 📋 Mathlib.CategoryTheory.Limits.Shapes.Images
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y} {Y' : C} {g : Y ⟶ Y'} [CategoryTheory.IsIso g] (F : CategoryTheory.Limits.MonoFactorisation (CategoryTheory.CategoryStruct.comp f g)) : F.ofCompIso.e = F.e
• CategoryTheory.Limits.MonoFactorisation.ofIsoComp_m 📋 Mathlib.CategoryTheory.Limits.Shapes.Images
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y} {X' : C} (g : X' ⟶ X) [CategoryTheory.IsIso g] (F : CategoryTheory.Limits.MonoFactorisation (CategoryTheory.CategoryStruct.comp g f)) : (CategoryTheory.Limits.MonoFactorisation.ofIsoComp g F).m = F.m
• 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.MonoFactorisation.copy 📋 Mathlib.CategoryTheory.Limits.Shapes.Images
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y} (F : CategoryTheory.Limits.MonoFactorisation f) (m : F.I ⟶ Y) (e : X ⟶ F.I) (hm : m = F.m := by cat_disch) (he : e = F.e := by cat_disch) : CategoryTheory.Limits.MonoFactorisation f
• CategoryTheory.Limits.IsImage.mk 📋 Mathlib.CategoryTheory.Limits.Shapes.Images
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y} {F : CategoryTheory.Limits.MonoFactorisation f} (lift : (F' : CategoryTheory.Limits.MonoFactorisation f) → F.I ⟶ F'.I) (lift_fac : ∀ (F' : CategoryTheory.Limits.MonoFactorisation f), CategoryTheory.CategoryStruct.comp (lift F') F'.m = F.m := by cat_disch) : CategoryTheory.Limits.IsImage F
• CategoryTheory.Limits.IsImage.e_isoExt_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.Images
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y} {F F' : CategoryTheory.Limits.MonoFactorisation f} (hF : CategoryTheory.Limits.IsImage F) (hF' : CategoryTheory.Limits.IsImage F') : CategoryTheory.CategoryStruct.comp F.e (hF.isoExt hF').hom = F'.e
• CategoryTheory.Limits.IsImage.e_isoExt_inv 📋 Mathlib.CategoryTheory.Limits.Shapes.Images
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y} {F F' : CategoryTheory.Limits.MonoFactorisation f} (hF : CategoryTheory.Limits.IsImage F) (hF' : CategoryTheory.Limits.IsImage F') : CategoryTheory.CategoryStruct.comp F'.e (hF.isoExt hF').inv = F.e
• CategoryTheory.Limits.IsImage.isoExt_hom_m 📋 Mathlib.CategoryTheory.Limits.Shapes.Images
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y} {F F' : CategoryTheory.Limits.MonoFactorisation f} (hF : CategoryTheory.Limits.IsImage F) (hF' : CategoryTheory.Limits.IsImage F') : CategoryTheory.CategoryStruct.comp (hF.isoExt hF').hom F'.m = F.m
• CategoryTheory.Limits.IsImage.isoExt_inv_m 📋 Mathlib.CategoryTheory.Limits.Shapes.Images
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y} {F F' : CategoryTheory.Limits.MonoFactorisation f} (hF : CategoryTheory.Limits.IsImage F) (hF' : CategoryTheory.Limits.IsImage F') : CategoryTheory.CategoryStruct.comp (hF.isoExt hF').inv F.m = F'.m
• CategoryTheory.Limits.MonoFactorisation.ext 📋 Mathlib.CategoryTheory.Limits.Shapes.Images
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y} {F F' : CategoryTheory.Limits.MonoFactorisation f} (hI : F.I = F'.I) (hm : F.m = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom hI) F'.m) : F = F'
• 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.MonoFactorisation.copy_I 📋 Mathlib.CategoryTheory.Limits.Shapes.Images
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y} (F : CategoryTheory.Limits.MonoFactorisation f) (m : F.I ⟶ Y) (e : X ⟶ F.I) (hm : m = F.m := by cat_disch) (he : e = F.e := by cat_disch) : (F.copy m e hm he).I = F.I
• 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.IsImage.fac_lift_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.Images
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y} {F : CategoryTheory.Limits.MonoFactorisation f} (hF : CategoryTheory.Limits.IsImage F) (F' : CategoryTheory.Limits.MonoFactorisation f) {Z : C} (h : F'.I ⟶ Z) : CategoryTheory.CategoryStruct.comp F.e (CategoryTheory.CategoryStruct.comp (hF.lift F') h) = CategoryTheory.CategoryStruct.comp F'.e h
• CategoryTheory.Limits.IsImage.lift_fac_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.Images
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y} {F : CategoryTheory.Limits.MonoFactorisation f} (self : CategoryTheory.Limits.IsImage F) (F' : CategoryTheory.Limits.MonoFactorisation f) {Z : C} (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (self.lift F') (CategoryTheory.CategoryStruct.comp F'.m h) = CategoryTheory.CategoryStruct.comp F.m h
• CategoryTheory.Limits.MonoFactorisation.ofCompIso_m 📋 Mathlib.CategoryTheory.Limits.Shapes.Images
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y} {Y' : C} {g : Y ⟶ Y'} [CategoryTheory.IsIso g] (F : CategoryTheory.Limits.MonoFactorisation (CategoryTheory.CategoryStruct.comp f g)) : F.ofCompIso.m = CategoryTheory.CategoryStruct.comp F.m (CategoryTheory.inv g)
• CategoryTheory.Limits.MonoFactorisation.ofIsoComp_e 📋 Mathlib.CategoryTheory.Limits.Shapes.Images
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y} {X' : C} (g : X' ⟶ X) [CategoryTheory.IsIso g] (F : CategoryTheory.Limits.MonoFactorisation (CategoryTheory.CategoryStruct.comp g f)) : (CategoryTheory.Limits.MonoFactorisation.ofIsoComp g F).e = CategoryTheory.CategoryStruct.comp (CategoryTheory.inv g) F.e
• CategoryTheory.Limits.MonoFactorisation.copy_e 📋 Mathlib.CategoryTheory.Limits.Shapes.Images
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y} (F : CategoryTheory.Limits.MonoFactorisation f) (m : F.I ⟶ Y) (e : X ⟶ F.I) (hm : m = F.m := by cat_disch) (he : e = F.e := by cat_disch) : (F.copy m e hm he).e = e
• CategoryTheory.Limits.MonoFactorisation.copy_m 📋 Mathlib.CategoryTheory.Limits.Shapes.Images
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y} (F : CategoryTheory.Limits.MonoFactorisation f) (m : F.I ⟶ Y) (e : X ⟶ F.I) (hm : m = F.m := by cat_disch) (he : e = F.e := by cat_disch) : (F.copy m e hm he).m = m
• CategoryTheory.Limits.IsImage.copy 📋 Mathlib.CategoryTheory.Limits.Shapes.Images
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y} {F : CategoryTheory.Limits.MonoFactorisation f} (hF : CategoryTheory.Limits.IsImage F) (m : F.I ⟶ Y) (e : X ⟶ F.I) (hm : m = F.m := by cat_disch) (he : e = F.e := by cat_disch) : CategoryTheory.Limits.IsImage (F.copy m e ⋯ ⋯)
• CategoryTheory.Limits.ImageFactorisation.copy 📋 Mathlib.CategoryTheory.Limits.Shapes.Images
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y} (F : CategoryTheory.Limits.ImageFactorisation f) (m : F.F.I ⟶ Y) (e : X ⟶ F.F.I) (hm : m = F.F.m := by cat_disch) (he : e = F.F.e := by cat_disch) : CategoryTheory.Limits.ImageFactorisation f
• CategoryTheory.Limits.MonoFactorisation.ofArrowIso_m 📋 Mathlib.CategoryTheory.Limits.Shapes.Images
  {C : Type u} [CategoryTheory.Category.{v, u} C] {f g : CategoryTheory.Arrow C} (F : CategoryTheory.Limits.MonoFactorisation f.hom) (sq : f ⟶ g) [CategoryTheory.IsIso sq] : (F.ofArrowIso sq).m = CategoryTheory.CategoryStruct.comp F.m (CategoryTheory.Arrow.Hom.right sq)
• 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.IsImage.ofIsoI_lift 📋 Mathlib.CategoryTheory.Limits.Shapes.Images
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y} {F : CategoryTheory.Limits.MonoFactorisation f} (hF : CategoryTheory.Limits.IsImage F) {I' : C} (e : F.I ≅ I') (F' : CategoryTheory.Limits.MonoFactorisation f) : (hF.ofIsoI e).lift F' = CategoryTheory.CategoryStruct.comp e.inv (hF.lift F')
• 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.MonoFactorisation.ofArrowIso_e 📋 Mathlib.CategoryTheory.Limits.Shapes.Images
  {C : Type u} [CategoryTheory.Category.{v, u} C] {f g : CategoryTheory.Arrow C} (F : CategoryTheory.Limits.MonoFactorisation f.hom) (sq : f ⟶ g) [CategoryTheory.IsIso sq] : (F.ofArrowIso sq).e = CategoryTheory.CategoryStruct.comp (CategoryTheory.inv (CategoryTheory.Arrow.Hom.left sq)) F.e
• CategoryTheory.Limits.IsImage.copy_lift 📋 Mathlib.CategoryTheory.Limits.Shapes.Images
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y} {F : CategoryTheory.Limits.MonoFactorisation f} (hF : CategoryTheory.Limits.IsImage F) (m : F.I ⟶ Y) (e : X ⟶ F.I) (hm : m = F.m := by cat_disch) (he : e = F.e := by cat_disch) (F' : CategoryTheory.Limits.MonoFactorisation f) : (hF.copy m e hm he).lift F' = hF.lift F'
• CategoryTheory.Limits.ImageFactorisation.copy_F 📋 Mathlib.CategoryTheory.Limits.Shapes.Images
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y} (F : CategoryTheory.Limits.ImageFactorisation f) (m : F.F.I ⟶ Y) (e : X ⟶ F.F.I) (hm : m = F.F.m := by cat_disch) (he : e = F.F.e := by cat_disch) : (F.copy m e hm he).F = F.F.copy m e ⋯ ⋯
• CategoryTheory.Limits.IsImage.ofArrowIso_lift 📋 Mathlib.CategoryTheory.Limits.Shapes.Images
  {C : Type u} [CategoryTheory.Category.{v, u} C] {f g : CategoryTheory.Arrow C} {F : CategoryTheory.Limits.MonoFactorisation f.hom} (hF : CategoryTheory.Limits.IsImage F) (sq : f ⟶ g) [CategoryTheory.IsIso sq] (F' : CategoryTheory.Limits.MonoFactorisation g.hom) : (hF.ofArrowIso sq).lift F' = hF.lift (F'.ofArrowIso (CategoryTheory.inv sq))
• CategoryTheory.Limits.ImageFactorisation.copy_isImage 📋 Mathlib.CategoryTheory.Limits.Shapes.Images
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y} (F : CategoryTheory.Limits.ImageFactorisation f) (m : F.F.I ⟶ Y) (e : X ⟶ F.F.I) (hm : m = F.F.m := by cat_disch) (he : e = F.F.e := by cat_disch) : (F.copy m e hm he).isImage = F.isImage.copy m e ⋯ ⋯
• 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 📋 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.MonoFactorisation.fac_apply 📋 Mathlib.CategoryTheory.Limits.Shapes.Images
  {C : Type u} [CategoryTheory.Category.{v, u} C] {F G : CategoryTheory.Functor C (Type w)} {f : F ⟶ G} {X : C} (H : CategoryTheory.Limits.MonoFactorisation f) (x : F.obj X) : (CategoryTheory.ConcreteCategory.hom (H.m.app X)) ((CategoryTheory.ConcreteCategory.hom (H.e.app X)) x) = (CategoryTheory.ConcreteCategory.hom (f.app X)) x
• CategoryTheory.Limits.monoFactorisationZero_I 📋 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.monoFactorisationZero X Y).I = 0
• CategoryTheory.Limits.MonoFactorisation.kernel_ι_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] (F : CategoryTheory.Limits.MonoFactorisation f) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.ι f) F.e = 0
• CategoryTheory.Limits.Types.Image.lift 📋 Mathlib.CategoryTheory.Limits.Types.Images
  {α β : Type u} {f : α ⟶ β} (F' : CategoryTheory.Limits.MonoFactorisation f) : CategoryTheory.Limits.Types.Image f ⟶ F'.I
• CategoryTheory.Limits.Types.Image.lift_fac 📋 Mathlib.CategoryTheory.Limits.Types.Images
  {α β : Type u} {f : α ⟶ β} (F' : CategoryTheory.Limits.MonoFactorisation f) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Types.Image.lift F') F'.m = CategoryTheory.Limits.Types.Image.ι f
• CategoryTheory.Abelian.coimageStrongEpiMonoFactorisation_I 📋 Mathlib.CategoryTheory.Abelian.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {P Q : C} (f : P ⟶ Q) : (CategoryTheory.Abelian.coimageStrongEpiMonoFactorisation f).I = CategoryTheory.Abelian.coimage f
• CategoryTheory.Abelian.imageStrongEpiMonoFactorisation_I 📋 Mathlib.CategoryTheory.Abelian.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {P Q : C} (f : P ⟶ Q) : (CategoryTheory.Abelian.imageStrongEpiMonoFactorisation f).I = CategoryTheory.Abelian.image f
• CategoryTheory.Abelian.OfCoimageImageComparisonIsIso.instIsIsoMImageMonoFactorisationOfHasZeroObjectOfEpi 📋 Mathlib.CategoryTheory.Abelian.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasKernels C] [CategoryTheory.Limits.HasCokernels C] [CategoryTheory.Limits.HasZeroObject C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Epi f] : CategoryTheory.IsIso (CategoryTheory.Abelian.OfCoimageImageComparisonIsIso.imageMonoFactorisation f).m
• CategoryTheory.Abelian.OfCoimageImageComparisonIsIso.imageMonoFactorisation_I 📋 Mathlib.CategoryTheory.Abelian.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasKernels C] [CategoryTheory.Limits.HasCokernels C] {X Y : C} (f : X ⟶ Y) : (CategoryTheory.Abelian.OfCoimageImageComparisonIsIso.imageMonoFactorisation f).I = CategoryTheory.Abelian.image f
• CategoryTheory.Abelian.OfCoimageImageComparisonIsIso.instIsIsoEImageMonoFactorisationOfHasZeroObjectOfMonoOfCoimageImageComparison 📋 Mathlib.CategoryTheory.Abelian.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasKernels C] [CategoryTheory.Limits.HasCokernels C] [CategoryTheory.Limits.HasZeroObject C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Mono f] [CategoryTheory.IsIso (CategoryTheory.Abelian.coimageImageComparison f)] : CategoryTheory.IsIso (CategoryTheory.Abelian.OfCoimageImageComparisonIsIso.imageMonoFactorisation f).e
• CategoryTheory.Abelian.OfCoimageImageComparisonIsIso.imageMonoFactorisation_e' 📋 Mathlib.CategoryTheory.Abelian.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasKernels C] [CategoryTheory.Limits.HasCokernels C] {X Y : C} (f : X ⟶ Y) : (CategoryTheory.Abelian.OfCoimageImageComparisonIsIso.imageMonoFactorisation f).e = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.cokernel.π (CategoryTheory.Limits.kernel.ι f)) (CategoryTheory.Abelian.coimageImageComparison f)
• CategoryTheory.MonoOver.commSqOfHasStrongEpiMonoFactorisation 📋 Mathlib.CategoryTheory.Subobject.MonoOver
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {Y : C} [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Limits.HasStrongEpiMonoFactorisations C] {J : Type u₂} [CategoryTheory.Category.{v₂, u₂} J] (F : CategoryTheory.Functor J (CategoryTheory.MonoOver Y)) (c : CategoryTheory.Limits.Cocone F) : CategoryTheory.CommSq (CategoryTheory.Limits.Sigma.desc fun i => CategoryTheory.Over.Hom.left (c.ι.app i).hom) (CategoryTheory.MonoOver.strongEpiMonoFactorisationSigmaDesc F).e c.pt.arrow (CategoryTheory.MonoOver.strongEpiMonoFactorisationSigmaDesc F).m
• CategoryTheory.MonoOver.liftStructOfHasStrongEpiMonoFactorisation 📋 Mathlib.CategoryTheory.Subobject.MonoOver
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {Y : C} [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Limits.HasStrongEpiMonoFactorisations C] {J : Type u₂} [CategoryTheory.Category.{v₂, u₂} J] (F : CategoryTheory.Functor J (CategoryTheory.MonoOver Y)) (c : CategoryTheory.Limits.Cocone F) : ⋯.LiftStruct
• CategoryTheory.Subobject.imageFactorisation_F_I 📋 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.imageFactorisation f x).F.I = CategoryTheory.Subobject.underlying.obj ((CategoryTheory.Subobject.exists f).obj x)
• AddCommGrpCat.image.lift 📋 Mathlib.Algebra.Category.Grp.Images
  {G H : AddCommGrpCat} {f : G ⟶ H} (F' : CategoryTheory.Limits.MonoFactorisation f) : AddCommGrpCat.image f ⟶ F'.I
• AddCommGrpCat.image.lift_fac 📋 Mathlib.Algebra.Category.Grp.Images
  {G H : AddCommGrpCat} {f : G ⟶ H} (F' : CategoryTheory.Limits.MonoFactorisation f) : CategoryTheory.CategoryStruct.comp (AddCommGrpCat.image.lift F') F'.m = AddCommGrpCat.image.ι f
• ModuleCat.image.lift 📋 Mathlib.Algebra.Category.ModuleCat.Images
  {R : Type u} [Ring R] {G H : ModuleCat R} {f : G ⟶ H} (F' : CategoryTheory.Limits.MonoFactorisation f) : ModuleCat.image f ⟶ F'.I
• ModuleCat.image.lift_fac 📋 Mathlib.Algebra.Category.ModuleCat.Images
  {R : Type u} [Ring R] {G H : ModuleCat R} {f : G ⟶ H} (F' : CategoryTheory.Limits.MonoFactorisation f) : CategoryTheory.CategoryStruct.comp (ModuleCat.image.lift F') F'.m = ModuleCat.image.ι f
• CategoryTheory.FunctorToTypes.monoFactorisation_I 📋 Mathlib.CategoryTheory.Limits.FunctorCategory.Shapes.Images
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {F G : CategoryTheory.Functor C (Type u)} (f : F ⟶ G) : (CategoryTheory.FunctorToTypes.monoFactorisation f).I = (CategoryTheory.Subfunctor.range f).toFunctor
• 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))
• CategoryTheory.Regular.instIsRegularEpiEStrongEpiMonoFactorisation 📋 Mathlib.CategoryTheory.RegularCategory.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Regular C] {X Y : C} (f : X ⟶ Y) : CategoryTheory.IsRegularEpi (CategoryTheory.Regular.strongEpiMonoFactorisation f).e
• CategoryTheory.Regular.frobeniusStrongEpiMonoFactorisation_I 📋 Mathlib.CategoryTheory.RegularCategory.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Regular C] {A B : C} (f : A ⟶ B) (A' : CategoryTheory.Subobject A) (B' : CategoryTheory.Subobject B) : (CategoryTheory.Regular.frobeniusStrongEpiMonoFactorisation f A' B').I = CategoryTheory.Subobject.underlying.obj ((CategoryTheory.Subobject.exists f).obj A' ⊓ B')

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