Loogle!

Result

Found 96 declarations mentioning CategoryTheory.Limits.MonoFactorisation.

• CategoryTheory.Limits.MonoFactorisation 📋 Mathlib.CategoryTheory.Limits.Shapes.Images
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) : Type (max u v)
• CategoryTheory.Limits.IsImage 📋 Mathlib.CategoryTheory.Limits.Shapes.Images
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y} (F : CategoryTheory.Limits.MonoFactorisation f) : Type (max u v)
• 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.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.ImageFactorisation.F 📋 Mathlib.CategoryTheory.Limits.Shapes.Images
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y} (self : CategoryTheory.Limits.ImageFactorisation f) : CategoryTheory.Limits.MonoFactorisation f
• CategoryTheory.Limits.MonoFactorisation.self 📋 Mathlib.CategoryTheory.Limits.Shapes.Images
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Mono f] : CategoryTheory.Limits.MonoFactorisation f
• CategoryTheory.Limits.StrongEpiMonoFactorisation.toMonoFactorisation 📋 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.Limits.MonoFactorisation f
• CategoryTheory.Limits.MonoFactorisation.instInhabitedOfMono 📋 Mathlib.CategoryTheory.Limits.Shapes.Images
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Mono f] : Inhabited (CategoryTheory.Limits.MonoFactorisation f)
• CategoryTheory.Limits.ImageFactorisation.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) (isImage : CategoryTheory.Limits.IsImage F) : CategoryTheory.Limits.ImageFactorisation f
• 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.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.MonoFactorisation.isoComp 📋 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) : CategoryTheory.Limits.MonoFactorisation (CategoryTheory.CategoryStruct.comp g 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.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.MonoFactorisation.compMono 📋 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] : CategoryTheory.Limits.MonoFactorisation (CategoryTheory.CategoryStruct.comp f g)
• CategoryTheory.Limits.MonoFactorisation.ofCompIso 📋 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)) : CategoryTheory.Limits.MonoFactorisation f
• CategoryTheory.Limits.MonoFactorisation.ofIsoComp 📋 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 f
• CategoryTheory.Limits.image.lift_mono 📋 Mathlib.CategoryTheory.Limits.Shapes.Images
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y} [CategoryTheory.Limits.HasImage f] (F' : CategoryTheory.Limits.MonoFactorisation f) : CategoryTheory.Mono (CategoryTheory.Limits.image.lift F')
• CategoryTheory.Limits.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.ofArrowIso 📋 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] : CategoryTheory.Limits.MonoFactorisation g.hom
• 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.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.MonoFactorisation.mk 📋 Mathlib.CategoryTheory.Limits.Shapes.Images
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y} (I : C) (m : I ⟶ Y) [m_mono : CategoryTheory.Mono m] (e : X ⟶ I) (fac : CategoryTheory.CategoryStruct.comp e m = f := by cat_disch) : CategoryTheory.Limits.MonoFactorisation f
• 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.IsImage.ofArrowIso 📋 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] : CategoryTheory.Limits.IsImage (F.ofArrowIso sq)
• 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.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.ImageFactorisation.ofArrowIso_F 📋 Mathlib.CategoryTheory.Limits.Shapes.Images
  {C : Type u} [CategoryTheory.Category.{v, u} C] {f g : CategoryTheory.Arrow C} (F : CategoryTheory.Limits.ImageFactorisation f.hom) (sq : f ⟶ g) [CategoryTheory.IsIso sq] : (F.ofArrowIso sq).F = F.F.ofArrowIso sq
• 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.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.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.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.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 📋 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.MonoFactorisation 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.monoFactorisation 📋 Mathlib.CategoryTheory.Limits.Types.Images
  {α β : Type u} (f : α ⟶ β) : CategoryTheory.Limits.MonoFactorisation f
• 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.OfCoimageImageComparisonIsIso.imageMonoFactorisation 📋 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.Limits.MonoFactorisation f
• AddCommGrpCat.monoFactorisation 📋 Mathlib.Algebra.Category.Grp.Images
  {G H : AddCommGrpCat} (f : G ⟶ H) : CategoryTheory.Limits.MonoFactorisation f
• 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.monoFactorisation 📋 Mathlib.Algebra.Category.ModuleCat.Images
  {R : Type u} [Ring R] {G H : ModuleCat R} (f : G ⟶ H) : CategoryTheory.Limits.MonoFactorisation 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.imageMonoFactorization 📋 Mathlib.CategoryTheory.Sites.Subsheaf
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {F F' : CategoryTheory.Sheaf J (Type w)} (f : F ⟶ F') : CategoryTheory.Limits.MonoFactorisation f
• CategoryTheory.FunctorToTypes.monoFactorisation 📋 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.Limits.MonoFactorisation 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