AB

📁 Source: Mathlib/Algebra/Category/Grp/AB.lean

Statistics

Metric	Count
Definitions	0
Theorems instAB4AddCommGrpCat, instAB4StarAddCommGrpCat, instAB5AddCommGrpCat, instAdditiveFunctorColim, instHasExactLimitsOfShapeDiscreteAddCommGrpCat, instHasFilteredColimitsAddCommGrpCat, instPreservesFiniteLimitsFunctorAddCommGrpCatColim, instPreservesHomologyFunctorAddCommGrpCatColim	8
Total	8

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instAB4AddCommGrpCat 📖	mathematical	—	CategoryTheory.AB4 AddCommGrpCat AddCommGrpCat.instCategory AddCommGrpCat.hasColimitsOfShape CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.instSmallDiscrete UnivLE.small UnivLE.self	—	CategoryTheory.AB4.of_AB5 AddCommGrpCat.instHasFiniteBiproducts CategoryTheory.Limits.hasFiniteLimits_of_hasCountableLimits CategoryTheory.Limits.hasCountableLimits_of_hasLimits AddCommGrpCat.hasLimits instHasFilteredColimitsAddCommGrpCat instAB5AddCommGrpCat
instAB4StarAddCommGrpCat 📖	mathematical	—	CategoryTheory.AB4Star AddCommGrpCat AddCommGrpCat.instCategory AddCommGrpCat.hasLimitsOfShape CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.instSmallDiscrete UnivLE.small UnivLE.self	—	AddCommGrpCat.hasLimitsOfShape CategoryTheory.instSmallDiscrete UnivLE.small UnivLE.self instHasExactLimitsOfShapeDiscreteAddCommGrpCat
instAB5AddCommGrpCat 📖	mathematical	—	CategoryTheory.AB5 AddCommGrpCat AddCommGrpCat.instCategory instHasFilteredColimitsAddCommGrpCat	—	instHasFilteredColimitsAddCommGrpCat CategoryTheory.Limits.hasColimitsOfShape_of_has_filtered_colimits instPreservesFiniteLimitsFunctorAddCommGrpCatColim
instAdditiveFunctorColim 📖	mathematical	—	CategoryTheory.Functor.Additive CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.functorCategoryPreadditive CategoryTheory.Limits.colim	—	CategoryTheory.Limits.colimit.hom_ext CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.ι_colimMap CategoryTheory.Preadditive.add_comp CategoryTheory.Preadditive.comp_add
instHasExactLimitsOfShapeDiscreteAddCommGrpCat 📖	mathematical	—	CategoryTheory.HasExactLimitsOfShape CategoryTheory.Discrete CategoryTheory.discreteCategory AddCommGrpCat AddCommGrpCat.instCategory AddCommGrpCat.hasLimitsOfShape CategoryTheory.instSmallDiscrete UnivLE.small UnivLE.self	—	CategoryTheory.hasExactLimitsOfShape_of_preservesEpi AddCommGrpCat.hasLimitsOfShape CategoryTheory.instSmallDiscrete UnivLE.small UnivLE.self AddCommGrpCat.hasLimit small_subtype small_Pi CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Category.assoc CategoryTheory.Limits.limit.lift_map_assoc CategoryTheory.Limits.limit.lift_π CategoryTheory.Limits.limit.lift_π_assoc AddCommGrpCat.epi_iff_surjective CategoryTheory.Limits.hasColimitsOfShape_widePushoutShape Finite.of_fintype CategoryTheory.Limits.hasFiniteWidePushouts_of_has_finite_limits CategoryTheory.Limits.hasFiniteColimits_of_hasCountableColimits CategoryTheory.Limits.hasCountableColimits_of_hasColimits AddCommGrpCat.hasColimitsOfSize CategoryTheory.epi_comp CategoryTheory.epi_of_effectiveEpi CategoryTheory.instEffectiveEpiOfIsIso CategoryTheory.Iso.isIso_hom CategoryTheory.Iso.isIso_inv CategoryTheory.Iso.hom_inv_id CategoryTheory.Category.comp_id CategoryTheory.Iso.hom_inv_id_assoc
instHasFilteredColimitsAddCommGrpCat 📖	mathematical	—	CategoryTheory.Limits.HasFilteredColimits AddCommGrpCat AddCommGrpCat.instCategory	—	AddCommGrpCat.hasColimitsOfShape UnivLE.small UnivLE.self
instPreservesFiniteLimitsFunctorAddCommGrpCatColim 📖	mathematical	—	CategoryTheory.Limits.PreservesFiniteLimits CategoryTheory.Functor AddCommGrpCat AddCommGrpCat.instCategory CategoryTheory.Functor.category CategoryTheory.Limits.colim AddCommGrpCat.hasColimitsOfShape UnivLE.small UnivLE.self	—	CategoryTheory.Functor.preservesFiniteLimits_of_preservesHomology AddCommGrpCat.hasColimitsOfShape UnivLE.small UnivLE.self instAdditiveFunctorColim instPreservesHomologyFunctorAddCommGrpCatColim CategoryTheory.Limits.HasZeroObject.instFunctor CategoryTheory.Abelian.hasZeroObject CategoryTheory.Limits.instHasFiniteProductsFunctor CategoryTheory.Limits.hasFiniteProducts_of_hasCountableProducts CategoryTheory.Limits.hasCountableProducts_of_hasCountableLimits CategoryTheory.Limits.hasCountableLimits_of_hasLimits AddCommGrpCat.hasLimits CategoryTheory.Abelian.has_kernels
instPreservesHomologyFunctorAddCommGrpCatColim 📖	mathematical	—	CategoryTheory.Functor.PreservesHomology CategoryTheory.Functor AddCommGrpCat AddCommGrpCat.instCategory CategoryTheory.Functor.category CategoryTheory.Limits.instHasZeroMorphismsFunctor CategoryTheory.Preadditive.preadditiveHasZeroMorphisms AddCommGrpCat.instPreadditive CategoryTheory.Limits.colim AddCommGrpCat.hasColimitsOfShape UnivLE.small UnivLE.self CategoryTheory.Functor.preservesZeroMorphisms_of_additive CategoryTheory.functorCategoryPreadditive instAdditiveFunctorColim	—	CategoryTheory.Functor.preservesHomology_of_map_exact AddCommGrpCat.hasColimitsOfShape UnivLE.small UnivLE.self CategoryTheory.Functor.preservesZeroMorphisms_of_additive instAdditiveFunctorColim CategoryTheory.Functor.preservesZeroMorphisms_evaluation_obj CategoryTheory.ShortComplex.Exact.map CategoryTheory.Functor.PreservesHomology.preservesLeftHomologyOf CategoryTheory.Functor.preservesHomologyOfExact CategoryTheory.Limits.instPreservesFiniteLimitsFunctorObjEvaluationOfHasFiniteLimits CategoryTheory.Limits.hasFiniteLimits_of_hasCountableLimits CategoryTheory.Limits.hasCountableLimits_of_hasLimits AddCommGrpCat.hasLimits CategoryTheory.Limits.instPreservesFiniteColimitsFunctorObjEvaluationOfHasFiniteColimits CategoryTheory.Limits.hasFiniteColimits_of_hasCountableColimits CategoryTheory.Limits.hasCountableColimits_of_hasColimits AddCommGrpCat.hasColimitsOfSize CategoryTheory.Functor.PreservesHomology.preservesRightHomologyOf CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.Concrete.colimit_exists_rep CategoryTheory.Limits.PreservesColimitsOfShape.preservesColimit CategoryTheory.Limits.PreservesFilteredColimitsOfSize.preserves_filtered_colimits AddCommGrpCat.FilteredColimits.forget_preservesFilteredColimits CategoryTheory.Limits.Concrete.colimit_exists_of_rep_eq AddCommGrpCat.hasColimit map_zero AddMonoidHomClass.toZeroHomClass AddMonoidHom.instAddMonoidHomClass CategoryTheory.ConcreteCategory.comp_apply CategoryTheory.Limits.colimit.ι_map CategoryTheory.Limits.colimMap_eq CategoryTheory.NatTrans.naturality CategoryTheory.Limits.colimit.w_apply

---

← Back to Index