Loogle!

Result

Found 74 declarations mentioning CategoryTheory.Limits.HasImages.

• CategoryTheory.Limits.HasImages 📋 Mathlib.CategoryTheory.Limits.Shapes.Images
  (C : Type u) [CategoryTheory.Category.{v, u} C] : Prop
• CategoryTheory.Limits.HasImageMaps 📋 Mathlib.CategoryTheory.Limits.Shapes.Images
  (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasImages C] : Prop
• CategoryTheory.Limits.HasStrongEpiImages 📋 Mathlib.CategoryTheory.Limits.Shapes.Images
  (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasImages C] : Prop
• CategoryTheory.Limits.hasImages_of_hasStrongEpiMonoFactorisations 📋 Mathlib.CategoryTheory.Limits.Shapes.Images
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasStrongEpiMonoFactorisations C] : CategoryTheory.Limits.HasImages C
• CategoryTheory.Limits.hasImageMapsOfHasStrongEpiImages 📋 Mathlib.CategoryTheory.Limits.Shapes.Images
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasImages C] [CategoryTheory.Limits.HasStrongEpiImages C] : CategoryTheory.Limits.HasImageMaps C
• CategoryTheory.Limits.hasStrongEpiImages_of_hasPullbacks_of_hasEqualizers 📋 Mathlib.CategoryTheory.Limits.Shapes.Images
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasImages C] [CategoryTheory.Limits.HasPullbacks C] [CategoryTheory.Limits.HasEqualizers C] : CategoryTheory.Limits.HasStrongEpiImages C
• CategoryTheory.Limits.im 📋 Mathlib.CategoryTheory.Limits.Shapes.Images
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasImages C] [CategoryTheory.Limits.HasImageMaps C] : CategoryTheory.Functor (CategoryTheory.Arrow C) 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.im_obj 📋 Mathlib.CategoryTheory.Limits.Shapes.Images
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasImages C] [CategoryTheory.Limits.HasImageMaps C] (f : CategoryTheory.Arrow C) : CategoryTheory.Limits.im.obj f = CategoryTheory.Limits.image f.hom
• CategoryTheory.Limits.HasStrongEpiImages.mk 📋 Mathlib.CategoryTheory.Limits.Shapes.Images
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasImages C] (strong_factorThruImage : ∀ {X Y : C} (f : X ⟶ Y), CategoryTheory.StrongEpi (CategoryTheory.Limits.factorThruImage f)) : CategoryTheory.Limits.HasStrongEpiImages C
• CategoryTheory.Limits.HasStrongEpiImages.strong_factorThruImage 📋 Mathlib.CategoryTheory.Limits.Shapes.Images
  {C : Type u} {inst✝ : CategoryTheory.Category.{v, u} C} {inst✝¹ : CategoryTheory.Limits.HasImages C} [self : CategoryTheory.Limits.HasStrongEpiImages C] {X Y : C} (f : X ⟶ Y) : CategoryTheory.StrongEpi (CategoryTheory.Limits.factorThruImage f)
• CategoryTheory.Limits.HasImageMaps.has_image_map 📋 Mathlib.CategoryTheory.Limits.Shapes.Images
  {C : Type u} {inst✝ : CategoryTheory.Category.{v, u} C} {inst✝¹ : CategoryTheory.Limits.HasImages C} [self : CategoryTheory.Limits.HasImageMaps C] {f g : CategoryTheory.Arrow C} (st : f ⟶ g) : CategoryTheory.Limits.HasImageMap st
• CategoryTheory.Limits.HasImageMaps.mk 📋 Mathlib.CategoryTheory.Limits.Shapes.Images
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasImages C] (has_image_map : ∀ {f g : CategoryTheory.Arrow C} (st : f ⟶ g), CategoryTheory.Limits.HasImageMap st) : CategoryTheory.Limits.HasImageMaps C
• CategoryTheory.Limits.im_map 📋 Mathlib.CategoryTheory.Limits.Shapes.Images
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasImages C] [CategoryTheory.Limits.HasImageMaps C] {X✝ Y✝ : CategoryTheory.Arrow C} (st : X✝ ⟶ Y✝) : CategoryTheory.Limits.im.map st = CategoryTheory.Limits.image.map st
• CategoryTheory.Limits.Types.instHasImagesType 📋 Mathlib.CategoryTheory.Limits.Types.Images
  : CategoryTheory.Limits.HasImages (Type u)
• CategoryTheory.Abelian.OfCoimageImageComparisonIsIso.hasImages 📋 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.IsIso (CategoryTheory.Abelian.coimageImageComparison f)] : CategoryTheory.Limits.HasImages C
• CategoryTheory.MonoOver.image 📋 Mathlib.CategoryTheory.Subobject.MonoOver
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} [CategoryTheory.Limits.HasImages C] : CategoryTheory.Functor (CategoryTheory.Over X) (CategoryTheory.MonoOver X)
• CategoryTheory.MonoOver.instIsRightAdjointOverForget 📋 Mathlib.CategoryTheory.Subobject.MonoOver
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} [CategoryTheory.Limits.HasImages C] : (CategoryTheory.MonoOver.forget X).IsRightAdjoint
• CategoryTheory.MonoOver.reflective 📋 Mathlib.CategoryTheory.Subobject.MonoOver
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} [CategoryTheory.Limits.HasImages C] : CategoryTheory.Reflective (CategoryTheory.MonoOver.forget X)
• CategoryTheory.MonoOver.imageForgetAdj 📋 Mathlib.CategoryTheory.Subobject.MonoOver
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} [CategoryTheory.Limits.HasImages C] : CategoryTheory.MonoOver.image ⊣ CategoryTheory.MonoOver.forget X
• CategoryTheory.MonoOver.exists 📋 Mathlib.CategoryTheory.Subobject.MonoOver
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} [CategoryTheory.Limits.HasImages C] (f : X ⟶ Y) : CategoryTheory.Functor (CategoryTheory.MonoOver X) (CategoryTheory.MonoOver Y)
• CategoryTheory.MonoOver.faithful_exists 📋 Mathlib.CategoryTheory.Subobject.MonoOver
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} [CategoryTheory.Limits.HasImages C] (f : X ⟶ Y) : (CategoryTheory.MonoOver.exists f).Faithful
• CategoryTheory.MonoOver.image_obj 📋 Mathlib.CategoryTheory.Subobject.MonoOver
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} [CategoryTheory.Limits.HasImages C] (f : CategoryTheory.Over X) : CategoryTheory.MonoOver.image.obj f = CategoryTheory.MonoOver.imageMonoOver f.hom
• CategoryTheory.MonoOver.existsPullbackAdj 📋 Mathlib.CategoryTheory.Subobject.MonoOver
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} [CategoryTheory.Limits.HasImages C] (f : X ⟶ Y) [CategoryTheory.Limits.HasPullbacks C] : CategoryTheory.MonoOver.exists f ⊣ CategoryTheory.MonoOver.pullback f
• CategoryTheory.MonoOver.existsIsoMap 📋 Mathlib.CategoryTheory.Subobject.MonoOver
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} [CategoryTheory.Limits.HasImages C] (f : X ⟶ Y) [CategoryTheory.Mono f] : CategoryTheory.MonoOver.exists f ≅ CategoryTheory.MonoOver.map f
• CategoryTheory.MonoOver.forgetImage 📋 Mathlib.CategoryTheory.Subobject.MonoOver
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} [CategoryTheory.Limits.HasImages C] : (CategoryTheory.MonoOver.forget X).comp CategoryTheory.MonoOver.image ≅ CategoryTheory.Functor.id (CategoryTheory.MonoOver X)
• CategoryTheory.MonoOver.image_map 📋 Mathlib.CategoryTheory.Subobject.MonoOver
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} [CategoryTheory.Limits.HasImages C] {f g : CategoryTheory.Over X} (k : f ⟶ g) : CategoryTheory.MonoOver.image.map k = (CategoryTheory.MonoOver.forget X).preimage (CategoryTheory.Over.homMk (CategoryTheory.Limits.image.lift { I := CategoryTheory.Limits.image g.hom, m := CategoryTheory.Limits.image.ι g.hom, m_mono := ⋯, e := CategoryTheory.CategoryStruct.comp (CategoryTheory.Over.Hom.left k) (CategoryTheory.Limits.factorThruImage g.hom), fac := ⋯ }) ⋯)
• CategoryTheory.Subobject.exists 📋 Mathlib.CategoryTheory.Subobject.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} [CategoryTheory.Limits.HasImages C] (f : X ⟶ Y) : CategoryTheory.Functor (CategoryTheory.Subobject X) (CategoryTheory.Subobject Y)
• CategoryTheory.Subobject.existsPullbackAdj 📋 Mathlib.CategoryTheory.Subobject.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} [CategoryTheory.Limits.HasImages C] (f : X ⟶ Y) [CategoryTheory.Limits.HasPullbacks C] : CategoryTheory.Subobject.exists f ⊣ CategoryTheory.Subobject.pullback f
• CategoryTheory.Subobject.exists_iso_map 📋 Mathlib.CategoryTheory.Subobject.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} [CategoryTheory.Limits.HasImages C] (f : X ⟶ Y) [CategoryTheory.Mono f] : CategoryTheory.Subobject.exists f = CategoryTheory.Subobject.map f
• CategoryTheory.Subobject.imageFactorisation 📋 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.Limits.ImageFactorisation (CategoryTheory.CategoryStruct.comp x.arrow f)
• CategoryTheory.Subobject.existsCompRepresentativeIso 📋 Mathlib.CategoryTheory.Subobject.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} [CategoryTheory.Limits.HasImages C] (f : X ⟶ Y) : (CategoryTheory.Subobject.exists f).comp CategoryTheory.Subobject.representative ≅ CategoryTheory.Subobject.representative.comp (CategoryTheory.MonoOver.exists f)
• CategoryTheory.Subobject.existsIsoImage 📋 Mathlib.CategoryTheory.Subobject.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} [CategoryTheory.Limits.HasImages C] (f : X ⟶ Y) (x : CategoryTheory.Subobject X) : CategoryTheory.Subobject.underlying.obj ((CategoryTheory.Subobject.exists f).obj x) ≅ CategoryTheory.Limits.image (CategoryTheory.CategoryStruct.comp x.arrow f)
• CategoryTheory.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)
• CategoryTheory.Subobject.imageFactorisation_F_m 📋 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.m = ((CategoryTheory.Subobject.exists f).obj x).arrow
• CategoryTheory.Subobject.semilatticeSup 📋 Mathlib.CategoryTheory.Subobject.Lattice
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasImages C] [CategoryTheory.Limits.HasBinaryCoproducts C] {B : C} : SemilatticeSup (CategoryTheory.Subobject B)
• CategoryTheory.Subobject.instLattice 📋 Mathlib.CategoryTheory.Subobject.Lattice
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasPullbacks C] [CategoryTheory.Limits.HasImages C] [CategoryTheory.Limits.HasBinaryCoproducts C] {B : C} : Lattice (CategoryTheory.Subobject B)
• CategoryTheory.Subobject.completeSemilatticeSup 📋 Mathlib.CategoryTheory.Subobject.Lattice
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.LocallySmall.{w, v₁, u₁} C] [CategoryTheory.WellPowered.{w, v₁, u₁} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Limits.HasImages C] {B : C} : CompleteSemilatticeSup (CategoryTheory.Subobject B)
• CategoryTheory.Subobject.sSup 📋 Mathlib.CategoryTheory.Subobject.Lattice
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.LocallySmall.{w, v₁, u₁} C] [CategoryTheory.WellPowered.{w, v₁, u₁} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Limits.HasImages C] {A : C} (s : Set (CategoryTheory.Subobject A)) : CategoryTheory.Subobject A
• CategoryTheory.Subobject.instCompleteLattice 📋 Mathlib.CategoryTheory.Subobject.Lattice
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.LocallySmall.{w, v₁, u₁} C] [CategoryTheory.WellPowered.{w, v₁, u₁} C] [CategoryTheory.Limits.HasWidePullbacks C] [CategoryTheory.Limits.HasImages C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Limits.InitialMonoClass C] {B : C} : CompleteLattice (CategoryTheory.Subobject B)
• CategoryTheory.Subobject.sup_factors_of_factors_left 📋 Mathlib.CategoryTheory.Subobject.Lattice
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasImages C] [CategoryTheory.Limits.HasBinaryCoproducts C] {A B : C} {X Y : CategoryTheory.Subobject B} {f : A ⟶ B} (P : X.Factors f) : (X ⊔ Y).Factors f
• CategoryTheory.Subobject.sup_factors_of_factors_right 📋 Mathlib.CategoryTheory.Subobject.Lattice
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasImages C] [CategoryTheory.Limits.HasBinaryCoproducts C] {A B : C} {X Y : CategoryTheory.Subobject B} {f : A ⟶ B} (P : Y.Factors f) : (X ⊔ Y).Factors f
• CategoryTheory.Subobject.le_sSup 📋 Mathlib.CategoryTheory.Subobject.Lattice
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.LocallySmall.{w, v₁, u₁} C] [CategoryTheory.WellPowered.{w, v₁, u₁} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Limits.HasImages C] {A : C} (s : Set (CategoryTheory.Subobject A)) (f : CategoryTheory.Subobject A) (hf : f ∈ s) : f ≤ CategoryTheory.Subobject.sSup s
• CategoryTheory.Subobject.finset_sup_factors 📋 Mathlib.CategoryTheory.Subobject.Lattice
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasImages C] [CategoryTheory.Limits.HasBinaryCoproducts C] [CategoryTheory.Limits.HasInitial C] [CategoryTheory.Limits.InitialMonoClass C] {I : Type u_1} {A B : C} {s : Finset I} {P : I → CategoryTheory.Subobject B} {f : A ⟶ B} (h : ∃ i ∈ s, (P i).Factors f) : (s.sup P).Factors f
• CategoryTheory.Subobject.sSup_le 📋 Mathlib.CategoryTheory.Subobject.Lattice
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.LocallySmall.{w, v₁, u₁} C] [CategoryTheory.WellPowered.{w, v₁, u₁} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Limits.HasImages C] {A : C} (s : Set (CategoryTheory.Subobject A)) (f : CategoryTheory.Subobject A) (k : ∀ g ∈ s, g ≤ f) : CategoryTheory.Subobject.sSup s ≤ f
• CategoryTheory.MonoOver.sup 📋 Mathlib.CategoryTheory.Subobject.Lattice
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasImages C] [CategoryTheory.Limits.HasBinaryCoproducts C] {A : C} : CategoryTheory.Functor (CategoryTheory.MonoOver A) (CategoryTheory.Functor (CategoryTheory.MonoOver A) (CategoryTheory.MonoOver A))
• CategoryTheory.Subobject.sup 📋 Mathlib.CategoryTheory.Subobject.Lattice
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasImages C] [CategoryTheory.Limits.HasBinaryCoproducts C] {A : C} : CategoryTheory.Functor (CategoryTheory.Subobject A) (CategoryTheory.Functor (CategoryTheory.Subobject A) (CategoryTheory.Subobject A))
• CategoryTheory.MonoOver.leSupLeft 📋 Mathlib.CategoryTheory.Subobject.Lattice
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasImages C] [CategoryTheory.Limits.HasBinaryCoproducts C] {A : C} (f g : CategoryTheory.MonoOver A) : f ⟶ (CategoryTheory.MonoOver.sup.obj f).obj g
• CategoryTheory.MonoOver.leSupRight 📋 Mathlib.CategoryTheory.Subobject.Lattice
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasImages C] [CategoryTheory.Limits.HasBinaryCoproducts C] {A : C} (f g : CategoryTheory.MonoOver A) : g ⟶ (CategoryTheory.MonoOver.sup.obj f).obj g
• CategoryTheory.MonoOver.supLe 📋 Mathlib.CategoryTheory.Subobject.Lattice
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasImages C] [CategoryTheory.Limits.HasBinaryCoproducts C] {A : C} (f g h : CategoryTheory.MonoOver A) : (f ⟶ h) → (g ⟶ h) → ((CategoryTheory.MonoOver.sup.obj f).obj g ⟶ h)
• imageToKernel' 📋 Mathlib.Algebra.Homology.ImageToKernel
  {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {A B C : V} (f : A ⟶ B) (g : B ⟶ C) [CategoryTheory.Limits.HasKernels V] [CategoryTheory.Limits.HasImages V] (w : CategoryTheory.CategoryStruct.comp f g = 0) : CategoryTheory.Limits.image f ⟶ CategoryTheory.Limits.kernel g
• imageToKernel_epi_of_epi_of_zero 📋 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.HasImages V] [CategoryTheory.Epi f] : CategoryTheory.Epi (imageToKernel f 0 ⋯)
• imageSubobjectIso_imageToKernel' 📋 Mathlib.Algebra.Homology.ImageToKernel
  {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {A B C : V} (f : A ⟶ B) (g : B ⟶ C) [CategoryTheory.Limits.HasKernels V] [CategoryTheory.Limits.HasImages V] (w : CategoryTheory.CategoryStruct.comp f g = 0) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.imageSubobjectIso f).hom (imageToKernel' f g w) = CategoryTheory.CategoryStruct.comp (imageToKernel f g w) (CategoryTheory.Limits.kernelSubobjectIso g).hom
• imageToKernel'_kernelSubobjectIso 📋 Mathlib.Algebra.Homology.ImageToKernel
  {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {A B C : V} (f : A ⟶ B) (g : B ⟶ C) [CategoryTheory.Limits.HasKernels V] [CategoryTheory.Limits.HasImages V] (w : CategoryTheory.CategoryStruct.comp f g = 0) : CategoryTheory.CategoryStruct.comp (imageToKernel' f g w) (CategoryTheory.Limits.kernelSubobjectIso g).inv = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.imageSubobjectIso f).inv (imageToKernel f g w)
• imageToKernel_comp_left 📋 Mathlib.Algebra.Homology.ImageToKernel
  {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {A B C : V} (f : A ⟶ B) (g : B ⟶ C) [CategoryTheory.Limits.HasKernels V] [CategoryTheory.Limits.HasImages V] {Z : V} (h : Z ⟶ A) (w : CategoryTheory.CategoryStruct.comp f g = 0) : imageToKernel (CategoryTheory.CategoryStruct.comp h f) g ⋯ = CategoryTheory.CategoryStruct.comp ((CategoryTheory.Limits.imageSubobject (CategoryTheory.CategoryStruct.comp h f)).ofLE (CategoryTheory.Limits.imageSubobject f) ⋯) (imageToKernel f g w)
• imageToKernel_comp_right 📋 Mathlib.Algebra.Homology.ImageToKernel
  {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {A B C : V} (f : A ⟶ B) (g : B ⟶ C) [CategoryTheory.Limits.HasKernels V] [CategoryTheory.Limits.HasImages V] {D : V} (h : C ⟶ D) (w : CategoryTheory.CategoryStruct.comp f g = 0) : imageToKernel f (CategoryTheory.CategoryStruct.comp g h) ⋯ = CategoryTheory.CategoryStruct.comp (imageToKernel f g w) ((CategoryTheory.Limits.kernelSubobject g).ofLE (CategoryTheory.Limits.kernelSubobject (CategoryTheory.CategoryStruct.comp g h)) ⋯)
• imageToKernel_zero_right 📋 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.HasImages V] {w : CategoryTheory.CategoryStruct.comp f 0 = 0} : imageToKernel f 0 w = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.imageSubobject f).arrow (CategoryTheory.inv (CategoryTheory.Limits.kernelSubobject 0).arrow)
• imageToKernel_epi_comp 📋 Mathlib.Algebra.Homology.ImageToKernel
  {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {A B C : V} (f : A ⟶ B) (g : B ⟶ C) [CategoryTheory.Limits.HasKernels V] [CategoryTheory.Limits.HasImages V] {Z : V} (h : Z ⟶ A) [CategoryTheory.Epi h] (w : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp h f) g = 0) : imageToKernel (CategoryTheory.CategoryStruct.comp h f) g w = CategoryTheory.CategoryStruct.comp ((CategoryTheory.Limits.imageSubobject (CategoryTheory.CategoryStruct.comp h f)).ofLE (CategoryTheory.Limits.imageSubobject f) ⋯) (imageToKernel f g ⋯)
• imageToKernel_comp_mono 📋 Mathlib.Algebra.Homology.ImageToKernel
  {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {A B C : V} (f : A ⟶ B) (g : B ⟶ C) [CategoryTheory.Limits.HasKernels V] [CategoryTheory.Limits.HasImages V] {D : V} (h : C ⟶ D) [CategoryTheory.Mono h] (w : CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp g h) = 0) : imageToKernel f (CategoryTheory.CategoryStruct.comp g h) w = CategoryTheory.CategoryStruct.comp (imageToKernel f g ⋯) ((CategoryTheory.Limits.kernelSubobject (CategoryTheory.CategoryStruct.comp g h)).isoOfEq (CategoryTheory.Limits.kernelSubobject g) ⋯).inv
• imageToKernel_comp_hom_inv_comp 📋 Mathlib.Algebra.Homology.ImageToKernel
  {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {A B C : V} (f : A ⟶ B) (g : B ⟶ C) [CategoryTheory.Limits.HasEqualizers V] [CategoryTheory.Limits.HasImages V] {Z : V} {i : B ≅ Z} (w : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f i.hom) (CategoryTheory.CategoryStruct.comp i.inv g) = 0) : imageToKernel (CategoryTheory.CategoryStruct.comp f i.hom) (CategoryTheory.CategoryStruct.comp i.inv g) w = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.imageSubobjectCompIso f i.hom).hom (CategoryTheory.CategoryStruct.comp (imageToKernel f g ⋯) (CategoryTheory.Limits.kernelSubobjectIsoComp i.inv g).inv)
• HomologicalComplex.image_to_eq_image 📋 Mathlib.Algebra.Homology.HomologicalComplex
  {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (C : HomologicalComplex V c) [CategoryTheory.Limits.HasImages V] [CategoryTheory.Limits.HasEqualizers V] {i j : ι} (r : c.Rel i j) : CategoryTheory.Limits.imageSubobject (C.dTo j) = CategoryTheory.Limits.imageSubobject (C.d i j)
• HomologicalComplex.image_eq_image 📋 Mathlib.Algebra.Homology.HomologicalComplex
  {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (C : HomologicalComplex V c) [CategoryTheory.Limits.HasImages V] [CategoryTheory.Limits.HasEqualizers V] {i i' j : ι} (r : c.Rel i j) (r' : c.Rel i' j) : CategoryTheory.Limits.imageSubobject (C.d i j) = CategoryTheory.Limits.imageSubobject (C.d i' j)
• CategoryTheory.instHasImagesSheafType 📋 Mathlib.CategoryTheory.Sites.Subsheaf
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} : CategoryTheory.Limits.HasImages (CategoryTheory.Sheaf J (Type (max v u)))
• CategoryTheory.FunctorToTypes.instHasImagesFunctorType 📋 Mathlib.CategoryTheory.Limits.FunctorCategory.Shapes.Images
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] : CategoryTheory.Limits.HasImages (CategoryTheory.Functor C (Type u_2))
• CategoryTheory.PreservesImage.iso 📋 Mathlib.CategoryTheory.Limits.Preserves.Shapes.Images
  {A : Type u₁} {B : Type u₂} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Limits.HasEqualizers A] [CategoryTheory.Limits.HasImages A] [CategoryTheory.StrongEpiCategory B] [CategoryTheory.Limits.HasImages B] (L : CategoryTheory.Functor A B) [∀ {X Y Z : A} (f : X ⟶ Z) (g : Y ⟶ Z), CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan f g) L] [∀ {X Y Z : A} (f : X ⟶ Y) (g : X ⟶ Z), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.span f g) L] {X Y : A} (f : X ⟶ Y) : CategoryTheory.Limits.image (L.map f) ≅ L.obj (CategoryTheory.Limits.image f)
• CategoryTheory.PreservesImage.factorThruImage_comp_hom 📋 Mathlib.CategoryTheory.Limits.Preserves.Shapes.Images
  {A : Type u₁} {B : Type u₂} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Limits.HasEqualizers A] [CategoryTheory.Limits.HasImages A] [CategoryTheory.StrongEpiCategory B] [CategoryTheory.Limits.HasImages B] (L : CategoryTheory.Functor A B) [∀ {X Y Z : A} (f : X ⟶ Z) (g : Y ⟶ Z), CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan f g) L] [∀ {X Y Z : A} (f : X ⟶ Y) (g : X ⟶ Z), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.span f g) L] {X Y : A} (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.factorThruImage (L.map f)) (CategoryTheory.PreservesImage.iso L f).hom = L.map (CategoryTheory.Limits.factorThruImage f)
• CategoryTheory.PreservesImage.inv_comp_image_ι_map 📋 Mathlib.CategoryTheory.Limits.Preserves.Shapes.Images
  {A : Type u₁} {B : Type u₂} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Limits.HasEqualizers A] [CategoryTheory.Limits.HasImages A] [CategoryTheory.StrongEpiCategory B] [CategoryTheory.Limits.HasImages B] (L : CategoryTheory.Functor A B) [∀ {X Y Z : A} (f : X ⟶ Z) (g : Y ⟶ Z), CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan f g) L] [∀ {X Y Z : A} (f : X ⟶ Y) (g : X ⟶ Z), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.span f g) L] {X Y : A} (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp (CategoryTheory.PreservesImage.iso L f).inv (CategoryTheory.Limits.image.ι (L.map f)) = L.map (CategoryTheory.Limits.image.ι f)
• CategoryTheory.PreservesImage.hom_comp_map_image_ι 📋 Mathlib.CategoryTheory.Limits.Preserves.Shapes.Images
  {A : Type u₁} {B : Type u₂} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Limits.HasEqualizers A] [CategoryTheory.Limits.HasImages A] [CategoryTheory.StrongEpiCategory B] [CategoryTheory.Limits.HasImages B] (L : CategoryTheory.Functor A B) [∀ {X Y Z : A} (f : X ⟶ Z) (g : Y ⟶ Z), CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan f g) L] [∀ {X Y Z : A} (f : X ⟶ Y) (g : X ⟶ Z), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.span f g) L] {X Y : A} (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp (CategoryTheory.PreservesImage.iso L f).hom (L.map (CategoryTheory.Limits.image.ι f)) = CategoryTheory.Limits.image.ι (L.map f)
• CategoryTheory.PreservesImage.factorThruImage_comp_hom_assoc 📋 Mathlib.CategoryTheory.Limits.Preserves.Shapes.Images
  {A : Type u₁} {B : Type u₂} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Limits.HasEqualizers A] [CategoryTheory.Limits.HasImages A] [CategoryTheory.StrongEpiCategory B] [CategoryTheory.Limits.HasImages B] (L : CategoryTheory.Functor A B) [∀ {X Y Z : A} (f : X ⟶ Z) (g : Y ⟶ Z), CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan f g) L] [∀ {X Y Z : A} (f : X ⟶ Y) (g : X ⟶ Z), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.span f g) L] {X Y : A} (f : X ⟶ Y) {Z : B} (h : L.obj (CategoryTheory.Limits.image f) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.factorThruImage (L.map f)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.PreservesImage.iso L f).hom h) = CategoryTheory.CategoryStruct.comp (L.map (CategoryTheory.Limits.factorThruImage f)) h
• CategoryTheory.PreservesImage.inv_comp_image_ι_map_assoc 📋 Mathlib.CategoryTheory.Limits.Preserves.Shapes.Images
  {A : Type u₁} {B : Type u₂} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Limits.HasEqualizers A] [CategoryTheory.Limits.HasImages A] [CategoryTheory.StrongEpiCategory B] [CategoryTheory.Limits.HasImages B] (L : CategoryTheory.Functor A B) [∀ {X Y Z : A} (f : X ⟶ Z) (g : Y ⟶ Z), CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan f g) L] [∀ {X Y Z : A} (f : X ⟶ Y) (g : X ⟶ Z), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.span f g) L] {X Y : A} (f : X ⟶ Y) {Z : B} (h : L.obj Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.PreservesImage.iso L f).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.image.ι (L.map f)) h) = CategoryTheory.CategoryStruct.comp (L.map (CategoryTheory.Limits.image.ι f)) h
• CategoryTheory.PreservesImage.hom_comp_map_image_ι_assoc 📋 Mathlib.CategoryTheory.Limits.Preserves.Shapes.Images
  {A : Type u₁} {B : Type u₂} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Limits.HasEqualizers A] [CategoryTheory.Limits.HasImages A] [CategoryTheory.StrongEpiCategory B] [CategoryTheory.Limits.HasImages B] (L : CategoryTheory.Functor A B) [∀ {X Y Z : A} (f : X ⟶ Z) (g : Y ⟶ Z), CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan f g) L] [∀ {X Y Z : A} (f : X ⟶ Y) (g : X ⟶ Z), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.span f g) L] {X Y : A} (f : X ⟶ Y) {Z : B} (h : L.obj Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.PreservesImage.iso L f).hom (CategoryTheory.CategoryStruct.comp (L.map (CategoryTheory.Limits.image.ι f)) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.image.ι (L.map f)) h
• CategoryTheory.PreservesImage.iso_hom 📋 Mathlib.CategoryTheory.Limits.Preserves.Shapes.Images
  {A : Type u₁} {B : Type u₂} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Limits.HasEqualizers A] [CategoryTheory.Limits.HasImages A] [CategoryTheory.StrongEpiCategory B] [CategoryTheory.Limits.HasImages B] (L : CategoryTheory.Functor A B) [∀ {X Y Z : A} (f : X ⟶ Z) (g : Y ⟶ Z), CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan f g) L] [∀ {X Y Z : A} (f : X ⟶ Y) (g : X ⟶ Z), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.span f g) L] {X Y : A} (f : X ⟶ Y) : (CategoryTheory.PreservesImage.iso L f).hom = CategoryTheory.Limits.image.lift { I := L.obj (CategoryTheory.Limits.image f), m := L.map (CategoryTheory.Limits.image.ι f), m_mono := ⋯, e := L.map (CategoryTheory.Limits.factorThruImage f), fac := ⋯ }
• CategoryTheory.PreservesImage.iso_inv 📋 Mathlib.CategoryTheory.Limits.Preserves.Shapes.Images
  {A : Type u₁} {B : Type u₂} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Limits.HasEqualizers A] [CategoryTheory.Limits.HasImages A] [CategoryTheory.StrongEpiCategory B] [CategoryTheory.Limits.HasImages B] (L : CategoryTheory.Functor A B) [∀ {X Y Z : A} (f : X ⟶ Z) (g : Y ⟶ Z), CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan f g) L] [∀ {X Y Z : A} (f : X ⟶ Y) (g : X ⟶ Z), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.span f g) L] {X Y : A} (f : X ⟶ Y) : (CategoryTheory.PreservesImage.iso L f).inv = { I := L.obj (CategoryTheory.Limits.image f), m := L.map (CategoryTheory.Limits.image.ι f), m_mono := ⋯, e := L.map (CategoryTheory.Limits.factorThruImage f), fac := ⋯, e_strong_epi := ⋯ }.toMonoIsImage.lift (CategoryTheory.Limits.Image.monoFactorisation (L.map f))

About

Loogle searches Lean and Mathlib definitions and theorems.

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

Usage

Loogle finds definitions and lemmas in various ways:

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

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

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

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

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

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

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

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

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

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

Source code

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

This is Loogle revision 9f11169 serving mathlib revision ce5dd8c