Theorems · Theorem · category theory

HomologicalComplex.isSeparating_separatingFamily

∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {ι : Type w} (c : ComplexShape ι) [c.HasNoLoop]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : CategoryTheory.Limits.HasZeroObject C] {α : Type t}
  {X : α → C},
  (CategoryTheory.ObjectProperty.ofObj X).IsSeparating →
    (CategoryTheory.ObjectProperty.ofObj (HomologicalComplex.separatingFamily c X)).IsSeparating

Defined in

Mathlib.CategoryTheory.Generator.HomologicalComplex

Cited by

1 results in Mathlib

Foundations

Depth 33 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.CategoryComplexShape.HasNoLoopCategoryTheory.Limits.HasZeroMorphismsCategoryTheory.Limits.HasZeroObject