Loogle!

Result

Found 331 declarations mentioning CategoryTheory.Limits.IsZero. Of these, only the first 200 are shown.

• CategoryTheory.Limits.IsZero 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
  {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) : Prop
• CategoryTheory.Limits.IsZero.hasZeroObject 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} (hX : CategoryTheory.Limits.IsZero X) : CategoryTheory.Limits.HasZeroObject C
• CategoryTheory.Limits.IsZero.isInitial 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} (hX : CategoryTheory.Limits.IsZero X) : CategoryTheory.Limits.IsInitial X
• CategoryTheory.Limits.IsZero.isTerminal 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} (hX : CategoryTheory.Limits.IsZero X) : CategoryTheory.Limits.IsTerminal X
• CategoryTheory.Limits.HasZeroObject.mk 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
  {C : Type u} [CategoryTheory.Category.{v, u} C] (zero : ∃ X, CategoryTheory.Limits.IsZero X) : CategoryTheory.Limits.HasZeroObject C
• CategoryTheory.Limits.HasZeroObject.zero 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
  {C : Type u} {inst✝ : CategoryTheory.Category.{v, u} C} [self : CategoryTheory.Limits.HasZeroObject C] : ∃ X, CategoryTheory.Limits.IsZero X
• CategoryTheory.Limits.IsZero.retract 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} (Y : C) (h : CategoryTheory.Limits.IsZero X) : CategoryTheory.Retract X Y
• CategoryTheory.Limits.IsZero.op 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} (h : CategoryTheory.Limits.IsZero X) : CategoryTheory.Limits.IsZero (Opposite.op X)
• CategoryTheory.Limits.isZero_zero 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
  (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] : CategoryTheory.Limits.IsZero 0
• CategoryTheory.Limits.IsZero.from_ 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} (h : CategoryTheory.Limits.IsZero X) (Y : C) : Y ⟶ X
• CategoryTheory.Limits.IsZero.iso 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (hX : CategoryTheory.Limits.IsZero X) (hY : CategoryTheory.Limits.IsZero Y) : X ≅ Y
• CategoryTheory.Limits.IsZero.isoIsInitial 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (hX : CategoryTheory.Limits.IsZero X) (hY : CategoryTheory.Limits.IsInitial Y) : X ≅ Y
• CategoryTheory.Limits.IsZero.isoIsTerminal 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (hX : CategoryTheory.Limits.IsZero X) (hY : CategoryTheory.Limits.IsTerminal Y) : X ≅ Y
• CategoryTheory.Limits.IsZero.of_iso 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (hY : CategoryTheory.Limits.IsZero Y) (e : X ≅ Y) : CategoryTheory.Limits.IsZero X
• CategoryTheory.Limits.IsZero.to_ 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} (h : CategoryTheory.Limits.IsZero X) (Y : C) : X ⟶ Y
• CategoryTheory.Limits.IsZero.unop 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X : Cᵒᵖ} (h : CategoryTheory.Limits.IsZero X) : CategoryTheory.Limits.IsZero (Opposite.unop X)
• CategoryTheory.Iso.isZero_iff 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (e : X ≅ Y) : CategoryTheory.Limits.IsZero X ↔ CategoryTheory.Limits.IsZero Y
• CategoryTheory.Limits.IsZero.unique_from 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} (self : CategoryTheory.Limits.IsZero X) (Y : C) : Nonempty (Unique (Y ⟶ X))
• CategoryTheory.Limits.IsZero.unique_to 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} (self : CategoryTheory.Limits.IsZero X) (Y : C) : Nonempty (Unique (X ⟶ Y))
• CategoryTheory.Limits.IsZero.epi 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} (h : CategoryTheory.Limits.IsZero X) {Y : C} (f : Y ⟶ X) : CategoryTheory.Epi f
• CategoryTheory.Limits.IsZero.isoZero 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] {X : C} (hX : CategoryTheory.Limits.IsZero X) : X ≅ 0
• CategoryTheory.Limits.IsZero.mono 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} (h : CategoryTheory.Limits.IsZero X) {Y : C} (f : X ⟶ Y) : CategoryTheory.Mono f
• CategoryTheory.Limits.IsZero.isIso 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (hX : CategoryTheory.Limits.IsZero X) (hY : CategoryTheory.Limits.IsZero Y) (f : X ⟶ Y) : CategoryTheory.IsIso f
• CategoryTheory.Limits.IsZero.mk 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} (unique_to : ∀ (Y : C), Nonempty (Unique (X ⟶ Y))) (unique_from : ∀ (Y : C), Nonempty (Unique (Y ⟶ X))) : CategoryTheory.Limits.IsZero X
• CategoryTheory.Functor.isZero 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] (F : CategoryTheory.Functor C D) (hF : ∀ (X : C), CategoryTheory.Limits.IsZero (F.obj X)) : CategoryTheory.Limits.IsZero F
• CategoryTheory.Limits.IsZero.eq_from 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (h : CategoryTheory.Limits.IsZero X) (f : Y ⟶ X) : f = h.from_ Y
• CategoryTheory.Limits.IsZero.eq_to 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (h : CategoryTheory.Limits.IsZero X) (f : X ⟶ Y) : f = h.to_ Y
• CategoryTheory.Limits.IsZero.from_eq 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (h : CategoryTheory.Limits.IsZero X) (f : Y ⟶ X) : h.from_ Y = f
• CategoryTheory.Limits.IsZero.to_eq 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (h : CategoryTheory.Limits.IsZero X) (f : X ⟶ Y) : h.to_ Y = f
• CategoryTheory.Limits.IsZero.obj 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Limits.HasZeroObject D] {F : CategoryTheory.Functor C D} (hF : CategoryTheory.Limits.IsZero F) (X : C) : CategoryTheory.Limits.IsZero (F.obj X)
• CategoryTheory.Functor.isZero_iff 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Limits.HasZeroObject D] (F : CategoryTheory.Functor C D) : CategoryTheory.Limits.IsZero F ↔ ∀ (X : C), CategoryTheory.Limits.IsZero (F.obj X)
• CategoryTheory.Limits.IsZero.of_full_of_faithful_of_isZero 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] (F : CategoryTheory.Functor C D) [F.Full] [F.Faithful] (X : C) (hX : CategoryTheory.Limits.IsZero (F.obj X)) : CategoryTheory.Limits.IsZero X
• CategoryTheory.Limits.IsZero.eq_of_src 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (hX : CategoryTheory.Limits.IsZero X) (f g : X ⟶ Y) : f = g
• CategoryTheory.Limits.IsZero.eq_of_tgt 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (hX : CategoryTheory.Limits.IsZero X) (f g : Y ⟶ X) : f = g
• CategoryTheory.Limits.IsZero.hasZeroMorphisms 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
  {C : Type u} [CategoryTheory.Category.{v, u} C] {O : C} (hO : CategoryTheory.Limits.IsZero O) : CategoryTheory.Limits.HasZeroMorphisms C
• CategoryTheory.Limits.IsInitial.isZero 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {X : C} (hX : CategoryTheory.Limits.IsInitial X) : CategoryTheory.Limits.IsZero X
• CategoryTheory.Limits.IsTerminal.isZero 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {X : C} (hX : CategoryTheory.Limits.IsTerminal X) : CategoryTheory.Limits.IsZero X
• CategoryTheory.Limits.IsZero.of_epi 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Epi f] (i : CategoryTheory.Limits.IsZero X) : CategoryTheory.Limits.IsZero Y
• CategoryTheory.Limits.IsZero.of_mono 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Mono f] (i : CategoryTheory.Limits.IsZero Y) : CategoryTheory.Limits.IsZero X
• CategoryTheory.Limits.IsZero.of_epi_zero 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (X Y : C) [CategoryTheory.Epi 0] : CategoryTheory.Limits.IsZero Y
• CategoryTheory.Limits.IsZero.of_mono_zero 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (X Y : C) [CategoryTheory.Mono 0] : CategoryTheory.Limits.IsZero X
• CategoryTheory.Functor.zero_obj 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Limits.HasZeroObject D] (X : C) : CategoryTheory.Limits.IsZero (CategoryTheory.Functor.obj 0 X)
• CategoryTheory.Limits.IsColimit.isZero_pt 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] {F : CategoryTheory.Functor D C} {c : CategoryTheory.Limits.Cocone F} (hc : CategoryTheory.Limits.IsColimit c) (hF : CategoryTheory.Limits.IsZero F) : CategoryTheory.Limits.IsZero c.pt
• CategoryTheory.Limits.IsColimit.ofIsZero 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] {F : CategoryTheory.Functor D C} (c : CategoryTheory.Limits.Cocone F) (hF : CategoryTheory.Limits.IsZero F) (hc : CategoryTheory.Limits.IsZero c.pt) : CategoryTheory.Limits.IsColimit c
• CategoryTheory.Limits.IsLimit.isZero_pt 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] {F : CategoryTheory.Functor D C} {c : CategoryTheory.Limits.Cone F} (hc : CategoryTheory.Limits.IsLimit c) (hF : CategoryTheory.Limits.IsZero F) : CategoryTheory.Limits.IsZero c.pt
• CategoryTheory.Limits.IsLimit.ofIsZero 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] {F : CategoryTheory.Functor D C} (c : CategoryTheory.Limits.Cone F) (hF : CategoryTheory.Limits.IsZero F) (hc : CategoryTheory.Limits.IsZero c.pt) : CategoryTheory.Limits.IsLimit c
• CategoryTheory.Limits.isIsoZero_iff_source_target_isZero 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] (X Y : C) : CategoryTheory.IsIso 0 ↔ CategoryTheory.Limits.IsZero X ∧ CategoryTheory.Limits.IsZero Y
• CategoryTheory.Limits.IsZero.iff_id_eq_zero 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (X : C) : CategoryTheory.Limits.IsZero X ↔ CategoryTheory.CategoryStruct.id X = 0
• CategoryTheory.Limits.IsZero.eq_zero_of_src 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} (o : CategoryTheory.Limits.IsZero X) (f : X ⟶ Y) : f = 0
• CategoryTheory.Limits.IsZero.eq_zero_of_tgt 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} (o : CategoryTheory.Limits.IsZero Y) (f : X ⟶ Y) : f = 0
• CategoryTheory.Limits.IsZero.of_epi_eq_zero 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Epi f] (h : f = 0) : CategoryTheory.Limits.IsZero Y
• CategoryTheory.Limits.IsZero.of_mono_eq_zero 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Mono f] (h : f = 0) : CategoryTheory.Limits.IsZero X
• CategoryTheory.Limits.IsZero.iff_isSplitEpi_eq_zero 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.IsSplitEpi f] : CategoryTheory.Limits.IsZero Y ↔ f = 0
• CategoryTheory.Limits.IsZero.iff_isSplitMono_eq_zero 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.IsSplitMono f] : CategoryTheory.Limits.IsZero X ↔ f = 0
• CategoryTheory.Limits.IsZero.map 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasZeroMorphisms D] {F : CategoryTheory.Functor C D} (hF : CategoryTheory.Limits.IsZero F) {X Y : C} (f : X ⟶ Y) : F.map f = 0
• SemimoduleCat.isZero_of_subsingleton 📋 Mathlib.Algebra.Category.ModuleCat.Semi
  {R : Type u} [Semiring R] (M : SemimoduleCat R) [Subsingleton ↑M] : CategoryTheory.Limits.IsZero M
• SemimoduleCat.subsingleton_of_isZero 📋 Mathlib.Algebra.Category.ModuleCat.Semi
  {R : Type u} [Semiring R] {M : SemimoduleCat R} (h : CategoryTheory.Limits.IsZero M) : Subsingleton ↑M
• SemimoduleCat.isZero_iff_subsingleton 📋 Mathlib.Algebra.Category.ModuleCat.Semi
  {R : Type u} [Semiring R] {M : SemimoduleCat R} : CategoryTheory.Limits.IsZero M ↔ Subsingleton ↑M
• SemimoduleCat.isZero_of_iff_subsingleton 📋 Mathlib.Algebra.Category.ModuleCat.Semi
  {R : Type u} [Semiring R] {M : Type u_1} [AddCommMonoid M] [Module R M] : CategoryTheory.Limits.IsZero (SemimoduleCat.of R M) ↔ Subsingleton M
• CategoryTheory.Functor.preservesColimitsOfSize_of_isZero 📋 Mathlib.CategoryTheory.Limits.Preserves.Shapes.Zero
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasZeroMorphisms D] (G : CategoryTheory.Functor C D) (hG : CategoryTheory.Limits.IsZero G) : CategoryTheory.Limits.PreservesColimitsOfSize.{v, u, v₁, v₂, u₁, u₂} G
• CategoryTheory.Functor.preservesLimitsOfSize_of_isZero 📋 Mathlib.CategoryTheory.Limits.Preserves.Shapes.Zero
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasZeroMorphisms D] (G : CategoryTheory.Functor C D) (hG : CategoryTheory.Limits.IsZero G) : CategoryTheory.Limits.PreservesLimitsOfSize.{v, u, v₁, v₂, u₁, u₂} G
• CategoryTheory.Functor.map_isZero 📋 Mathlib.CategoryTheory.Limits.Preserves.Shapes.Zero
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroMorphisms D] (F : CategoryTheory.Functor C D) [F.PreservesZeroMorphisms] {X : C} (hX : CategoryTheory.Limits.IsZero X) : CategoryTheory.Limits.IsZero (F.obj X)
• CategoryTheory.Functor.preservesColimitsOfShape_of_isZero 📋 Mathlib.CategoryTheory.Limits.Preserves.Shapes.Zero
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasZeroMorphisms D] (G : CategoryTheory.Functor C D) (hG : CategoryTheory.Limits.IsZero G) (J : Type u_1) [CategoryTheory.Category.{v_1, u_1} J] : CategoryTheory.Limits.PreservesColimitsOfShape J G
• CategoryTheory.Functor.preservesLimitsOfShape_of_isZero 📋 Mathlib.CategoryTheory.Limits.Preserves.Shapes.Zero
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasZeroMorphisms D] (G : CategoryTheory.Functor C D) (hG : CategoryTheory.Limits.IsZero G) (J : Type u_1) [CategoryTheory.Category.{v_1, u_1} J] : CategoryTheory.Limits.PreservesLimitsOfShape J G
• CategoryTheory.Limits.isZero_cokernel_of_epi 📋 Mathlib.CategoryTheory.Limits.Shapes.Kernels
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Epi f] [CategoryTheory.Limits.HasCokernel f] : CategoryTheory.Limits.IsZero (CategoryTheory.Limits.cokernel f)
• CategoryTheory.Limits.isZero_kernel_of_mono 📋 Mathlib.CategoryTheory.Limits.Shapes.Kernels
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Mono f] [CategoryTheory.Limits.HasKernel f] : CategoryTheory.Limits.IsZero (CategoryTheory.Limits.kernel f)
• CategoryTheory.Limits.CokernelCofork.IsColimit.isZero_of_epi 📋 Mathlib.CategoryTheory.Limits.Shapes.Kernels
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} {f : X ⟶ Y} {c : CategoryTheory.Limits.CokernelCofork f} (hc : CategoryTheory.Limits.IsColimit c) [CategoryTheory.Epi f] : CategoryTheory.Limits.IsZero c.pt
• CategoryTheory.Limits.CokernelCofork.IsColimit.ofEpiOfIsZero 📋 Mathlib.CategoryTheory.Limits.Shapes.Kernels
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} {f : X ⟶ Y} (c : CategoryTheory.Limits.CokernelCofork f) (hf : CategoryTheory.Epi f) (h : CategoryTheory.Limits.IsZero c.pt) : CategoryTheory.Limits.IsColimit c
• CategoryTheory.Limits.KernelFork.IsLimit.isZero_of_mono 📋 Mathlib.CategoryTheory.Limits.Shapes.Kernels
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} {f : X ⟶ Y} {c : CategoryTheory.Limits.KernelFork f} (hc : CategoryTheory.Limits.IsLimit c) [CategoryTheory.Mono f] : CategoryTheory.Limits.IsZero c.pt
• CategoryTheory.Limits.KernelFork.IsLimit.ofMonoOfIsZero 📋 Mathlib.CategoryTheory.Limits.Shapes.Kernels
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} {f : X ⟶ Y} (c : CategoryTheory.Limits.KernelFork f) (hf : CategoryTheory.Mono f) (h : CategoryTheory.Limits.IsZero c.pt) : CategoryTheory.Limits.IsLimit c
• CategoryTheory.Preadditive.epi_of_isZero_cokernel 📋 Mathlib.CategoryTheory.Preadditive.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Limits.HasCokernel f] (h : CategoryTheory.Limits.IsZero (CategoryTheory.Limits.cokernel f)) : CategoryTheory.Epi f
• CategoryTheory.Preadditive.mono_of_isZero_kernel 📋 Mathlib.CategoryTheory.Preadditive.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Limits.HasKernel f] (h : CategoryTheory.Limits.IsZero (CategoryTheory.Limits.kernel f)) : CategoryTheory.Mono f
• CategoryTheory.Preadditive.epi_iff_isZero_cokernel 📋 Mathlib.CategoryTheory.Preadditive.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Limits.HasCokernel f] : CategoryTheory.Epi f ↔ CategoryTheory.Limits.IsZero (CategoryTheory.Limits.cokernel f)
• CategoryTheory.Preadditive.mono_iff_isZero_kernel 📋 Mathlib.CategoryTheory.Preadditive.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Limits.HasKernel f] : CategoryTheory.Mono f ↔ CategoryTheory.Limits.IsZero (CategoryTheory.Limits.kernel f)
• CategoryTheory.Preadditive.epi_of_isZero_cokernel' 📋 Mathlib.CategoryTheory.Preadditive.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {X Y : C} {f : X ⟶ Y} (c : CategoryTheory.Limits.CokernelCofork f) (hc : CategoryTheory.Limits.IsColimit c) (h : CategoryTheory.Limits.IsZero c.pt) : CategoryTheory.Epi f
• CategoryTheory.Preadditive.mono_of_isZero_kernel' 📋 Mathlib.CategoryTheory.Preadditive.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {X Y : C} {f : X ⟶ Y} (c : CategoryTheory.Limits.KernelFork f) (hc : CategoryTheory.Limits.IsLimit c) (h : CategoryTheory.Limits.IsZero c.pt) : CategoryTheory.Mono f
• CategoryTheory.Preadditive.epi_iff_isZero_cokernel' 📋 Mathlib.CategoryTheory.Preadditive.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {X Y : C} {f : X ⟶ Y} (c : CategoryTheory.Limits.CokernelCofork f) (hc : CategoryTheory.Limits.IsColimit c) : CategoryTheory.Epi f ↔ CategoryTheory.Limits.IsZero c.pt
• CategoryTheory.Preadditive.mono_iff_isZero_kernel' 📋 Mathlib.CategoryTheory.Preadditive.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {X Y : C} {f : X ⟶ Y} (c : CategoryTheory.Limits.KernelFork f) (hc : CategoryTheory.Limits.IsLimit c) : CategoryTheory.Mono f ↔ CategoryTheory.Limits.IsZero c.pt
• CategoryTheory.Limits.isoBiprodZero 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
  {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} [CategoryTheory.Limits.HasBinaryBiproduct X Y] (hY : CategoryTheory.Limits.IsZero Y) : X ≅ X ⊞ Y
• CategoryTheory.Limits.isoZeroBiprod 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
  {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} [CategoryTheory.Limits.HasBinaryBiproduct X Y] (hY : CategoryTheory.Limits.IsZero X) : Y ≅ X ⊞ Y
• CategoryTheory.Limits.biprod_isZero_iff 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
  {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] (A B : C) [CategoryTheory.Limits.HasBinaryBiproduct A B] : CategoryTheory.Limits.IsZero (A ⊞ B) ↔ CategoryTheory.Limits.IsZero A ∧ CategoryTheory.Limits.IsZero B
• CategoryTheory.Limits.isoBiprodZero_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
  {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} [CategoryTheory.Limits.HasBinaryBiproduct X Y] (hY : CategoryTheory.Limits.IsZero Y) : (CategoryTheory.Limits.isoBiprodZero hY).hom = CategoryTheory.Limits.biprod.inl
• CategoryTheory.Limits.isoBiprodZero_inv 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
  {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} [CategoryTheory.Limits.HasBinaryBiproduct X Y] (hY : CategoryTheory.Limits.IsZero Y) : (CategoryTheory.Limits.isoBiprodZero hY).inv = CategoryTheory.Limits.biprod.fst
• CategoryTheory.Limits.isoZeroBiprod_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
  {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} [CategoryTheory.Limits.HasBinaryBiproduct X Y] (hY : CategoryTheory.Limits.IsZero X) : (CategoryTheory.Limits.isoZeroBiprod hY).hom = CategoryTheory.Limits.biprod.inr
• CategoryTheory.Limits.isoZeroBiprod_inv 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
  {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} [CategoryTheory.Limits.HasBinaryBiproduct X Y] (hY : CategoryTheory.Limits.IsZero X) : (CategoryTheory.Limits.isoZeroBiprod hY).inv = CategoryTheory.Limits.biprod.snd
• CategoryTheory.Functor.Additive.of_isZero 📋 Mathlib.CategoryTheory.Preadditive.AdditiveFunctor
  {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] {F : CategoryTheory.Functor C D} (hF : CategoryTheory.Limits.IsZero F) : F.Additive
• ModuleCat.isZero_of_subsingleton 📋 Mathlib.Algebra.Category.ModuleCat.Basic
  {R : Type u} [Ring R] (M : ModuleCat R) [Subsingleton ↑M] : CategoryTheory.Limits.IsZero M
• ModuleCat.subsingleton_of_isZero 📋 Mathlib.Algebra.Category.ModuleCat.Basic
  {R : Type u} [Ring R] {M : ModuleCat R} (h : CategoryTheory.Limits.IsZero M) : Subsingleton ↑M
• ModuleCat.isZero_iff_subsingleton 📋 Mathlib.Algebra.Category.ModuleCat.Basic
  {R : Type u} [Ring R] {M : ModuleCat R} : CategoryTheory.Limits.IsZero M ↔ Subsingleton ↑M
• ModuleCat.isZero_of_iff_subsingleton 📋 Mathlib.Algebra.Category.ModuleCat.Basic
  {R : Type u} [Ring R] {M : Type u_1} [AddCommGroup M] [Module R M] : CategoryTheory.Limits.IsZero (ModuleCat.of R M) ↔ Subsingleton M
• CategoryTheory.ObjectProperty.instContainsZeroIsZeroOfHasZeroObject 📋 Mathlib.CategoryTheory.ObjectProperty.ContainsZero
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] : CategoryTheory.ObjectProperty.ContainsZero CategoryTheory.Limits.IsZero
• CategoryTheory.ObjectProperty.exists_prop_of_containsZero 📋 Mathlib.CategoryTheory.ObjectProperty.ContainsZero
  {C : Type u} [CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C) [P.ContainsZero] : ∃ Z, CategoryTheory.Limits.IsZero Z ∧ P Z
• CategoryTheory.ObjectProperty.ContainsZero.exists_zero 📋 Mathlib.CategoryTheory.ObjectProperty.ContainsZero
  {C : Type u} {inst✝ : CategoryTheory.Category.{v, u} C} {P : CategoryTheory.ObjectProperty C} [self : P.ContainsZero] : ∃ Z, CategoryTheory.Limits.IsZero Z ∧ P Z
• CategoryTheory.ObjectProperty.ContainsZero.mk 📋 Mathlib.CategoryTheory.ObjectProperty.ContainsZero
  {C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.ObjectProperty C} (exists_zero : ∃ Z, CategoryTheory.Limits.IsZero Z ∧ P Z) : P.ContainsZero
• CategoryTheory.ObjectProperty.prop_of_isZero 📋 Mathlib.CategoryTheory.ObjectProperty.ContainsZero
  {C : Type u} [CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C) [P.ContainsZero] [P.IsClosedUnderIsomorphisms] {Z : C} (hZ : CategoryTheory.Limits.IsZero Z) : P Z
• CategoryTheory.AddMon.isZero_trivial 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
  (D : Type u_1) [CategoryTheory.Category.{v_1, u_1} D] [CategoryTheory.SemiCartesianMonoidalCategory D] : CategoryTheory.Limits.IsZero (CategoryTheory.AddMon.trivial D)
• CategoryTheory.Mon.isZero_trivial 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
  (D : Type u_1) [CategoryTheory.Category.{v_1, u_1} D] [CategoryTheory.SemiCartesianMonoidalCategory D] : CategoryTheory.Limits.IsZero (CategoryTheory.Mon.trivial D)
• CategoryTheory.AddGrp.isZero_trivial 📋 Mathlib.CategoryTheory.Monoidal.Grp
  (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] : CategoryTheory.Limits.IsZero (CategoryTheory.AddGrp.trivial C)
• CategoryTheory.Grp.isZero_trivial 📋 Mathlib.CategoryTheory.Monoidal.Grp
  (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] : CategoryTheory.Limits.IsZero (CategoryTheory.Grp.trivial C)
• CategoryTheory.ShortComplex.isZero_homology_of_isZero_X₂ 📋 Mathlib.Algebra.Homology.ShortComplex.Homology
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) (hS : CategoryTheory.Limits.IsZero S.X₂) [S.HasHomology] : CategoryTheory.Limits.IsZero S.homology
• CategoryTheory.Limits.IsZero.projective 📋 Mathlib.CategoryTheory.Preadditive.Projective.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} (h : CategoryTheory.Limits.IsZero X) : CategoryTheory.Projective X
• CategoryTheory.Limits.IsZero.injective 📋 Mathlib.CategoryTheory.Preadditive.Injective.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} (h : CategoryTheory.Limits.IsZero X) : CategoryTheory.Injective X
• CategoryTheory.Injective.isZero_under 📋 Mathlib.CategoryTheory.Preadditive.Injective.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.EnoughInjectives C] (X : C) (hX : CategoryTheory.Limits.IsZero X) : CategoryTheory.Limits.IsZero (CategoryTheory.Injective.under X)
• CategoryTheory.Injective.exists_presentation 📋 Mathlib.CategoryTheory.Preadditive.Injective.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.EnoughInjectives C] (X : C) : ∃ p, CategoryTheory.Limits.IsZero X → CategoryTheory.Limits.IsZero p.J
• CategoryTheory.ShortComplex.exact_of_isZero_X₂ 📋 Mathlib.Algebra.Homology.ShortComplex.Exact
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) (h : CategoryTheory.Limits.IsZero S.X₂) : S.Exact
• CategoryTheory.ShortComplex.exact_iff_isZero_homology 📋 Mathlib.Algebra.Homology.ShortComplex.Exact
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) [S.HasHomology] : S.Exact ↔ CategoryTheory.Limits.IsZero S.homology
• CategoryTheory.ShortComplex.exact_iff_isZero_leftHomology 📋 Mathlib.Algebra.Homology.ShortComplex.Exact
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) [S.HasHomology] : S.Exact ↔ CategoryTheory.Limits.IsZero S.leftHomology
• CategoryTheory.ShortComplex.exact_iff_isZero_rightHomology 📋 Mathlib.Algebra.Homology.ShortComplex.Exact
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) [S.HasHomology] : S.Exact ↔ CategoryTheory.Limits.IsZero S.rightHomology
• CategoryTheory.ShortComplex.HomologyData.exact_iff 📋 Mathlib.Algebra.Homology.ShortComplex.Exact
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S : CategoryTheory.ShortComplex C} (h : S.HomologyData) : S.Exact ↔ CategoryTheory.Limits.IsZero h.left.H
• CategoryTheory.ShortComplex.HomologyData.exact_iff' 📋 Mathlib.Algebra.Homology.ShortComplex.Exact
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S : CategoryTheory.ShortComplex C} (h : S.HomologyData) : S.Exact ↔ CategoryTheory.Limits.IsZero h.right.H
• CategoryTheory.ShortComplex.LeftHomologyData.exact_iff 📋 Mathlib.Algebra.Homology.ShortComplex.Exact
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S : CategoryTheory.ShortComplex C} [S.HasHomology] (h : S.LeftHomologyData) : S.Exact ↔ CategoryTheory.Limits.IsZero h.H
• CategoryTheory.ShortComplex.RightHomologyData.exact_iff 📋 Mathlib.Algebra.Homology.ShortComplex.Exact
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S : CategoryTheory.ShortComplex C} [S.HasHomology] (h : S.RightHomologyData) : S.Exact ↔ CategoryTheory.Limits.IsZero h.H
• CategoryTheory.ShortComplex.Exact.isZero_of_both_isZero 📋 Mathlib.Algebra.Homology.ShortComplex.Exact
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S : CategoryTheory.ShortComplex C} (ex : S.Exact) (hX₁ : CategoryTheory.Limits.IsZero S.X₁) (hX₃ : CategoryTheory.Limits.IsZero S.X₃) : CategoryTheory.Limits.IsZero S.X₂
• CategoryTheory.ShortComplex.Exact.condition 📋 Mathlib.Algebra.Homology.ShortComplex.Exact
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S : CategoryTheory.ShortComplex C} (self : S.Exact) : ∃ h, CategoryTheory.Limits.IsZero h.left.H
• CategoryTheory.ShortComplex.Exact.mk 📋 Mathlib.Algebra.Homology.ShortComplex.Exact
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S : CategoryTheory.ShortComplex C} (condition : ∃ h, CategoryTheory.Limits.IsZero h.left.H) : S.Exact
• CategoryTheory.ShortComplex.Splitting.ofIsZero 📋 Mathlib.Algebra.Homology.ShortComplex.Exact
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] (S : CategoryTheory.ShortComplex C) (h₁ : CategoryTheory.Limits.IsZero S.X₁) (h₂ : CategoryTheory.Limits.IsZero S.X₂) (h₃ : CategoryTheory.Limits.IsZero S.X₃) : S.Splitting
• CategoryTheory.ShortComplex.Splitting.ofIsIsoOfIsZero 📋 Mathlib.Algebra.Homology.ShortComplex.Exact
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] (S : CategoryTheory.ShortComplex C) (hf : CategoryTheory.IsIso S.f) (hg : CategoryTheory.Limits.IsZero S.X₃) : S.Splitting
• CategoryTheory.ShortComplex.Splitting.ofIsZeroOfIsIso 📋 Mathlib.Algebra.Homology.ShortComplex.Exact
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] (S : CategoryTheory.ShortComplex C) (hf : CategoryTheory.Limits.IsZero S.X₁) (hg : CategoryTheory.IsIso S.g) : S.Splitting
• CategoryTheory.ShortComplex.LeftHomologyData.exact_map_iff 📋 Mathlib.Algebra.Homology.ShortComplex.Exact
  {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroMorphisms D] {S : CategoryTheory.ShortComplex C} (h : S.LeftHomologyData) (F : CategoryTheory.Functor C D) [F.PreservesZeroMorphisms] [h.IsPreservedBy F] [(S.map F).HasHomology] : (S.map F).Exact ↔ CategoryTheory.Limits.IsZero (F.obj h.H)
• CategoryTheory.ShortComplex.RightHomologyData.exact_map_iff 📋 Mathlib.Algebra.Homology.ShortComplex.Exact
  {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroMorphisms D] {S : CategoryTheory.ShortComplex C} (h : S.RightHomologyData) (F : CategoryTheory.Functor C D) [F.PreservesZeroMorphisms] [h.IsPreservedBy F] [(S.map F).HasHomology] : (S.map F).Exact ↔ CategoryTheory.Limits.IsZero (F.obj h.H)
• CategoryTheory.ShortComplex.Exact.isZero_of_both_zeros 📋 Mathlib.Algebra.Homology.ShortComplex.Exact
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S : CategoryTheory.ShortComplex C} (ex : S.Exact) (hf : S.f = 0) (hg : S.g = 0) : CategoryTheory.Limits.IsZero S.X₂
• CategoryTheory.ShortComplex.Exact.isZero_X₂ 📋 Mathlib.Algebra.Homology.ShortComplex.Exact
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {S : CategoryTheory.ShortComplex C} (hS : S.Exact) (hf : S.f = 0) (hg : S.g = 0) : CategoryTheory.Limits.IsZero S.X₂
• CategoryTheory.ShortComplex.Exact.isZero_X₂_iff 📋 Mathlib.Algebra.Homology.ShortComplex.Exact
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {S : CategoryTheory.ShortComplex C} (hS : S.Exact) : CategoryTheory.Limits.IsZero S.X₂ ↔ S.f = 0 ∧ S.g = 0
• CategoryTheory.ShortComplex.ShortExact.isIso_f_iff 📋 Mathlib.Algebra.Homology.ShortComplex.ShortExact
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {S : CategoryTheory.ShortComplex C} (hS : S.ShortExact) [CategoryTheory.Balanced C] : CategoryTheory.IsIso S.f ↔ CategoryTheory.Limits.IsZero S.X₃
• CategoryTheory.ShortComplex.ShortExact.isIso_g_iff 📋 Mathlib.Algebra.Homology.ShortComplex.ShortExact
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {S : CategoryTheory.ShortComplex C} (hS : S.ShortExact) [CategoryTheory.Balanced C] : CategoryTheory.IsIso S.g ↔ CategoryTheory.Limits.IsZero S.X₁
• CategoryTheory.Subobject.subsingleton_of_isZero 📋 Mathlib.CategoryTheory.Subobject.Lattice
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} (hX : CategoryTheory.Limits.IsZero X) : Subsingleton (CategoryTheory.Subobject X)
• CategoryTheory.Subobject.nontrivial_of_not_isZero 📋 Mathlib.CategoryTheory.Subobject.Lattice
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] {X : C} (h : ¬CategoryTheory.Limits.IsZero X) : Nontrivial (CategoryTheory.Subobject X)
• AddCommGrpCat.isZero_of_subsingleton 📋 Mathlib.Algebra.Category.Grp.Zero
  (G : AddCommGrpCat) [Subsingleton ↑G] : CategoryTheory.Limits.IsZero G
• AddCommGrpCat.subsingleton_of_isZero 📋 Mathlib.Algebra.Category.Grp.Zero
  {G : AddCommGrpCat} (h : CategoryTheory.Limits.IsZero G) : Subsingleton ↑G
• AddGrpCat.isZero_of_subsingleton 📋 Mathlib.Algebra.Category.Grp.Zero
  (G : AddGrpCat) [Subsingleton ↑G] : CategoryTheory.Limits.IsZero G
• AddGrpCat.subsingleton_of_isZero 📋 Mathlib.Algebra.Category.Grp.Zero
  {G : AddGrpCat} (h : CategoryTheory.Limits.IsZero G) : Subsingleton ↑G
• CommGrpCat.isZero_of_subsingleton 📋 Mathlib.Algebra.Category.Grp.Zero
  (G : CommGrpCat) [Subsingleton ↑G] : CategoryTheory.Limits.IsZero G
• CommGrpCat.subsingleton_of_isZero 📋 Mathlib.Algebra.Category.Grp.Zero
  {G : CommGrpCat} (h : CategoryTheory.Limits.IsZero G) : Subsingleton ↑G
• GrpCat.isZero_of_subsingleton 📋 Mathlib.Algebra.Category.Grp.Zero
  (G : GrpCat) [Subsingleton ↑G] : CategoryTheory.Limits.IsZero G
• GrpCat.subsingleton_of_isZero 📋 Mathlib.Algebra.Category.Grp.Zero
  {G : GrpCat} (h : CategoryTheory.Limits.IsZero G) : Subsingleton ↑G
• AddCommGrpCat.isZero_iff_subsingleton 📋 Mathlib.Algebra.Category.Grp.Zero
  {G : AddCommGrpCat} : CategoryTheory.Limits.IsZero G ↔ Subsingleton ↑G
• AddGrpCat.isZero_iff_subsingleton 📋 Mathlib.Algebra.Category.Grp.Zero
  {G : AddGrpCat} : CategoryTheory.Limits.IsZero G ↔ Subsingleton ↑G
• CommGrpCat.isZero_iff_subsingleton 📋 Mathlib.Algebra.Category.Grp.Zero
  {G : CommGrpCat} : CategoryTheory.Limits.IsZero G ↔ Subsingleton ↑G
• GrpCat.isZero_iff_subsingleton 📋 Mathlib.Algebra.Category.Grp.Zero
  {G : GrpCat} : CategoryTheory.Limits.IsZero G ↔ Subsingleton ↑G
• AddCommGrpCat.isZero_of_iff_subsingleton 📋 Mathlib.Algebra.Category.Grp.Zero
  {G : Type u_1} [AddCommGroup G] : CategoryTheory.Limits.IsZero (AddCommGrpCat.of G) ↔ Subsingleton G
• AddGrpCat.isZero_of_iff_subsingleton 📋 Mathlib.Algebra.Category.Grp.Zero
  {G : Type u_1} [AddGroup G] : CategoryTheory.Limits.IsZero (AddGrpCat.of G) ↔ Subsingleton G
• CommGrpCat.isZero_of_iff_subsingleton 📋 Mathlib.Algebra.Category.Grp.Zero
  {G : Type u_1} [CommGroup G] : CategoryTheory.Limits.IsZero (CommGrpCat.of G) ↔ Subsingleton G
• GrpCat.isZero_of_iff_subsingleton 📋 Mathlib.Algebra.Category.Grp.Zero
  {G : Type u_1} [Group G] : CategoryTheory.Limits.IsZero (GrpCat.of G) ↔ Subsingleton G
• CategoryTheory.ObjectProperty.instIsClosedUnderQuotientsIsZeroOfHasZeroMorphisms 📋 Mathlib.CategoryTheory.ObjectProperty.EpiMono
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] : CategoryTheory.ObjectProperty.IsClosedUnderQuotients CategoryTheory.Limits.IsZero
• CategoryTheory.ObjectProperty.instIsClosedUnderSubobjectsIsZeroOfHasZeroMorphisms 📋 Mathlib.CategoryTheory.ObjectProperty.EpiMono
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] : CategoryTheory.ObjectProperty.IsClosedUnderSubobjects CategoryTheory.Limits.IsZero
• CategoryTheory.ObjectProperty.instIsClosedUnderExtensionsIsZero 📋 Mathlib.CategoryTheory.ObjectProperty.Extensions
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] : CategoryTheory.ObjectProperty.IsClosedUnderExtensions CategoryTheory.Limits.IsZero
• CategoryTheory.ObjectProperty.instIsSerreClassIsZero 📋 Mathlib.CategoryTheory.Abelian.SerreClass.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] : CategoryTheory.ObjectProperty.IsSerreClass CategoryTheory.Limits.IsZero
• CategoryTheory.ShortComplex.SnakeInput.epi_δ 📋 Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex.SnakeInput C) (h₃ : CategoryTheory.Limits.IsZero S.L₃.X₂) : CategoryTheory.Epi S.δ
• CategoryTheory.ShortComplex.SnakeInput.mono_δ 📋 Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex.SnakeInput C) (h₀ : CategoryTheory.Limits.IsZero S.L₀.X₂) : CategoryTheory.Mono S.δ
• CategoryTheory.ShortComplex.SnakeInput.δIso 📋 Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex.SnakeInput C) (h₀ : CategoryTheory.Limits.IsZero S.L₀.X₂) (h₃ : CategoryTheory.Limits.IsZero S.L₃.X₂) : S.L₀.X₃ ≅ S.L₃.X₁
• CategoryTheory.ShortComplex.SnakeInput.isIso_δ 📋 Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex.SnakeInput C) (h₀ : CategoryTheory.Limits.IsZero S.L₀.X₂) (h₃ : CategoryTheory.Limits.IsZero S.L₃.X₂) : CategoryTheory.IsIso S.δ
• HomologicalComplex.isZero_zero 📋 Mathlib.Algebra.Homology.HomologicalComplex
  {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} [CategoryTheory.Limits.HasZeroObject V] : CategoryTheory.Limits.IsZero HomologicalComplex.zero
• HomologicalComplex.isZero_single_obj_X 📋 Mathlib.Algebra.Homology.Single
  {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] [CategoryTheory.Limits.HasZeroObject V] {ι : Type u_1} [DecidableEq ι] (c : ComplexShape ι) (j : ι) (A : V) (i : ι) (hi : i ≠ j) : CategoryTheory.Limits.IsZero (((HomologicalComplex.single V c j).obj A).X i)
• HomologicalComplex.isZero_single_comp_eval 📋 Mathlib.Algebra.Homology.Single
  (V : Type u) [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] [CategoryTheory.Limits.HasZeroObject V] {ι : Type u_1} [DecidableEq ι] (c : ComplexShape ι) (j i : ι) (hi : i ≠ j) : CategoryTheory.Limits.IsZero ((HomologicalComplex.single V c j).comp (HomologicalComplex.eval V c i))
• HomologicalComplex.ExactAt.of_isZero 📋 Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} {K : HomologicalComplex C c} {i : ι} (h : CategoryTheory.Limits.IsZero (K.X i)) : K.ExactAt i
• HomologicalComplex.acyclic_of_isZero 📋 Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (hK : CategoryTheory.Limits.IsZero K) : K.Acyclic
• HomologicalComplex.ExactAt.isZero_homology 📋 Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} {K : HomologicalComplex C c} {i : ι} [K.HasHomology i] (h : K.ExactAt i) : CategoryTheory.Limits.IsZero (K.homology i)
• HomologicalComplex.exactAt_iff_isZero_homology 📋 Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) [K.HasHomology i] : K.ExactAt i ↔ CategoryTheory.Limits.IsZero (K.homology i)
• HomologicalComplex.homotopyCofiber.isZero_X 📋 Mathlib.Algebra.Homology.HomotopyCofiber
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {ι : Type u_2} {c : ComplexShape ι} {F G : HomologicalComplex C c} (φ : F ⟶ G) [HomologicalComplex.HasHomotopyCofiber φ] [DecidableRel c.Rel] (i : ι) (hG : CategoryTheory.Limits.IsZero (G.X i)) (hF : ∀ (j : ι), c.Rel i j → CategoryTheory.Limits.IsZero (F.X j)) : CategoryTheory.Limits.IsZero (HomologicalComplex.homotopyCofiber.X φ i)
• CochainComplex.mappingCone.isZero_X_iff 📋 Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
  {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.Preadditive C] {F G : CochainComplex C ℤ} (φ : F ⟶ G) [HomologicalComplex.HasHomotopyCofiber φ] (i : ℤ) : CategoryTheory.Limits.IsZero ((CochainComplex.mappingCone φ).X i) ↔ CategoryTheory.Limits.IsZero (F.X (i + 1)) ∧ CategoryTheory.Limits.IsZero (G.X i)
• HomotopyCategory.isZero_quotient_obj_iff 📋 Mathlib.Algebra.Homology.HomotopyCategory
  {ι : Type u_2} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} (C : HomologicalComplex V c) : CategoryTheory.Limits.IsZero ((HomotopyCategory.quotient V c).obj C) ↔ Nonempty (Homotopy (CategoryTheory.CategoryStruct.id C) 0)
• CategoryTheory.Pretriangulated.Triangle.isZero₁_of_isZero₂₃ 📋 Mathlib.CategoryTheory.Triangulated.Pretriangulated
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [hC : CategoryTheory.Pretriangulated C] (T : CategoryTheory.Pretriangulated.Triangle C) (hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles) (h₂ : CategoryTheory.Limits.IsZero T.obj₂) (h₃ : CategoryTheory.Limits.IsZero T.obj₃) : CategoryTheory.Limits.IsZero T.obj₁
• CategoryTheory.Pretriangulated.Triangle.isZero₂_of_isZero₁₃ 📋 Mathlib.CategoryTheory.Triangulated.Pretriangulated
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [hC : CategoryTheory.Pretriangulated C] (T : CategoryTheory.Pretriangulated.Triangle C) (hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles) (h₁ : CategoryTheory.Limits.IsZero T.obj₁) (h₃ : CategoryTheory.Limits.IsZero T.obj₃) : CategoryTheory.Limits.IsZero T.obj₂
• CategoryTheory.Pretriangulated.Triangle.isZero₃_of_isZero₁₂ 📋 Mathlib.CategoryTheory.Triangulated.Pretriangulated
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [hC : CategoryTheory.Pretriangulated C] (T : CategoryTheory.Pretriangulated.Triangle C) (hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles) (h₁ : CategoryTheory.Limits.IsZero T.obj₁) (h₂ : CategoryTheory.Limits.IsZero T.obj₂) : CategoryTheory.Limits.IsZero T.obj₃
• CategoryTheory.Pretriangulated.Triangle.isZero₁_of_isIso₂ 📋 Mathlib.CategoryTheory.Triangulated.Pretriangulated
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [hC : CategoryTheory.Pretriangulated C] (T : CategoryTheory.Pretriangulated.Triangle C) (hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles) (h : CategoryTheory.IsIso T.mor₂) : CategoryTheory.Limits.IsZero T.obj₁
• CategoryTheory.Pretriangulated.Triangle.isZero₃_of_isIso₁ 📋 Mathlib.CategoryTheory.Triangulated.Pretriangulated
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [hC : CategoryTheory.Pretriangulated C] (T : CategoryTheory.Pretriangulated.Triangle C) (hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles) (h : CategoryTheory.IsIso T.mor₁) : CategoryTheory.Limits.IsZero T.obj₃
• CategoryTheory.Pretriangulated.Triangle.distinguished_iff_of_isZero₁ 📋 Mathlib.CategoryTheory.Triangulated.Pretriangulated
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [hC : CategoryTheory.Pretriangulated C] (T : CategoryTheory.Pretriangulated.Triangle C) (h : CategoryTheory.Limits.IsZero T.obj₁) : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles ↔ CategoryTheory.IsIso T.mor₂
• CategoryTheory.Pretriangulated.Triangle.distinguished_iff_of_isZero₃ 📋 Mathlib.CategoryTheory.Triangulated.Pretriangulated
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [hC : CategoryTheory.Pretriangulated C] (T : CategoryTheory.Pretriangulated.Triangle C) (h : CategoryTheory.Limits.IsZero T.obj₃) : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles ↔ CategoryTheory.IsIso T.mor₁
• CategoryTheory.Pretriangulated.Triangle.isZero₁_iff_isIso₂ 📋 Mathlib.CategoryTheory.Triangulated.Pretriangulated
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [hC : CategoryTheory.Pretriangulated C] (T : CategoryTheory.Pretriangulated.Triangle C) (hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles) : CategoryTheory.Limits.IsZero T.obj₁ ↔ CategoryTheory.IsIso T.mor₂
• CategoryTheory.Pretriangulated.Triangle.isZero₃_iff_isIso₁ 📋 Mathlib.CategoryTheory.Triangulated.Pretriangulated
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [hC : CategoryTheory.Pretriangulated C] (T : CategoryTheory.Pretriangulated.Triangle C) (hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles) : CategoryTheory.Limits.IsZero T.obj₃ ↔ CategoryTheory.IsIso T.mor₁
• CategoryTheory.Pretriangulated.Triangle.isZero₂_of_isIso₃ 📋 Mathlib.CategoryTheory.Triangulated.Pretriangulated
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [hC : CategoryTheory.Pretriangulated C] (T : CategoryTheory.Pretriangulated.Triangle C) (hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles) (h : CategoryTheory.IsIso T.mor₃) : CategoryTheory.Limits.IsZero T.obj₂
• CategoryTheory.Pretriangulated.Triangle.distinguished_iff_of_isZero₂ 📋 Mathlib.CategoryTheory.Triangulated.Pretriangulated
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [hC : CategoryTheory.Pretriangulated C] (T : CategoryTheory.Pretriangulated.Triangle C) (h : CategoryTheory.Limits.IsZero T.obj₂) : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles ↔ CategoryTheory.IsIso T.mor₃
• CategoryTheory.Pretriangulated.Triangle.isZero₂_iff_isIso₃ 📋 Mathlib.CategoryTheory.Triangulated.Pretriangulated
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [hC : CategoryTheory.Pretriangulated C] (T : CategoryTheory.Pretriangulated.Triangle C) (hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles) : CategoryTheory.Limits.IsZero T.obj₂ ↔ CategoryTheory.IsIso T.mor₃
• CategoryTheory.Pretriangulated.Triangle.isZero₂_iff 📋 Mathlib.CategoryTheory.Triangulated.Pretriangulated
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [hC : CategoryTheory.Pretriangulated C] (T : CategoryTheory.Pretriangulated.Triangle C) (hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles) : CategoryTheory.Limits.IsZero T.obj₂ ↔ T.mor₁ = 0 ∧ T.mor₂ = 0
• CategoryTheory.Pretriangulated.Triangle.isZero₁_iff 📋 Mathlib.CategoryTheory.Triangulated.Pretriangulated
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [hC : CategoryTheory.Pretriangulated C] (T : CategoryTheory.Pretriangulated.Triangle C) (hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles) : CategoryTheory.Limits.IsZero T.obj₁ ↔ T.mor₁ = 0 ∧ T.mor₃ = 0
• CategoryTheory.Pretriangulated.Triangle.isZero₃_iff 📋 Mathlib.CategoryTheory.Triangulated.Pretriangulated
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [hC : CategoryTheory.Pretriangulated C] (T : CategoryTheory.Pretriangulated.Triangle C) (hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles) : CategoryTheory.Limits.IsZero T.obj₃ ↔ T.mor₂ = 0 ∧ T.mor₃ = 0
• CategoryTheory.ShortComplex.ShortExact.epi_δ 📋 Mathlib.Algebra.Homology.HomologySequence
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {c : ComplexShape ι} {S : CategoryTheory.ShortComplex (HomologicalComplex C c)} (hS : S.ShortExact) (i j : ι) (hij : c.Rel i j) (hj : CategoryTheory.Limits.IsZero (S.X₂.homology j)) : CategoryTheory.Epi (hS.δ i j hij)
• CategoryTheory.ShortComplex.ShortExact.mono_δ 📋 Mathlib.Algebra.Homology.HomologySequence
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {c : ComplexShape ι} {S : CategoryTheory.ShortComplex (HomologicalComplex C c)} (hS : S.ShortExact) (i j : ι) (hij : c.Rel i j) (hi : CategoryTheory.Limits.IsZero (S.X₂.homology i)) : CategoryTheory.Mono (hS.δ i j hij)
• CategoryTheory.ShortComplex.ShortExact.δIso 📋 Mathlib.Algebra.Homology.HomologySequence
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {c : ComplexShape ι} {S : CategoryTheory.ShortComplex (HomologicalComplex C c)} (hS : S.ShortExact) (i j : ι) (hij : c.Rel i j) (hi : CategoryTheory.Limits.IsZero (S.X₂.homology i)) (hj : CategoryTheory.Limits.IsZero (S.X₂.homology j)) : S.X₃.homology i ≅ S.X₁.homology j
• CategoryTheory.ShortComplex.ShortExact.isIso_δ 📋 Mathlib.Algebra.Homology.HomologySequence
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {c : ComplexShape ι} {S : CategoryTheory.ShortComplex (HomologicalComplex C c)} (hS : S.ShortExact) (i j : ι) (hij : c.Rel i j) (hi : CategoryTheory.Limits.IsZero (S.X₂.homology i)) (hj : CategoryTheory.Limits.IsZero (S.X₂.homology j)) : CategoryTheory.IsIso (hS.δ i j hij)
• CategoryTheory.Functor.mem_homologicalKernel_iff 📋 Mathlib.CategoryTheory.Triangulated.HomologicalFunctor
  {C : Type u_1} {A : Type u_3} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Category.{v_3, u_3} A] (F : CategoryTheory.Functor C A) [F.ShiftSequence ℤ] (X : C) : F.homologicalKernel X ↔ ∀ (n : ℤ), CategoryTheory.Limits.IsZero ((F.shift n).obj X)
• HomotopyCategory.mem_subcategoryAcyclic_iff 📋 Mathlib.Algebra.Homology.HomotopyCategory.Acyclic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (X : HomotopyCategory C (ComplexShape.up ℤ)) : HomotopyCategory.subcategoryAcyclic C X ↔ ∀ (n : ℤ), CategoryTheory.Limits.IsZero ((HomotopyCategory.homologyFunctor C (ComplexShape.up ℤ) n).obj X)
• HomologicalComplex.IsStrictlySupportedOutside.isZero 📋 Mathlib.Algebra.Homology.Embedding.IsSupported
  {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3} [CategoryTheory.Category.{v_1, u_3} C] [CategoryTheory.Limits.HasZeroMorphisms C] {K : HomologicalComplex C c'} {e : c.Embedding c'} (self : K.IsStrictlySupportedOutside e) (i : ι) : CategoryTheory.Limits.IsZero (K.X (e.f i))
• HomologicalComplex.IsStrictlySupportedOutside.mk 📋 Mathlib.Algebra.Homology.Embedding.IsSupported
  {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3} [CategoryTheory.Category.{v_1, u_3} C] [CategoryTheory.Limits.HasZeroMorphisms C] {K : HomologicalComplex C c'} {e : c.Embedding c'} (isZero : ∀ (i : ι), CategoryTheory.Limits.IsZero (K.X (e.f i))) : K.IsStrictlySupportedOutside e
• HomologicalComplex.isZero_X_of_isStrictlySupported 📋 Mathlib.Algebra.Homology.Embedding.IsSupported
  {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3} [CategoryTheory.Category.{v_1, u_3} C] [CategoryTheory.Limits.HasZeroMorphisms C] (K : HomologicalComplex C c') (e : c.Embedding c') [K.IsStrictlySupported e] (i' : ι') (hi' : ∀ (i : ι), e.f i ≠ i') : CategoryTheory.Limits.IsZero (K.X i')
• HomologicalComplex.IsStrictlySupported.isZero 📋 Mathlib.Algebra.Homology.Embedding.IsSupported
  {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3} {inst✝ : CategoryTheory.Category.{v_1, u_3} C} {inst✝¹ : CategoryTheory.Limits.HasZeroMorphisms C} {K : HomologicalComplex C c'} {e : c.Embedding c'} [self : K.IsStrictlySupported e] (i' : ι') (hi' : ∀ (i : ι), e.f i ≠ i') : CategoryTheory.Limits.IsZero (K.X i')
• HomologicalComplex.IsStrictlySupported.mk 📋 Mathlib.Algebra.Homology.Embedding.IsSupported
  {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3} [CategoryTheory.Category.{v_1, u_3} C] [CategoryTheory.Limits.HasZeroMorphisms C] {K : HomologicalComplex C c'} {e : c.Embedding c'} (isZero : ∀ (i' : ι'), (∀ (i : ι), e.f i ≠ i') → CategoryTheory.Limits.IsZero (K.X i')) : K.IsStrictlySupported e
• HomologicalComplex.isZero_iff_isStrictlySupported_and_isStrictlySupportedOutside 📋 Mathlib.Algebra.Homology.Embedding.IsSupported
  {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3} [CategoryTheory.Category.{v_1, u_3} C] [CategoryTheory.Limits.HasZeroMorphisms C] (K : HomologicalComplex C c') (e : c.Embedding c') : CategoryTheory.Limits.IsZero K ↔ K.IsStrictlySupported e ∧ K.IsStrictlySupportedOutside e
• HomologicalComplex.extend.isZero_X 📋 Mathlib.Algebra.Homology.Embedding.Extend
  {ι : Type u_1} {c : ComplexShape ι} {C : Type u_3} [CategoryTheory.Category.{v_1, u_3} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] (K : HomologicalComplex C c) {i : Option ι} (hi : i = none) : CategoryTheory.Limits.IsZero (HomologicalComplex.extend.X K i)
• HomologicalComplex.isZero_extend_X 📋 Mathlib.Algebra.Homology.Embedding.Extend
  {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3} [CategoryTheory.Category.{v_1, u_3} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] (K : HomologicalComplex C c) (e : c.Embedding c') (i' : ι') (hi' : ∀ (i : ι), e.f i ≠ i') : CategoryTheory.Limits.IsZero ((K.extend e).X i')
• HomologicalComplex.isZero_extend_X' 📋 Mathlib.Algebra.Homology.Embedding.Extend
  {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3} [CategoryTheory.Category.{v_1, u_3} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] (K : HomologicalComplex C c) (e : c.Embedding c') (i' : ι') (hi' : e.r i' = none) : CategoryTheory.Limits.IsZero ((K.extend e).X i')
• CochainComplex.isStrictlyLE_iff 📋 Mathlib.Algebra.Homology.Embedding.CochainComplex
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (K : CochainComplex C ℤ) (n : ℤ) : K.IsStrictlyLE n ↔ ∀ (i : ℤ), n < i → CategoryTheory.Limits.IsZero (K.X i)
• CochainComplex.isZero_of_isStrictlyGE 📋 Mathlib.Algebra.Homology.Embedding.CochainComplex
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (K : CochainComplex C ℤ) (n i : ℤ) (hi : i < n := by lia) [K.IsStrictlyGE n] : CategoryTheory.Limits.IsZero (K.X i)
• CochainComplex.isZero_of_isStrictlyLE 📋 Mathlib.Algebra.Homology.Embedding.CochainComplex
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (K : CochainComplex C ℤ) (n i : ℤ) (hi : n < i := by lia) [K.IsStrictlyLE n] : CategoryTheory.Limits.IsZero (K.X i)
• CochainComplex.isStrictlyGE_iff 📋 Mathlib.Algebra.Homology.Embedding.CochainComplex
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (K : CochainComplex C ℤ) (n : ℤ) : K.IsStrictlyGE n ↔ ∀ (i : ℤ), autoParam (i < n) CochainComplex.isStrictlyGE_iff._auto_1 → CategoryTheory.Limits.IsZero (K.X i)
• CochainComplex.isZero_of_isGE 📋 Mathlib.Algebra.Homology.Embedding.CochainComplex
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (K : CochainComplex C ℤ) (n i : ℤ) (hi : i < n := by lia) [K.IsGE n] [HomologicalComplex.HasHomology K i] : CategoryTheory.Limits.IsZero (HomologicalComplex.homology K i)
• CochainComplex.isZero_of_isLE 📋 Mathlib.Algebra.Homology.Embedding.CochainComplex
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (K : CochainComplex C ℤ) (n i : ℤ) (hi : n < i := by lia) [K.IsLE n] [HomologicalComplex.HasHomology K i] : CategoryTheory.Limits.IsZero (HomologicalComplex.homology K i)
• HomologicalComplex.isZero_single_obj_homology 📋 Mathlib.Algebra.Homology.SingleHomology
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] {ι : Type u_1} [DecidableEq ι] (c : ComplexShape ι) (j : ι) (A : C) (i : ι) (hi : i ≠ j) : CategoryTheory.Limits.IsZero (((HomologicalComplex.single C c j).obj A).homology i)
• CategoryTheory.isZero_of_hasInjectiveDimensionLT_zero 📋 Mathlib.CategoryTheory.Abelian.Injective.Dimension
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (X : C) [CategoryTheory.HasInjectiveDimensionLT X 0] : CategoryTheory.Limits.IsZero X
• CategoryTheory.Limits.IsZero.hasInjectiveDimensionLT_zero 📋 Mathlib.CategoryTheory.Abelian.Injective.Dimension
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {X : C} (hX : CategoryTheory.Limits.IsZero X) : CategoryTheory.HasInjectiveDimensionLT X 0

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 69fae59