HomologicalComplex

📁 Source: Mathlib/CategoryTheory/Generator/HomologicalComplex.lean

Statistics

Metric	Count
Definitions separatingFamily	1
Theorems instHasSeparator, isSeparating_separatingFamily, isSeparator_coproduct_separatingFamily	3
Total	4

HomologicalComplex

Definitions

Name	Category	Theorems
separatingFamily 📖	CompOp	2 math math: isSeparator_coproduct_separatingFamily, isSeparating_separatingFamily

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instHasSeparator 📖	mathematical	—	CategoryTheory.HasSeparator HomologicalComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms instCategory	—	instHasColimit CategoryTheory.Limits.instHasColimitCompOfPreservesColimit CategoryTheory.Limits.hasColimitOfHasColimitsOfShape instHasColimitsOfShape CategoryTheory.Limits.PreservesColimitsOfShape.preservesColimit instPreservesColimitsOfShapeEvalOfHasColimitsOfShape isSeparator_coproduct_separatingFamily CategoryTheory.isSeparator_separator
isSeparating_separatingFamily 📖	mathematical	CategoryTheory.ObjectProperty.IsSeparating CategoryTheory.ObjectProperty.ofObj CategoryTheory.Category.toCategoryStruct	HomologicalComplex instCategory separatingFamily	—	hom_ext Equiv.injective CategoryTheory.Functor.CorepresentableBy.homEquiv_symm_comp CategoryTheory.ObjectProperty.ofObj_apply
isSeparator_coproduct_separatingFamily 📖	mathematical	CategoryTheory.IsSeparator	HomologicalComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms instCategory CategoryTheory.Limits.sigmaObj separatingFamily instHasColimit CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Discrete.functor CategoryTheory.Limits.instHasColimitCompOfPreservesColimit CategoryTheory.Limits.hasColimitOfHasColimitsOfShape instHasColimitsOfShape eval CategoryTheory.Limits.PreservesColimitsOfShape.preservesColimit instPreservesColimitsOfShapeEvalOfHasColimitsOfShape	—	CategoryTheory.isSeparator_of_isColimit_cofan isSeparating_separatingFamily instHasColimit CategoryTheory.Limits.hasColimitOfHasColimitsOfShape

---

← Back to Index