Colimits

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

Statistics

Metric	Count
Definitions desc, ι, colimitCocone, colimitCoconeIsColimit, instAddCommGroupQuot, isColimit_of_bijective_desc, quotQuotUliftAddEquiv, quotToQuotUlift, quotUliftToQuot, toCocone, cokernelIsoQuotient	11
Theorems addMonoidHom_ext, desc_colimitCocone, desc_quotQuotUliftAddEquiv, desc_toCocone_desc, desc_toCocone_desc_app, map_ι, ι_desc, colimitCocone_pt, colimitCocone_ι_app, quotToQuotUlift_ι, quotUliftToQuot_ι, toCocone_pt_coe, toCocone_ι_app, hasColimit, hasColimit_of_small_quot, hasColimitsOfShape, hasColimitsOfSize, instSmallQuot	18
Total	29

AddCommGrpCat

Definitions

Name	Category	Theorems
cokernelIsoQuotient 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hasColimit 📖	mathematical	—	CategoryTheory.Limits.HasColimit AddCommGrpCat instCategory	—	hasColimit_of_small_quot instSmallQuot
hasColimit_of_small_quot 📖	mathematical	—	CategoryTheory.Limits.HasColimit AddCommGrpCat instCategory	—	—
hasColimitsOfShape 📖	mathematical	—	CategoryTheory.Limits.HasColimitsOfShape AddCommGrpCat instCategory	—	hasColimit
hasColimitsOfSize 📖	mathematical	—	CategoryTheory.Limits.HasColimitsOfSize AddCommGrpCat instCategory	—	hasColimitsOfShape UnivLE.small
instSmallQuot 📖	mathematical	—	Small Colimits.Quot	—	small_of_surjective DFinsupp.small UnivLE.small UnivLE.self AddSubgroup.normal_of_comm QuotientAddGroup.mk'_surjective

AddCommGrpCat.Colimits

Definitions

Name	Category	Theorems
colimitCocone 📖	CompOp	3 math math: colimitCocone_ι_app, colimitCocone_pt, Quot.desc_colimitCocone
colimitCoconeIsColimit 📖	CompOp	—
instAddCommGroupQuot 📖	CompOp	12 math math: AddCommGrpCat.isColimit_iff_bijective_desc, colimitCocone_ι_app, quotUliftToQuot_ι, colimitCocone_pt, Quot.desc_toCocone_desc, quotToQuotUlift_ι, Quot.desc_colimitCocone, Quot.desc_toCocone_desc_app, toCocone_ι_app, Quot.ι_desc, Quot.map_ι, Quot.desc_quotQuotUliftAddEquiv
isColimit_of_bijective_desc 📖	CompOp	—
quotQuotUliftAddEquiv 📖	CompOp	1 math math: Quot.desc_quotQuotUliftAddEquiv
quotToQuotUlift 📖	CompOp	1 math math: quotToQuotUlift_ι
quotUliftToQuot 📖	CompOp	1 math math: quotUliftToQuot_ι
toCocone 📖	CompOp	4 math math: Quot.desc_toCocone_desc, Quot.desc_toCocone_desc_app, toCocone_ι_app, toCocone_pt_coe

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
colimitCocone_pt 📖	mathematical	—	CategoryTheory.Limits.Cocone.pt AddCommGrpCat AddCommGrpCat.instCategory colimitCocone AddCommGrpCat.of Shrink Quot Shrink.instAddCommGroup instAddCommGroupQuot	—	—
colimitCocone_ι_app 📖	mathematical	—	CategoryTheory.NatTrans.app AddCommGrpCat AddCommGrpCat.instCategory CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const AddCommGrpCat.of Shrink Quot Shrink.instAddCommGroup instAddCommGroupQuot CategoryTheory.Limits.Cocone.ι colimitCocone AddCommGrpCat.ofHom AddCommGrpCat.carrier AddCommGrpCat.str AddMonoidHom.comp AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup Shrink.instAddZeroClass AddEquiv.toAddMonoidHom AddEquiv.symm Shrink.instAdd AddZero.toAdd Shrink.addEquiv Quot.ι	—	—
quotToQuotUlift_ι 📖	mathematical	—	DFunLike.coe AddMonoidHom Quot CategoryTheory.Functor.comp AddCommGrpCat AddCommGrpCat.instCategory AddCommGrpCat.uliftFunctor AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup instAddCommGroupQuot AddMonoidHom.instFunLike quotToQuotUlift AddCommGrpCat.carrier CategoryTheory.Functor.obj AddCommGrpCat.str Quot.ι	—	AddEquivClass.instAddMonoidHomClass AddEquiv.instAddEquivClass AddSubgroup.normal_of_comm AddMonoidHom.comp_apply QuotientAddGroup.lift_mk' DFinsupp.sumAddHom_single
quotUliftToQuot_ι 📖	mathematical	—	DFunLike.coe AddMonoidHom Quot CategoryTheory.Functor.comp AddCommGrpCat AddCommGrpCat.instCategory AddCommGrpCat.uliftFunctor AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup instAddCommGroupQuot AddMonoidHom.instFunLike quotUliftToQuot AddCommGrpCat.carrier CategoryTheory.Functor.obj AddCommGrpCat.str Quot.ι	—	AddEquivClass.instAddMonoidHomClass AddEquiv.instAddEquivClass AddSubgroup.normal_of_comm AddMonoidHom.comp_apply QuotientAddGroup.lift_mk' DFinsupp.sumAddHom_single
toCocone_pt_coe 📖	mathematical	—	AddCommGrpCat.carrier CategoryTheory.Limits.Cocone.pt AddCommGrpCat AddCommGrpCat.instCategory toCocone	—	—
toCocone_ι_app 📖	mathematical	—	CategoryTheory.NatTrans.app AddCommGrpCat AddCommGrpCat.instCategory CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const AddCommGrpCat.of CategoryTheory.Limits.Cocone.ι toCocone AddCommGrpCat.ofHom AddCommGrpCat.carrier AddCommGrpCat.str AddMonoidHom.comp Quot AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup instAddCommGroupQuot Quot.ι	—	—

AddCommGrpCat.Colimits.Quot

Definitions

Name	Category	Theorems
desc 📖	CompOp	6 math math: AddCommGrpCat.isColimit_iff_bijective_desc, desc_toCocone_desc, desc_colimitCocone, desc_toCocone_desc_app, ι_desc, desc_quotQuotUliftAddEquiv
ι 📖	CompOp	6 math math: AddCommGrpCat.Colimits.colimitCocone_ι_app, AddCommGrpCat.Colimits.quotUliftToQuot_ι, AddCommGrpCat.Colimits.quotToQuotUlift_ι, AddCommGrpCat.Colimits.toCocone_ι_app, ι_desc, map_ι

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
addMonoidHom_ext 📖	—	DFunLike.coe AddMonoidHom AddCommGrpCat.Colimits.Quot AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddCommGrpCat.Colimits.instAddCommGroupQuot AddMonoidHom.instFunLike AddCommGrpCat.carrier CategoryTheory.Functor.obj AddCommGrpCat AddCommGrpCat.instCategory AddCommGrpCat.str ι	—	—	QuotientAddGroup.addMonoidHom_ext AddSubgroup.normal_of_comm DFinsupp.addHom_ext
desc_colimitCocone 📖	mathematical	—	desc AddCommGrpCat.Colimits.colimitCocone AddEquiv.toAddMonoidHom AddCommGrpCat.Colimits.Quot Shrink AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddCommGrpCat.Colimits.instAddCommGroupQuot Shrink.instAddZeroClass AddEquiv.symm Shrink.instAdd AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid Shrink.addEquiv	—	addMonoidHom_ext ι_desc
desc_quotQuotUliftAddEquiv 📖	mathematical	—	AddMonoidHom.comp AddCommGrpCat.Colimits.Quot CategoryTheory.Functor.comp AddCommGrpCat AddCommGrpCat.instCategory AddCommGrpCat.uliftFunctor AddCommGrpCat.carrier CategoryTheory.Limits.Cocone.pt CategoryTheory.Functor.mapCocone AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddCommGrpCat.Colimits.instAddCommGroupQuot AddCommGrpCat.str desc AddEquiv.toAddMonoidHom AddCommGrpCat.Colimits.quotQuotUliftAddEquiv ULift.addZeroClass AddEquiv.symm ULift.add AddZero.toAdd AddEquiv.ulift	—	addMonoidHom_ext AddCommGrpCat.Colimits.quotToQuotUlift_ι ι_desc
desc_toCocone_desc 📖	mathematical	—	AddMonoidHom.comp AddCommGrpCat.Colimits.Quot AddCommGrpCat.carrier CategoryTheory.Limits.Cocone.pt AddCommGrpCat AddCommGrpCat.instCategory AddCommGrpCat.Colimits.toCocone AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddCommGrpCat.Colimits.instAddCommGroupQuot AddCommGrpCat.str AddCommGrpCat.Hom.hom CategoryTheory.Limits.IsColimit.desc desc	—	addMonoidHom_ext AddMonoidHom.comp_apply ι_desc CategoryTheory.Limits.IsColimit.fac
desc_toCocone_desc_app 📖	mathematical	—	DFunLike.coe CategoryTheory.Limits.Cocone.pt AddCommGrpCat AddCommGrpCat.instCategory AddCommGrpCat.Colimits.toCocone AddCommGrpCat.carrier CategoryTheory.ConcreteCategory.hom AddMonoidHom AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddCommGrpCat.str AddMonoidHom.instFunLike AddCommGrpCat.instConcreteCategoryAddMonoidHomCarrier CategoryTheory.Limits.IsColimit.desc AddCommGrpCat.Colimits.Quot AddCommGrpCat.Colimits.instAddCommGroupQuot desc	—	desc_toCocone_desc
map_ι 📖	mathematical	—	DFunLike.coe AddMonoidHom AddCommGrpCat.carrier CategoryTheory.Functor.obj AddCommGrpCat AddCommGrpCat.instCategory AddCommGrpCat.Colimits.Quot AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddCommGrpCat.str AddCommGrpCat.Colimits.instAddCommGroupQuot AddMonoidHom.instFunLike ι CategoryTheory.ConcreteCategory.hom AddCommGrpCat.instConcreteCategoryAddMonoidHomCarrier CategoryTheory.Functor.map	—	eq_of_sub_eq_zero AddSubgroup.normal_of_comm AddMonoidHom.map_sub AddMonoidHom.mem_ker QuotientAddGroup.ker_mk' AddSubgroup.subset_closure
ι_desc 📖	mathematical	—	DFunLike.coe AddMonoidHom AddCommGrpCat.Colimits.Quot AddCommGrpCat.carrier CategoryTheory.Limits.Cocone.pt AddCommGrpCat AddCommGrpCat.instCategory AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddCommGrpCat.Colimits.instAddCommGroupQuot AddCommGrpCat.str AddMonoidHom.instFunLike desc CategoryTheory.Functor.obj ι CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.ConcreteCategory.hom AddCommGrpCat.instConcreteCategoryAddMonoidHomCarrier CategoryTheory.NatTrans.app CategoryTheory.Limits.Cocone.ι	—	QuotientAddGroup.lift_mk' DFinsupp.sumAddHom_single

---

← Back to Index