Loogle!

Result

Found 61 declarations mentioning CategoryTheory.Limits.imageSubobject.

CategoryTheory.Limits.imageSubobject 📋 Mathlib.CategoryTheory.Subobject.Limits
{C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Limits.HasImage f] : CategoryTheory.Subobject Y
CategoryTheory.Limits.imageSubobject_mono 📋 Mathlib.CategoryTheory.Subobject.Limits
{C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Mono f] : CategoryTheory.Limits.imageSubobject f = CategoryTheory.Subobject.mk f
CategoryTheory.Limits.imageSubobject_factors_comp_self 📋 Mathlib.CategoryTheory.Subobject.Limits
{C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Limits.HasImage f] {W : C} (k : W ⟶ X) : (CategoryTheory.Limits.imageSubobject f).Factors (CategoryTheory.CategoryStruct.comp k f)
CategoryTheory.Limits.factorThruImageSubobject 📋 Mathlib.CategoryTheory.Subobject.Limits
{C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Limits.HasImage f] : X ⟶ CategoryTheory.Subobject.underlying.obj (CategoryTheory.Limits.imageSubobject f)
CategoryTheory.Limits.imageSubobjectIso 📋 Mathlib.CategoryTheory.Subobject.Limits
{C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Limits.HasImage f] : CategoryTheory.Subobject.underlying.obj (CategoryTheory.Limits.imageSubobject f) ≅ CategoryTheory.Limits.image f
CategoryTheory.Limits.instEpiFactorThruImageSubobjectOfHasEqualizers 📋 Mathlib.CategoryTheory.Subobject.Limits
{C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Limits.HasImage f] [CategoryTheory.Limits.HasEqualizers C] : CategoryTheory.Epi (CategoryTheory.Limits.factorThruImageSubobject f)
CategoryTheory.Limits.imageSubobject_iso_comp 📋 Mathlib.CategoryTheory.Subobject.Limits
{C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} [CategoryTheory.Limits.HasEqualizers C] {X' : C} (h : X' ⟶ X) [CategoryTheory.IsIso h] (f : X ⟶ Y) [CategoryTheory.Limits.HasImage f] : CategoryTheory.Limits.imageSubobject (CategoryTheory.CategoryStruct.comp h f) = CategoryTheory.Limits.imageSubobject f
CategoryTheory.Limits.imageSubobject_comp_le 📋 Mathlib.CategoryTheory.Subobject.Limits
{C : Type u} [CategoryTheory.Category.{v, u} C] {X Y X' : C} (h : X' ⟶ X) (f : X ⟶ Y) [CategoryTheory.Limits.HasImage f] [CategoryTheory.Limits.HasImage (CategoryTheory.CategoryStruct.comp h f)] : CategoryTheory.Limits.imageSubobject (CategoryTheory.CategoryStruct.comp h f) ≤ CategoryTheory.Limits.imageSubobject f
CategoryTheory.Limits.imageSubobject_arrow_comp 📋 Mathlib.CategoryTheory.Subobject.Limits
{C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Limits.HasImage f] : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.factorThruImageSubobject f) (CategoryTheory.Limits.imageSubobject f).arrow = f
CategoryTheory.Limits.imageSubobject_zero 📋 Mathlib.CategoryTheory.Subobject.Limits
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] {A B : C} : CategoryTheory.Limits.imageSubobject 0 = ⊥
CategoryTheory.Limits.imageSubobject_le_mk 📋 Mathlib.CategoryTheory.Subobject.Limits
{C : Type u} [CategoryTheory.Category.{v, u} C] {A B X : C} (g : X ⟶ B) [CategoryTheory.Mono g] (f : A ⟶ B) [CategoryTheory.Limits.HasImage f] (h : A ⟶ X) (w : CategoryTheory.CategoryStruct.comp h g = f) : CategoryTheory.Limits.imageSubobject f ≤ CategoryTheory.Subobject.mk g
CategoryTheory.Limits.imageSubobjectCompIso 📋 Mathlib.CategoryTheory.Subobject.Limits
{C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} [CategoryTheory.Limits.HasEqualizers C] (f : X ⟶ Y) [CategoryTheory.Limits.HasImage f] {Y' : C} (h : Y ⟶ Y') [CategoryTheory.IsIso h] : CategoryTheory.Subobject.underlying.obj (CategoryTheory.Limits.imageSubobject (CategoryTheory.CategoryStruct.comp f h)) ≅ CategoryTheory.Subobject.underlying.obj (CategoryTheory.Limits.imageSubobject f)
CategoryTheory.Limits.imageSubobject_le 📋 Mathlib.CategoryTheory.Subobject.Limits
{C : Type u} [CategoryTheory.Category.{v, u} C] {A B : C} {X : CategoryTheory.Subobject B} (f : A ⟶ B) [CategoryTheory.Limits.HasImage f] (h : A ⟶ CategoryTheory.Subobject.underlying.obj X) (w : CategoryTheory.CategoryStruct.comp h X.arrow = f) : CategoryTheory.Limits.imageSubobject f ≤ X
CategoryTheory.Limits.imageSubobject_arrow_comp_assoc 📋 Mathlib.CategoryTheory.Subobject.Limits
{C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Limits.HasImage f] {Z : C} (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.factorThruImageSubobject f) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.imageSubobject f).arrow h) = CategoryTheory.CategoryStruct.comp f h
CategoryTheory.Limits.imageSubobject_arrow' 📋 Mathlib.CategoryTheory.Subobject.Limits
{C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Limits.HasImage f] : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.imageSubobjectIso f).inv (CategoryTheory.Limits.imageSubobject f).arrow = CategoryTheory.Limits.image.ι f
CategoryTheory.Limits.imageSubobjectMap 📋 Mathlib.CategoryTheory.Subobject.Limits
{C : Type u} [CategoryTheory.Category.{v, u} C] {W X Y Z : C} {f : W ⟶ X} [CategoryTheory.Limits.HasImage f] {g : Y ⟶ Z} [CategoryTheory.Limits.HasImage g] (sq : CategoryTheory.Arrow.mk f ⟶ CategoryTheory.Arrow.mk g) [CategoryTheory.Limits.HasImageMap sq] : CategoryTheory.Subobject.underlying.obj (CategoryTheory.Limits.imageSubobject f) ⟶ CategoryTheory.Subobject.underlying.obj (CategoryTheory.Limits.imageSubobject g)
CategoryTheory.Limits.factorThruImageSubobject_comp_self 📋 Mathlib.CategoryTheory.Subobject.Limits
{C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Limits.HasImage f] {W : C} (k : W ⟶ X) (h : (CategoryTheory.Limits.imageSubobject f).Factors (CategoryTheory.CategoryStruct.comp k f)) : (CategoryTheory.Limits.imageSubobject f).factorThru (CategoryTheory.CategoryStruct.comp k f) h = CategoryTheory.CategoryStruct.comp k (CategoryTheory.Limits.factorThruImageSubobject f)
CategoryTheory.Limits.imageSubobject_comp_le_epi_of_epi 📋 Mathlib.CategoryTheory.Subobject.Limits
{C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} [CategoryTheory.Limits.HasEqualizers C] {X' : C} (h : X' ⟶ X) [CategoryTheory.Epi h] (f : X ⟶ Y) [CategoryTheory.Limits.HasImage f] [CategoryTheory.Limits.HasImage (CategoryTheory.CategoryStruct.comp h f)] : CategoryTheory.Epi ((CategoryTheory.Limits.imageSubobject (CategoryTheory.CategoryStruct.comp h f)).ofLE (CategoryTheory.Limits.imageSubobject f) ⋯)
CategoryTheory.Limits.imageSubobject_arrow 📋 Mathlib.CategoryTheory.Subobject.Limits
{C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Limits.HasImage f] : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.imageSubobjectIso f).hom (CategoryTheory.Limits.image.ι f) = (CategoryTheory.Limits.imageSubobject f).arrow
CategoryTheory.Limits.imageSubobject_arrow'_assoc 📋 Mathlib.CategoryTheory.Subobject.Limits
{C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Limits.HasImage f] {Z : C} (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.imageSubobjectIso f).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.imageSubobject f).arrow h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.image.ι f) h
CategoryTheory.Limits.factorThruImageSubobject_comp_self_assoc 📋 Mathlib.CategoryTheory.Subobject.Limits
{C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Limits.HasImage f] {W W' : C} (k : W ⟶ W') (k' : W' ⟶ X) (h : (CategoryTheory.Limits.imageSubobject f).Factors (CategoryTheory.CategoryStruct.comp k (CategoryTheory.CategoryStruct.comp k' f))) : (CategoryTheory.Limits.imageSubobject f).factorThru (CategoryTheory.CategoryStruct.comp k (CategoryTheory.CategoryStruct.comp k' f)) h = CategoryTheory.CategoryStruct.comp k (CategoryTheory.CategoryStruct.comp k' (CategoryTheory.Limits.factorThruImageSubobject f))
CategoryTheory.Limits.imageSubobject_arrow_assoc 📋 Mathlib.CategoryTheory.Subobject.Limits
{C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Limits.HasImage f] {Z : C} (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.imageSubobjectIso f).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.image.ι f) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.imageSubobject f).arrow h
CategoryTheory.Limits.imageSubobjectMap_arrow 📋 Mathlib.CategoryTheory.Subobject.Limits
{C : Type u} [CategoryTheory.Category.{v, u} C] {W X Y Z : C} {f : W ⟶ X} [CategoryTheory.Limits.HasImage f] {g : Y ⟶ Z} [CategoryTheory.Limits.HasImage g] (sq : CategoryTheory.Arrow.mk f ⟶ CategoryTheory.Arrow.mk g) [CategoryTheory.Limits.HasImageMap sq] : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.imageSubobjectMap sq) (CategoryTheory.Limits.imageSubobject g).arrow = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.imageSubobject f).arrow (CategoryTheory.Arrow.Hom.right sq)
CategoryTheory.Limits.imageSubobject_arrow_comp_eq_zero 📋 Mathlib.CategoryTheory.Subobject.Limits
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {X Y Z : C} {f : X ⟶ Y} {g : Y ⟶ Z} [CategoryTheory.Limits.HasImage f] [CategoryTheory.Epi (CategoryTheory.Limits.factorThruImageSubobject f)] (h : CategoryTheory.CategoryStruct.comp f g = 0) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.imageSubobject f).arrow g = 0
CategoryTheory.Limits.imageSubobject_zero_arrow 📋 Mathlib.CategoryTheory.Subobject.Limits
{C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] : (CategoryTheory.Limits.imageSubobject 0).arrow = 0
CategoryTheory.Limits.imageSubobjectCompIso_inv_arrow 📋 Mathlib.CategoryTheory.Subobject.Limits
{C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} [CategoryTheory.Limits.HasEqualizers C] (f : X ⟶ Y) [CategoryTheory.Limits.HasImage f] {Y' : C} (h : Y ⟶ Y') [CategoryTheory.IsIso h] : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.imageSubobjectCompIso f h).inv (CategoryTheory.Limits.imageSubobject (CategoryTheory.CategoryStruct.comp f h)).arrow = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.imageSubobject f).arrow h
CategoryTheory.Limits.imageSubobjectMap_arrow_assoc 📋 Mathlib.CategoryTheory.Subobject.Limits
{C : Type u} [CategoryTheory.Category.{v, u} C] {W X Y Z : C} {f : W ⟶ X} [CategoryTheory.Limits.HasImage f] {g : Y ⟶ Z} [CategoryTheory.Limits.HasImage g] (sq : CategoryTheory.Arrow.mk f ⟶ CategoryTheory.Arrow.mk g) [CategoryTheory.Limits.HasImageMap sq] {Z✝ : C} (h : Z ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.imageSubobjectMap sq) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.imageSubobject g).arrow h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.imageSubobject f).arrow (CategoryTheory.CategoryStruct.comp (CategoryTheory.Arrow.Hom.right sq) h)
CategoryTheory.Limits.imageSubobjectCompIso_hom_arrow 📋 Mathlib.CategoryTheory.Subobject.Limits
{C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} [CategoryTheory.Limits.HasEqualizers C] (f : X ⟶ Y) [CategoryTheory.Limits.HasImage f] {Y' : C} (h : Y ⟶ Y') [CategoryTheory.IsIso h] : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.imageSubobjectCompIso f h).hom (CategoryTheory.Limits.imageSubobject f).arrow = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.imageSubobject (CategoryTheory.CategoryStruct.comp f h)).arrow (CategoryTheory.inv h)
CategoryTheory.Limits.imageSubobject_arrow_comp_apply 📋 Mathlib.CategoryTheory.Subobject.Limits
{C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Limits.HasImage f] {F : C → C → Type uF} {carrier : C → Type w} {instFunLike : (X Y : C) → FunLike (F X Y) (carrier X) (carrier Y)} [inst : CategoryTheory.ConcreteCategory C F] (x : carrier X) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.imageSubobject f).arrow) ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.factorThruImageSubobject f)) x) = (CategoryTheory.ConcreteCategory.hom f) x
CategoryTheory.Limits.imageSubobjectCompIso_inv_arrow_assoc 📋 Mathlib.CategoryTheory.Subobject.Limits
{C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} [CategoryTheory.Limits.HasEqualizers C] (f : X ⟶ Y) [CategoryTheory.Limits.HasImage f] {Y' : C} (h : Y ⟶ Y') [CategoryTheory.IsIso h] {Z : C} (h✝ : Y' ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.imageSubobjectCompIso f h).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.imageSubobject (CategoryTheory.CategoryStruct.comp f h)).arrow h✝) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.imageSubobject f).arrow (CategoryTheory.CategoryStruct.comp h h✝)
CategoryTheory.Limits.imageSubobjectCompIso_hom_arrow_assoc 📋 Mathlib.CategoryTheory.Subobject.Limits
{C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} [CategoryTheory.Limits.HasEqualizers C] (f : X ⟶ Y) [CategoryTheory.Limits.HasImage f] {Y' : C} (h : Y ⟶ Y') [CategoryTheory.IsIso h] {Z : C} (h✝ : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.imageSubobjectCompIso f h).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.imageSubobject f).arrow h✝) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.imageSubobject (CategoryTheory.CategoryStruct.comp f h)).arrow (CategoryTheory.CategoryStruct.comp (CategoryTheory.inv h) h✝)
CategoryTheory.Limits.imageSubobjectIso_comp_image_map 📋 Mathlib.CategoryTheory.Subobject.Limits
{C : Type u} [CategoryTheory.Category.{v, u} C] {W X Y Z : C} {f : W ⟶ X} [CategoryTheory.Limits.HasImage f] {g : Y ⟶ Z} [CategoryTheory.Limits.HasImage g] (sq : CategoryTheory.Arrow.mk f ⟶ CategoryTheory.Arrow.mk g) [CategoryTheory.Limits.HasImageMap sq] : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.imageSubobjectIso (CategoryTheory.Arrow.mk f).hom).hom (CategoryTheory.Limits.image.map sq) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.imageSubobjectMap sq) (CategoryTheory.Limits.imageSubobjectIso g).hom
CategoryTheory.Limits.image_map_comp_imageSubobjectIso_inv 📋 Mathlib.CategoryTheory.Subobject.Limits
{C : Type u} [CategoryTheory.Category.{v, u} C] {W X Y Z : C} {f : W ⟶ X} [CategoryTheory.Limits.HasImage f] {g : Y ⟶ Z} [CategoryTheory.Limits.HasImage g] (sq : CategoryTheory.Arrow.mk f ⟶ CategoryTheory.Arrow.mk g) [CategoryTheory.Limits.HasImageMap sq] : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.image.map sq) (CategoryTheory.Limits.imageSubobjectIso (CategoryTheory.Arrow.mk g).hom).inv = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.imageSubobjectIso f).inv (CategoryTheory.Limits.imageSubobjectMap sq)
image_le_kernel 📋 Mathlib.Algebra.Homology.ImageToKernel
{V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {A B C : V} (f : A ⟶ B) [CategoryTheory.Limits.HasImage f] (g : B ⟶ C) [CategoryTheory.Limits.HasKernel g] (w : CategoryTheory.CategoryStruct.comp f g = 0) : CategoryTheory.Limits.imageSubobject f ≤ CategoryTheory.Limits.kernelSubobject g
imageToKernel 📋 Mathlib.Algebra.Homology.ImageToKernel
{V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {A B C : V} (f : A ⟶ B) [CategoryTheory.Limits.HasImage f] (g : B ⟶ C) [CategoryTheory.Limits.HasKernel g] (w : CategoryTheory.CategoryStruct.comp f g = 0) : CategoryTheory.Subobject.underlying.obj (CategoryTheory.Limits.imageSubobject f) ⟶ CategoryTheory.Subobject.underlying.obj (CategoryTheory.Limits.kernelSubobject g)
instMonoImageToKernel 📋 Mathlib.Algebra.Homology.ImageToKernel
{V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {A B C : V} (f : A ⟶ B) [CategoryTheory.Limits.HasImage f] (g : B ⟶ C) [CategoryTheory.Limits.HasKernel g] (w : CategoryTheory.CategoryStruct.comp f g = 0) : CategoryTheory.Mono (imageToKernel f g w)
imageToKernel_epi_of_zero_of_mono 📋 Mathlib.Algebra.Homology.ImageToKernel
{V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {A B C : V} (g : B ⟶ C) [CategoryTheory.Limits.HasKernels V] [CategoryTheory.Limits.HasZeroObject V] [CategoryTheory.Mono g] : CategoryTheory.Epi (imageToKernel 0 g ⋯)
subobject_ofLE_as_imageToKernel 📋 Mathlib.Algebra.Homology.ImageToKernel
{V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {A B C : V} (f : A ⟶ B) [CategoryTheory.Limits.HasImage f] (g : B ⟶ C) [CategoryTheory.Limits.HasKernel g] (w : CategoryTheory.CategoryStruct.comp f g = 0) (h : CategoryTheory.Limits.imageSubobject f ≤ CategoryTheory.Limits.kernelSubobject g) : (CategoryTheory.Limits.imageSubobject f).ofLE (CategoryTheory.Limits.kernelSubobject g) h = imageToKernel f g w
factorThruImageSubobject_comp_imageToKernel 📋 Mathlib.Algebra.Homology.ImageToKernel
{V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {A B C : V} (f : A ⟶ B) [CategoryTheory.Limits.HasImage f] (g : B ⟶ C) [CategoryTheory.Limits.HasKernel g] (w : CategoryTheory.CategoryStruct.comp f g = 0) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.factorThruImageSubobject f) (imageToKernel f g w) = CategoryTheory.Limits.factorThruKernelSubobject g f w
imageToKernel_arrow 📋 Mathlib.Algebra.Homology.ImageToKernel
{V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {A B C : V} (f : A ⟶ B) [CategoryTheory.Limits.HasImage f] (g : B ⟶ C) [CategoryTheory.Limits.HasKernel g] (w : CategoryTheory.CategoryStruct.comp f g = 0) : CategoryTheory.CategoryStruct.comp (imageToKernel f g w) (CategoryTheory.Limits.kernelSubobject g).arrow = (CategoryTheory.Limits.imageSubobject f).arrow
imageToKernel_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 ⋯)
imageToKernel_arrow_assoc 📋 Mathlib.Algebra.Homology.ImageToKernel
{V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {A B C : V} (f : A ⟶ B) [CategoryTheory.Limits.HasImage f] (g : B ⟶ C) [CategoryTheory.Limits.HasKernel g] (w : CategoryTheory.CategoryStruct.comp f g = 0) {Z : V} (h : B ⟶ Z) : CategoryTheory.CategoryStruct.comp (imageToKernel f g w) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernelSubobject g).arrow h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.imageSubobject f).arrow h
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_left 📋 Mathlib.Algebra.Homology.ImageToKernel
{V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {A B C : V} (g : B ⟶ C) [CategoryTheory.Limits.HasKernels V] [CategoryTheory.Limits.HasZeroObject V] {w : CategoryTheory.CategoryStruct.comp 0 g = 0} : imageToKernel 0 g w = 0
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_arrow_apply 📋 Mathlib.Algebra.Homology.ImageToKernel
{V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {A B C : V} (f : A ⟶ B) [CategoryTheory.Limits.HasImage f] (g : B ⟶ C) [CategoryTheory.Limits.HasKernel g] (w : CategoryTheory.CategoryStruct.comp f g = 0) {F : V → V → Type uF} {carrier : V → Type w} {instFunLike : (X Y : V) → FunLike (F X Y) (carrier X) (carrier Y)} [inst : CategoryTheory.ConcreteCategory V F] (x : carrier (CategoryTheory.Subobject.underlying.obj (CategoryTheory.Limits.imageSubobject f))) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.kernelSubobject g).arrow) ((CategoryTheory.ConcreteCategory.hom (imageToKernel f g w)) x) = (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.imageSubobject f).arrow) x
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)
CategoryTheory.ShortComplex.exact_iff_image_eq_kernel 📋 Mathlib.CategoryTheory.Abelian.Exact
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex C) : S.Exact ↔ CategoryTheory.Limits.imageSubobject S.f = CategoryTheory.Limits.kernelSubobject S.g
CategoryTheory.ShortComplex.Exact.isIso_imageToKernel 📋 Mathlib.CategoryTheory.Abelian.Exact
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex C) (hS : S.Exact) : CategoryTheory.IsIso (imageToKernel S.f S.g ⋯)
CategoryTheory.ShortComplex.exact_iff_epi_imageToKernel 📋 Mathlib.CategoryTheory.Abelian.Exact
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex C) : S.Exact ↔ CategoryTheory.Epi (imageToKernel S.f S.g ⋯)
CategoryTheory.ShortComplex.exact_iff_isIso_imageToKernel 📋 Mathlib.CategoryTheory.Abelian.Exact
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex C) : S.Exact ↔ CategoryTheory.IsIso (imageToKernel S.f S.g ⋯)
ModuleCat.cokernel_π_imageSubobject_ext 📋 Mathlib.Algebra.Category.ModuleCat.Subobject
{R : Type u} [Ring R] {L M N : ModuleCat R} (f : L ⟶ M) [CategoryTheory.Limits.HasImage f] (g : CategoryTheory.Subobject.underlying.obj (CategoryTheory.Limits.imageSubobject f) ⟶ N) [CategoryTheory.Limits.HasCokernel g] {x y : ↑N} (l : ↑L) (w : x = y + (CategoryTheory.ConcreteCategory.hom g) ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.factorThruImageSubobject f)) l)) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.cokernel.π g)) x = (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.cokernel.π g)) y
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)
imageToKernel_unop 📋 Mathlib.Algebra.Homology.Opposite
{V : Type u_1} [CategoryTheory.Category.{v_1, u_1} V] [CategoryTheory.Abelian V] {X Y Z : Vᵒᵖ} (f : X ⟶ Y) (g : Y ⟶ Z) (w : CategoryTheory.CategoryStruct.comp f g = 0) : imageToKernel g.unop f.unop ⋯ = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.imageSubobjectIso g.unop ≪≫ (CategoryTheory.imageUnopUnop g).symm).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.cokernel.desc f (CategoryTheory.Limits.factorThruImage g) ⋯).unop (CategoryTheory.Limits.kernelSubobjectIso f.unop ≪≫ CategoryTheory.kernelUnopUnop f).inv)
imageToKernel_op 📋 Mathlib.Algebra.Homology.Opposite
{V : Type u_1} [CategoryTheory.Category.{v_1, u_1} V] [CategoryTheory.Abelian V] {X Y Z : V} (f : X ⟶ Y) (g : Y ⟶ Z) (w : CategoryTheory.CategoryStruct.comp f g = 0) : imageToKernel g.op f.op ⋯ = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.imageSubobjectIso g.op ≪≫ (CategoryTheory.imageOpOp g).symm).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.cokernel.desc f (CategoryTheory.Limits.factorThruImage g) ⋯).op (CategoryTheory.Limits.kernelSubobjectIso f.op ≪≫ CategoryTheory.kernelOpOp f).inv)

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:

By constant:
🔍 Real.sin
finds all lemmas whose statement somehow mentions the sine function.
By lemma name substring:
🔍 "differ"
finds all lemmas that have "differ" somewhere in their lemma name.
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
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.
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