Loogle!

Result

Found 67 declarations mentioning CategoryTheory.Abelian.coimage.

• CategoryTheory.Abelian.coimage 📋 Mathlib.CategoryTheory.Abelian.Images
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {P Q : C} (f : P ⟶ Q) [CategoryTheory.Limits.HasKernel f] [CategoryTheory.Limits.HasCokernel (CategoryTheory.Limits.kernel.ι f)] : C
• CategoryTheory.Abelian.factorThruCoimage 📋 Mathlib.CategoryTheory.Abelian.Images
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {P Q : C} (f : P ⟶ Q) [CategoryTheory.Limits.HasKernel f] [CategoryTheory.Limits.HasCokernel (CategoryTheory.Limits.kernel.ι f)] : CategoryTheory.Abelian.coimage f ⟶ Q
• CategoryTheory.Abelian.coimage.π 📋 Mathlib.CategoryTheory.Abelian.Images
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {P Q : C} (f : P ⟶ Q) [CategoryTheory.Limits.HasKernel f] [CategoryTheory.Limits.HasCokernel (CategoryTheory.Limits.kernel.ι f)] : P ⟶ CategoryTheory.Abelian.coimage f
• CategoryTheory.Abelian.epi_factorThruCoimage 📋 Mathlib.CategoryTheory.Abelian.Images
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {P Q : C} (f : P ⟶ Q) [CategoryTheory.Limits.HasKernel f] [CategoryTheory.Limits.HasCokernel (CategoryTheory.Limits.kernel.ι f)] [CategoryTheory.Epi f] : CategoryTheory.Epi (CategoryTheory.Abelian.factorThruCoimage f)
• CategoryTheory.Abelian.coimage.fac 📋 Mathlib.CategoryTheory.Abelian.Images
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {P Q : C} (f : P ⟶ Q) [CategoryTheory.Limits.HasKernel f] [CategoryTheory.Limits.HasCokernel (CategoryTheory.Limits.kernel.ι f)] : CategoryTheory.CategoryStruct.comp (CategoryTheory.Abelian.coimage.π f) (CategoryTheory.Abelian.factorThruCoimage f) = f
• CategoryTheory.Abelian.coimageImageComparison 📋 Mathlib.CategoryTheory.Abelian.Images
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {P Q : C} (f : P ⟶ Q) [CategoryTheory.Limits.HasCokernel f] [CategoryTheory.Limits.HasKernel f] [CategoryTheory.Limits.HasKernel (CategoryTheory.Limits.cokernel.π f)] [CategoryTheory.Limits.HasCokernel (CategoryTheory.Limits.kernel.ι f)] : CategoryTheory.Abelian.coimage f ⟶ CategoryTheory.Abelian.image f
• CategoryTheory.Abelian.coimageImageComparison' 📋 Mathlib.CategoryTheory.Abelian.Images
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {P Q : C} (f : P ⟶ Q) [CategoryTheory.Limits.HasCokernel f] [CategoryTheory.Limits.HasKernel f] [CategoryTheory.Limits.HasKernel (CategoryTheory.Limits.cokernel.π f)] [CategoryTheory.Limits.HasCokernel (CategoryTheory.Limits.kernel.ι f)] : CategoryTheory.Abelian.coimage f ⟶ CategoryTheory.Abelian.image f
• CategoryTheory.Abelian.coimageImageComparison_eq_coimageImageComparison' 📋 Mathlib.CategoryTheory.Abelian.Images
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {P Q : C} (f : P ⟶ Q) [CategoryTheory.Limits.HasCokernel f] [CategoryTheory.Limits.HasKernel f] [CategoryTheory.Limits.HasKernel (CategoryTheory.Limits.cokernel.π f)] [CategoryTheory.Limits.HasCokernel (CategoryTheory.Limits.kernel.ι f)] : CategoryTheory.Abelian.coimageImageComparison f = CategoryTheory.Abelian.coimageImageComparison' f
• CategoryTheory.Abelian.coimageImageComparisonFunctor_obj 📋 Mathlib.CategoryTheory.Abelian.Images
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasKernels C] [CategoryTheory.Limits.HasCokernels C] (f : CategoryTheory.Arrow C) : CategoryTheory.Abelian.coimageImageComparisonFunctor.obj f = CategoryTheory.Arrow.mk (CategoryTheory.Abelian.coimageImageComparison f.hom)
• CategoryTheory.Abelian.coimage_image_factorisation 📋 Mathlib.CategoryTheory.Abelian.Images
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {P Q : C} (f : P ⟶ Q) [CategoryTheory.Limits.HasCokernel f] [CategoryTheory.Limits.HasKernel f] [CategoryTheory.Limits.HasKernel (CategoryTheory.Limits.cokernel.π f)] [CategoryTheory.Limits.HasCokernel (CategoryTheory.Limits.kernel.ι f)] : CategoryTheory.CategoryStruct.comp (CategoryTheory.Abelian.coimage.π f) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Abelian.coimageImageComparison f) (CategoryTheory.Abelian.image.ι f)) = f
• CategoryTheory.Abelian.coimage_image_factorisation_assoc 📋 Mathlib.CategoryTheory.Abelian.Images
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {P Q : C} (f : P ⟶ Q) [CategoryTheory.Limits.HasCokernel f] [CategoryTheory.Limits.HasKernel f] [CategoryTheory.Limits.HasKernel (CategoryTheory.Limits.cokernel.π f)] [CategoryTheory.Limits.HasCokernel (CategoryTheory.Limits.kernel.ι f)] {Z : C} (h : Q ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Abelian.coimage.π f) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Abelian.coimageImageComparison f) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Abelian.image.ι f) h)) = CategoryTheory.CategoryStruct.comp f h
• CategoryTheory.Abelian.coimageImageComparisonFunctor_map 📋 Mathlib.CategoryTheory.Abelian.Images
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasKernels C] [CategoryTheory.Limits.HasCokernels C] {f g : CategoryTheory.Arrow C} (η : f ⟶ g) : CategoryTheory.Abelian.coimageImageComparisonFunctor.map η = CategoryTheory.Arrow.homMk (CategoryTheory.Limits.cokernel.map (CategoryTheory.Limits.kernel.ι f.hom) (CategoryTheory.Limits.kernel.ι g.hom) (CategoryTheory.Limits.kernel.map f.hom g.hom (CategoryTheory.Arrow.Hom.left η) (CategoryTheory.Arrow.Hom.right η) ⋯) (CategoryTheory.Arrow.Hom.left η) ⋯) (CategoryTheory.Limits.kernel.map (CategoryTheory.Limits.cokernel.π f.hom) (CategoryTheory.Limits.cokernel.π g.hom) (CategoryTheory.Arrow.Hom.right η) (CategoryTheory.Limits.cokernel.map f.hom g.hom (CategoryTheory.Arrow.Hom.left η) (CategoryTheory.Arrow.Hom.right η) ⋯) ⋯) ⋯
• CategoryTheory.NonPreadditiveAbelian.instMonoFactorThruCoimage 📋 Mathlib.CategoryTheory.Abelian.NonPreadditive
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.NonPreadditiveAbelian C] {P Q : C} (f : P ⟶ Q) : CategoryTheory.Mono (CategoryTheory.Abelian.factorThruCoimage f)
• CategoryTheory.NonPreadditiveAbelian.isIso_factorThruCoimage 📋 Mathlib.CategoryTheory.Abelian.NonPreadditive
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.NonPreadditiveAbelian C] {P Q : C} (f : P ⟶ Q) [CategoryTheory.Epi f] : CategoryTheory.IsIso (CategoryTheory.Abelian.factorThruCoimage f)
• CategoryTheory.Abelian.coim_obj 📋 Mathlib.CategoryTheory.Abelian.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (f : CategoryTheory.Arrow C) : CategoryTheory.Abelian.coim.obj f = CategoryTheory.Abelian.coimage f.hom
• CategoryTheory.Abelian.coimageStrongEpiMonoFactorisation_I 📋 Mathlib.CategoryTheory.Abelian.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {P Q : C} (f : P ⟶ Q) : (CategoryTheory.Abelian.coimageStrongEpiMonoFactorisation f).I = CategoryTheory.Abelian.coimage f
• CategoryTheory.Abelian.coimageStrongEpiMonoFactorisation_e 📋 Mathlib.CategoryTheory.Abelian.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {P Q : C} (f : P ⟶ Q) : (CategoryTheory.Abelian.coimageStrongEpiMonoFactorisation f).e = CategoryTheory.Abelian.coimage.π f
• CategoryTheory.Abelian.coimageStrongEpiMonoFactorisation_m 📋 Mathlib.CategoryTheory.Abelian.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {P Q : C} (f : P ⟶ Q) : (CategoryTheory.Abelian.coimageStrongEpiMonoFactorisation f).m = CategoryTheory.Abelian.factorThruCoimage f
• CategoryTheory.Abelian.coimageIsoImage' 📋 Mathlib.CategoryTheory.Abelian.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {X Y : C} (f : X ⟶ Y) : CategoryTheory.Abelian.coimage f ≅ CategoryTheory.Limits.image f
• CategoryTheory.Abelian.coimageIsoImage 📋 Mathlib.CategoryTheory.Abelian.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {X Y : C} (f : X ⟶ Y) : CategoryTheory.Abelian.coimage f ≅ CategoryTheory.Abelian.image f
• CategoryTheory.Abelian.instMonoFactorThruCoimage 📋 Mathlib.CategoryTheory.Abelian.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {P Q : C} (f : P ⟶ Q) : CategoryTheory.Mono (CategoryTheory.Abelian.factorThruCoimage f)
• CategoryTheory.Abelian.isIso_factorThruCoimage 📋 Mathlib.CategoryTheory.Abelian.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {P Q : C} (f : P ⟶ Q) [CategoryTheory.Epi f] : CategoryTheory.IsIso (CategoryTheory.Abelian.factorThruCoimage f)
• CategoryTheory.Abelian.coimIsoIm_inv_app 📋 Mathlib.CategoryTheory.Abelian.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (X : CategoryTheory.Arrow C) : CategoryTheory.Abelian.coimIsoIm.inv.app X = CategoryTheory.inv (CategoryTheory.Abelian.coimageImageComparison X.hom)
• 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.Abelian.ofCoimageImageComparisonIsIso 📋 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.HasFiniteProducts C] : CategoryTheory.Abelian C
• CategoryTheory.Abelian.OfCoimageImageComparisonIsIso.imageFactorisation 📋 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.ImageFactorisation f
• CategoryTheory.Abelian.OfCoimageImageComparisonIsIso.isNormalEpiCategory 📋 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.HasFiniteProducts C] : CategoryTheory.IsNormalEpiCategory C
• CategoryTheory.Abelian.OfCoimageImageComparisonIsIso.isNormalMonoCategory 📋 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.HasFiniteProducts C] : CategoryTheory.IsNormalMonoCategory C
• CategoryTheory.Abelian.coim_map 📋 Mathlib.CategoryTheory.Abelian.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {f g : CategoryTheory.Arrow C} (u : f ⟶ g) : CategoryTheory.Abelian.coim.map u = CategoryTheory.Limits.cokernel.desc (CategoryTheory.Limits.kernel.ι f.hom) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Arrow.Hom.left u) (CategoryTheory.Abelian.coimage.π g.hom)) ⋯
• CategoryTheory.Abelian.OfCoimageImageComparisonIsIso.instIsIsoEImageMonoFactorisationOfHasZeroObjectOfMonoOfCoimageImageComparison 📋 Mathlib.CategoryTheory.Abelian.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasKernels C] [CategoryTheory.Limits.HasCokernels C] [CategoryTheory.Limits.HasZeroObject C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Mono f] [CategoryTheory.IsIso (CategoryTheory.Abelian.coimageImageComparison f)] : CategoryTheory.IsIso (CategoryTheory.Abelian.OfCoimageImageComparisonIsIso.imageMonoFactorisation f).e
• CategoryTheory.Abelian.instIsIsoCoimageImageComparison 📋 Mathlib.CategoryTheory.Abelian.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {X Y : C} (f : X ⟶ Y) : CategoryTheory.IsIso (CategoryTheory.Abelian.coimageImageComparison f)
• CategoryTheory.Abelian.coimageIsoImage'_hom 📋 Mathlib.CategoryTheory.Abelian.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {X Y : C} (f : X ⟶ Y) : (CategoryTheory.Abelian.coimageIsoImage' f).hom = CategoryTheory.Limits.cokernel.desc (CategoryTheory.Limits.kernel.ι f) (CategoryTheory.Limits.factorThruImage f) ⋯
• CategoryTheory.Abelian.factorThruImage_comp_coimageIsoImage'_inv 📋 Mathlib.CategoryTheory.Abelian.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {X Y : C} (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.factorThruImage f) (CategoryTheory.Abelian.coimageIsoImage' f).inv = CategoryTheory.Limits.cokernel.π (CategoryTheory.Limits.kernel.ι f)
• CategoryTheory.Abelian.coimage.comp_π_eq_zero 📋 Mathlib.CategoryTheory.Abelian.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {X Y : C} (f : X ⟶ Y) {Z : C} (g : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp f (CategoryTheory.Abelian.coimage.π g) = 0 ↔ CategoryTheory.CategoryStruct.comp f g = 0
• CategoryTheory.Abelian.comp_coimage_π_eq_zero 📋 Mathlib.CategoryTheory.Abelian.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {P Q : C} {f : P ⟶ Q} {R : C} {g : Q ⟶ R} (h : CategoryTheory.CategoryStruct.comp f g = 0) : CategoryTheory.CategoryStruct.comp f (CategoryTheory.Abelian.coimage.π g) = 0
• CategoryTheory.Abelian.PreservesCoimage.iso 📋 Mathlib.CategoryTheory.Limits.Preserves.Shapes.AbelianImages
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasZeroMorphisms C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Limits.HasZeroMorphisms D] (F : CategoryTheory.Functor C D) [F.PreservesZeroMorphisms] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Limits.HasKernel f] [CategoryTheory.Limits.HasCokernel (CategoryTheory.Limits.kernel.ι f)] [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair f 0) F] [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair (CategoryTheory.Limits.kernel.ι f) 0) F] [CategoryTheory.Limits.HasKernel (F.map f)] [CategoryTheory.Limits.HasCokernel (CategoryTheory.Limits.kernel.ι (F.map f))] : F.obj (CategoryTheory.Abelian.coimage f) ≅ CategoryTheory.Abelian.coimage (F.map f)
• CategoryTheory.Abelian.PreservesCoimage.factorThruCoimage_iso_hom 📋 Mathlib.CategoryTheory.Limits.Preserves.Shapes.AbelianImages
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasZeroMorphisms C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Limits.HasZeroMorphisms D] (F : CategoryTheory.Functor C D) [F.PreservesZeroMorphisms] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Limits.HasKernel f] [CategoryTheory.Limits.HasCokernel (CategoryTheory.Limits.kernel.ι f)] [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair f 0) F] [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair (CategoryTheory.Limits.kernel.ι f) 0) F] [CategoryTheory.Limits.HasKernel (F.map f)] [CategoryTheory.Limits.HasCokernel (CategoryTheory.Limits.kernel.ι (F.map f))] : CategoryTheory.CategoryStruct.comp (CategoryTheory.Abelian.PreservesCoimage.iso F f).hom (CategoryTheory.Abelian.factorThruCoimage (F.map f)) = F.map (CategoryTheory.Abelian.factorThruCoimage f)
• CategoryTheory.Abelian.PreservesCoimage.iso_inv_π 📋 Mathlib.CategoryTheory.Limits.Preserves.Shapes.AbelianImages
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasZeroMorphisms C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Limits.HasZeroMorphisms D] (F : CategoryTheory.Functor C D) [F.PreservesZeroMorphisms] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Limits.HasKernel f] [CategoryTheory.Limits.HasCokernel (CategoryTheory.Limits.kernel.ι f)] [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair f 0) F] [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair (CategoryTheory.Limits.kernel.ι f) 0) F] [CategoryTheory.Limits.HasKernel (F.map f)] [CategoryTheory.Limits.HasCokernel (CategoryTheory.Limits.kernel.ι (F.map f))] : CategoryTheory.CategoryStruct.comp (CategoryTheory.Abelian.coimage.π (F.map f)) (CategoryTheory.Abelian.PreservesCoimage.iso F f).inv = F.map (CategoryTheory.Abelian.coimage.π f)
• CategoryTheory.Abelian.PreservesCoimage.factorThruCoimage_iso_inv 📋 Mathlib.CategoryTheory.Limits.Preserves.Shapes.AbelianImages
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasZeroMorphisms C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Limits.HasZeroMorphisms D] (F : CategoryTheory.Functor C D) [F.PreservesZeroMorphisms] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Limits.HasKernel f] [CategoryTheory.Limits.HasCokernel (CategoryTheory.Limits.kernel.ι f)] [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair f 0) F] [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair (CategoryTheory.Limits.kernel.ι f) 0) F] [CategoryTheory.Limits.HasKernel (F.map f)] [CategoryTheory.Limits.HasCokernel (CategoryTheory.Limits.kernel.ι (F.map f))] : CategoryTheory.CategoryStruct.comp (CategoryTheory.Abelian.PreservesCoimage.iso F f).inv (F.map (CategoryTheory.Abelian.factorThruCoimage f)) = CategoryTheory.Abelian.factorThruCoimage (F.map f)
• CategoryTheory.Abelian.PreservesCoimage.iso_hom_π 📋 Mathlib.CategoryTheory.Limits.Preserves.Shapes.AbelianImages
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasZeroMorphisms C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Limits.HasZeroMorphisms D] (F : CategoryTheory.Functor C D) [F.PreservesZeroMorphisms] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Limits.HasKernel f] [CategoryTheory.Limits.HasCokernel (CategoryTheory.Limits.kernel.ι f)] [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair f 0) F] [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair (CategoryTheory.Limits.kernel.ι f) 0) F] [CategoryTheory.Limits.HasKernel (F.map f)] [CategoryTheory.Limits.HasCokernel (CategoryTheory.Limits.kernel.ι (F.map f))] : CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.Abelian.coimage.π f)) (CategoryTheory.Abelian.PreservesCoimage.iso F f).hom = CategoryTheory.Abelian.coimage.π (F.map f)
• CategoryTheory.Abelian.PreservesCoimage.factorThruCoimage_iso_hom_assoc 📋 Mathlib.CategoryTheory.Limits.Preserves.Shapes.AbelianImages
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasZeroMorphisms C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Limits.HasZeroMorphisms D] (F : CategoryTheory.Functor C D) [F.PreservesZeroMorphisms] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Limits.HasKernel f] [CategoryTheory.Limits.HasCokernel (CategoryTheory.Limits.kernel.ι f)] [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair f 0) F] [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair (CategoryTheory.Limits.kernel.ι f) 0) F] [CategoryTheory.Limits.HasKernel (F.map f)] [CategoryTheory.Limits.HasCokernel (CategoryTheory.Limits.kernel.ι (F.map f))] {Z : D} (h : F.obj Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Abelian.PreservesCoimage.iso F f).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Abelian.factorThruCoimage (F.map f)) h) = CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.Abelian.factorThruCoimage f)) h
• CategoryTheory.Abelian.PreservesCoimage.iso_inv_π_assoc 📋 Mathlib.CategoryTheory.Limits.Preserves.Shapes.AbelianImages
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasZeroMorphisms C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Limits.HasZeroMorphisms D] (F : CategoryTheory.Functor C D) [F.PreservesZeroMorphisms] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Limits.HasKernel f] [CategoryTheory.Limits.HasCokernel (CategoryTheory.Limits.kernel.ι f)] [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair f 0) F] [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair (CategoryTheory.Limits.kernel.ι f) 0) F] [CategoryTheory.Limits.HasKernel (F.map f)] [CategoryTheory.Limits.HasCokernel (CategoryTheory.Limits.kernel.ι (F.map f))] {Z : D} (h : F.obj (CategoryTheory.Abelian.coimage f) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Abelian.coimage.π (F.map f)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Abelian.PreservesCoimage.iso F f).inv h) = CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.Abelian.coimage.π f)) h
• CategoryTheory.Abelian.PreservesCoimage.factorThruCoimage_iso_inv_assoc 📋 Mathlib.CategoryTheory.Limits.Preserves.Shapes.AbelianImages
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasZeroMorphisms C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Limits.HasZeroMorphisms D] (F : CategoryTheory.Functor C D) [F.PreservesZeroMorphisms] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Limits.HasKernel f] [CategoryTheory.Limits.HasCokernel (CategoryTheory.Limits.kernel.ι f)] [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair f 0) F] [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair (CategoryTheory.Limits.kernel.ι f) 0) F] [CategoryTheory.Limits.HasKernel (F.map f)] [CategoryTheory.Limits.HasCokernel (CategoryTheory.Limits.kernel.ι (F.map f))] {Z : D} (h : F.obj Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Abelian.PreservesCoimage.iso F f).inv (CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.Abelian.factorThruCoimage f)) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Abelian.factorThruCoimage (F.map f)) h
• CategoryTheory.Abelian.PreservesCoimage.iso_hom_π_assoc 📋 Mathlib.CategoryTheory.Limits.Preserves.Shapes.AbelianImages
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasZeroMorphisms C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Limits.HasZeroMorphisms D] (F : CategoryTheory.Functor C D) [F.PreservesZeroMorphisms] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Limits.HasKernel f] [CategoryTheory.Limits.HasCokernel (CategoryTheory.Limits.kernel.ι f)] [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair f 0) F] [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair (CategoryTheory.Limits.kernel.ι f) 0) F] [CategoryTheory.Limits.HasKernel (F.map f)] [CategoryTheory.Limits.HasCokernel (CategoryTheory.Limits.kernel.ι (F.map f))] {Z : D} (h : CategoryTheory.Abelian.coimage (F.map f) ⟶ Z) : CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.Abelian.coimage.π f)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Abelian.PreservesCoimage.iso F f).hom h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Abelian.coimage.π (F.map f)) h
• CategoryTheory.Abelian.PreservesCoimageImageComparison.iso 📋 Mathlib.CategoryTheory.Limits.Preserves.Shapes.AbelianImages
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasZeroMorphisms C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Limits.HasZeroMorphisms D] (F : CategoryTheory.Functor C D) [F.PreservesZeroMorphisms] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Limits.HasKernel f] [CategoryTheory.Limits.HasCokernel f] [CategoryTheory.Limits.HasKernel (CategoryTheory.Limits.cokernel.π f)] [CategoryTheory.Limits.HasCokernel (CategoryTheory.Limits.kernel.ι f)] [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair f 0) F] [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f 0) F] [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair (CategoryTheory.Limits.cokernel.π f) 0) F] [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair (CategoryTheory.Limits.kernel.ι f) 0) F] [CategoryTheory.Limits.HasKernel (CategoryTheory.Limits.cokernel.π (F.map f))] [CategoryTheory.Limits.HasCokernel (CategoryTheory.Limits.kernel.ι (F.map f))] : CategoryTheory.Arrow.mk (F.map (CategoryTheory.Abelian.coimageImageComparison f)) ≅ CategoryTheory.Arrow.mk (CategoryTheory.Abelian.coimageImageComparison (F.map f))
• CategoryTheory.Abelian.PreservesCoimage.hom_coimageImageComparison 📋 Mathlib.CategoryTheory.Limits.Preserves.Shapes.AbelianImages
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasZeroMorphisms C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Limits.HasZeroMorphisms D] (F : CategoryTheory.Functor C D) [F.PreservesZeroMorphisms] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Limits.HasKernel f] [CategoryTheory.Limits.HasCokernel f] [CategoryTheory.Limits.HasKernel (CategoryTheory.Limits.cokernel.π f)] [CategoryTheory.Limits.HasCokernel (CategoryTheory.Limits.kernel.ι f)] [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair f 0) F] [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f 0) F] [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair (CategoryTheory.Limits.cokernel.π f) 0) F] [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair (CategoryTheory.Limits.kernel.ι f) 0) F] [CategoryTheory.Limits.HasKernel (CategoryTheory.Limits.cokernel.π (F.map f))] [CategoryTheory.Limits.HasCokernel (CategoryTheory.Limits.kernel.ι (F.map f))] : CategoryTheory.CategoryStruct.comp (CategoryTheory.Abelian.PreservesCoimage.iso F f).hom (CategoryTheory.Abelian.coimageImageComparison (F.map f)) = CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.Abelian.coimageImageComparison f)) (CategoryTheory.Abelian.PreservesImage.iso F f).hom
• CategoryTheory.Abelian.PreservesCoimageImageComparison.iso_hom_left 📋 Mathlib.CategoryTheory.Limits.Preserves.Shapes.AbelianImages
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasZeroMorphisms C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Limits.HasZeroMorphisms D] (F : CategoryTheory.Functor C D) [F.PreservesZeroMorphisms] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Limits.HasKernel f] [CategoryTheory.Limits.HasCokernel f] [CategoryTheory.Limits.HasKernel (CategoryTheory.Limits.cokernel.π f)] [CategoryTheory.Limits.HasCokernel (CategoryTheory.Limits.kernel.ι f)] [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair f 0) F] [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f 0) F] [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair (CategoryTheory.Limits.cokernel.π f) 0) F] [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair (CategoryTheory.Limits.kernel.ι f) 0) F] [CategoryTheory.Limits.HasKernel (CategoryTheory.Limits.cokernel.π (F.map f))] [CategoryTheory.Limits.HasCokernel (CategoryTheory.Limits.kernel.ι (F.map f))] : (CategoryTheory.Abelian.PreservesCoimageImageComparison.iso F f).hom.left = (CategoryTheory.Abelian.PreservesCoimage.iso F f).hom
• CategoryTheory.Abelian.PreservesCoimageImageComparison.iso_hom_right 📋 Mathlib.CategoryTheory.Limits.Preserves.Shapes.AbelianImages
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasZeroMorphisms C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Limits.HasZeroMorphisms D] (F : CategoryTheory.Functor C D) [F.PreservesZeroMorphisms] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Limits.HasKernel f] [CategoryTheory.Limits.HasCokernel f] [CategoryTheory.Limits.HasKernel (CategoryTheory.Limits.cokernel.π f)] [CategoryTheory.Limits.HasCokernel (CategoryTheory.Limits.kernel.ι f)] [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair f 0) F] [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f 0) F] [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair (CategoryTheory.Limits.cokernel.π f) 0) F] [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair (CategoryTheory.Limits.kernel.ι f) 0) F] [CategoryTheory.Limits.HasKernel (CategoryTheory.Limits.cokernel.π (F.map f))] [CategoryTheory.Limits.HasCokernel (CategoryTheory.Limits.kernel.ι (F.map f))] : (CategoryTheory.Abelian.PreservesCoimageImageComparison.iso F f).hom.right = (CategoryTheory.Abelian.PreservesImage.iso F f).hom
• CategoryTheory.Abelian.PreservesCoimageImageComparison.iso_inv_left 📋 Mathlib.CategoryTheory.Limits.Preserves.Shapes.AbelianImages
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasZeroMorphisms C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Limits.HasZeroMorphisms D] (F : CategoryTheory.Functor C D) [F.PreservesZeroMorphisms] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Limits.HasKernel f] [CategoryTheory.Limits.HasCokernel f] [CategoryTheory.Limits.HasKernel (CategoryTheory.Limits.cokernel.π f)] [CategoryTheory.Limits.HasCokernel (CategoryTheory.Limits.kernel.ι f)] [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair f 0) F] [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f 0) F] [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair (CategoryTheory.Limits.cokernel.π f) 0) F] [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair (CategoryTheory.Limits.kernel.ι f) 0) F] [CategoryTheory.Limits.HasKernel (CategoryTheory.Limits.cokernel.π (F.map f))] [CategoryTheory.Limits.HasCokernel (CategoryTheory.Limits.kernel.ι (F.map f))] : (CategoryTheory.Abelian.PreservesCoimageImageComparison.iso F f).inv.left = (CategoryTheory.Abelian.PreservesCoimage.iso F f).inv
• CategoryTheory.Abelian.PreservesCoimageImageComparison.iso_inv_right 📋 Mathlib.CategoryTheory.Limits.Preserves.Shapes.AbelianImages
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasZeroMorphisms C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Limits.HasZeroMorphisms D] (F : CategoryTheory.Functor C D) [F.PreservesZeroMorphisms] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Limits.HasKernel f] [CategoryTheory.Limits.HasCokernel f] [CategoryTheory.Limits.HasKernel (CategoryTheory.Limits.cokernel.π f)] [CategoryTheory.Limits.HasCokernel (CategoryTheory.Limits.kernel.ι f)] [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair f 0) F] [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f 0) F] [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair (CategoryTheory.Limits.cokernel.π f) 0) F] [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair (CategoryTheory.Limits.kernel.ι f) 0) F] [CategoryTheory.Limits.HasKernel (CategoryTheory.Limits.cokernel.π (F.map f))] [CategoryTheory.Limits.HasCokernel (CategoryTheory.Limits.kernel.ι (F.map f))] : (CategoryTheory.Abelian.PreservesCoimageImageComparison.iso F f).inv.right = (CategoryTheory.Abelian.PreservesImage.iso F f).inv
• FGModuleCat.instIsIsoCoimageImageComparison 📋 Mathlib.Algebra.Category.FGModuleCat.Abelian
  {k : Type u} [Ring k] [IsNoetherianRing k] {X Y : FGModuleCat k} (f : X ⟶ Y) : CategoryTheory.IsIso (CategoryTheory.Abelian.coimageImageComparison f)
• CategoryTheory.ShortComplex.LeftHomologyData.ofAbelian_H 📋 Mathlib.Algebra.Homology.ShortComplex.Abelian
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex C) : (CategoryTheory.ShortComplex.LeftHomologyData.ofAbelian S).H = CategoryTheory.Abelian.coimage (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.ι S.g) (CategoryTheory.Limits.cokernel.π S.f))
• CategoryTheory.ShortComplex.cokernelToAbelianCoimage 📋 Mathlib.Algebra.Homology.ShortComplex.Abelian
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex C) : CategoryTheory.Limits.cokernel S.f ⟶ CategoryTheory.Abelian.coimage S.g
• CategoryTheory.ShortComplex.instEpiCokernelToAbelianCoimage 📋 Mathlib.Algebra.Homology.ShortComplex.Abelian
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex C) : CategoryTheory.Epi S.cokernelToAbelianCoimage
• CategoryTheory.ShortComplex.cokernel_π_comp_cokernelToAbelianCoimage 📋 Mathlib.Algebra.Homology.ShortComplex.Abelian
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex C) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.cokernel.π S.f) S.cokernelToAbelianCoimage = CategoryTheory.Abelian.coimage.π S.g
• CategoryTheory.ShortComplex.cokernel_π_comp_cokernelToAbelianCoimage_assoc 📋 Mathlib.Algebra.Homology.ShortComplex.Abelian
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex C) {Z : C} (h : CategoryTheory.Abelian.coimage S.g ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.cokernel.π S.f) (CategoryTheory.CategoryStruct.comp S.cokernelToAbelianCoimage h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Abelian.coimage.π S.g) h
• CategoryTheory.ShortComplex.cokernelToAbelianCoimageIsCokernel 📋 Mathlib.Algebra.Homology.ShortComplex.Abelian
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex C) : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ S.cokernelToAbelianCoimage ⋯)
• CategoryTheory.ShortComplex.kernel_ι_comp_cokernel_π_comp_cokernelToAbelianCoimage 📋 Mathlib.Algebra.Homology.ShortComplex.Abelian
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex C) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.ι S.g) (CategoryTheory.Limits.cokernel.π S.f)) S.cokernelToAbelianCoimage = 0
• CategoryTheory.ShortComplex.exact_iff_exact_coimage_π 📋 Mathlib.CategoryTheory.Abelian.Exact
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex C) : S.Exact ↔ { X₁ := S.X₁, X₂ := S.X₂, X₃ := CategoryTheory.Abelian.coimage S.g, f := S.f, g := CategoryTheory.Abelian.coimage.π S.g, zero := ⋯ }.Exact
• CategoryTheory.ShortComplex.Exact.isColimitCoimage 📋 Mathlib.CategoryTheory.Abelian.Exact
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Abelian C] {S : CategoryTheory.ShortComplex C} (h : S.Exact) : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ (CategoryTheory.Abelian.coimage.π S.g) ⋯)
• CategoryTheory.Abelian.FunctorCategory.coimageObjIso 📋 Mathlib.CategoryTheory.Abelian.FunctorCategory
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type w} [CategoryTheory.Category.{z, w} D] [CategoryTheory.Abelian D] {F G : CategoryTheory.Functor C D} (α : F ⟶ G) (X : C) : (CategoryTheory.Abelian.coimage α).obj X ≅ CategoryTheory.Abelian.coimage (α.app X)
• CategoryTheory.Abelian.FunctorCategory.coimageObjIso_inv 📋 Mathlib.CategoryTheory.Abelian.FunctorCategory
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type w} [CategoryTheory.Category.{z, w} D] [CategoryTheory.Abelian D] {F G : CategoryTheory.Functor C D} (α : F ⟶ G) (X : C) : (CategoryTheory.Abelian.FunctorCategory.coimageObjIso α X).inv = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.cokernel.map (CategoryTheory.Limits.kernel.ι (α.app X)) ((CategoryTheory.Limits.kernel.ι α).app X) (CategoryTheory.Limits.PreservesKernel.iso ((CategoryTheory.evaluation C D).obj X) α).inv (CategoryTheory.CategoryStruct.id (F.obj X)) ⋯) (CategoryTheory.Limits.cokernelComparison (CategoryTheory.Limits.kernel.ι α) ((CategoryTheory.evaluation C D).obj X))
• CategoryTheory.Abelian.FunctorCategory.coimageObjIso_hom 📋 Mathlib.CategoryTheory.Abelian.FunctorCategory
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type w} [CategoryTheory.Category.{z, w} D] [CategoryTheory.Abelian D] {F G : CategoryTheory.Functor C D} (α : F ⟶ G) (X : C) : (CategoryTheory.Abelian.FunctorCategory.coimageObjIso α X).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.PreservesCokernel.iso ((CategoryTheory.evaluation C D).obj X) (CategoryTheory.Limits.kernel.ι α)).hom (CategoryTheory.Limits.cokernel.map ((CategoryTheory.Limits.kernel.ι α).app X) (CategoryTheory.Limits.kernel.ι (α.app X)) (CategoryTheory.Limits.kernelComparison α ((CategoryTheory.evaluation C D).obj X)) (CategoryTheory.CategoryStruct.id (F.obj X)) ⋯)
• CategoryTheory.Abelian.FunctorCategory.functor_category_isIso_coimageImageComparison 📋 Mathlib.CategoryTheory.Abelian.FunctorCategory
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type w} [CategoryTheory.Category.{z, w} D] [CategoryTheory.Abelian D] {F G : CategoryTheory.Functor C D} (α : F ⟶ G) : CategoryTheory.IsIso (CategoryTheory.Abelian.coimageImageComparison α)
• CategoryTheory.Abelian.FunctorCategory.coimageImageComparison_app 📋 Mathlib.CategoryTheory.Abelian.FunctorCategory
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type w} [CategoryTheory.Category.{z, w} D] [CategoryTheory.Abelian D] {F G : CategoryTheory.Functor C D} (α : F ⟶ G) (X : C) : CategoryTheory.Abelian.coimageImageComparison (α.app X) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Abelian.FunctorCategory.coimageObjIso α X).inv (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Abelian.coimageImageComparison α).app X) (CategoryTheory.Abelian.FunctorCategory.imageObjIso α X).hom)
• CategoryTheory.Abelian.FunctorCategory.coimageImageComparison_app' 📋 Mathlib.CategoryTheory.Abelian.FunctorCategory
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type w} [CategoryTheory.Category.{z, w} D] [CategoryTheory.Abelian D] {F G : CategoryTheory.Functor C D} (α : F ⟶ G) (X : C) : (CategoryTheory.Abelian.coimageImageComparison α).app X = CategoryTheory.CategoryStruct.comp (CategoryTheory.Abelian.FunctorCategory.coimageObjIso α X).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Abelian.coimageImageComparison (α.app X)) (CategoryTheory.Abelian.FunctorCategory.imageObjIso α X).inv)
• CategoryTheory.instIsIsoIndCoimageImageComparison 📋 Mathlib.CategoryTheory.Abelian.Indization
  {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.Abelian C] {X Y : CategoryTheory.Ind C} (f : X ⟶ Y) : CategoryTheory.IsIso (CategoryTheory.Abelian.coimageImageComparison 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