Documentation Verification Report

Colimits

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

Statistics

Metric	Count
Definitions `AddGroup`, `AddGroupWithOne`, `instAdd`, `instNeg`, `instZero`, `InhabitedColimitType`, `Prequotient`, `coconeFun`, `coconeMorphism`, `colimit`, `colimitCocone`, `colimitIsColimit`, `colimitSetoid`, `descFun`, `descFunLift`, `descMorphism`, `instCommRingColimitType`, `instInhabitedPrequotient`, `AddGroup`, `AddGroupWithOne`, `instAdd`, `instNeg`, `instZero`, `InhabitedColimitType`, `Prequotient`, `coconeFun`, `coconeMorphism`, `colimit`, `colimitCocone`, `colimitIsColimit`, `colimitSetoid`, `descFun`, `descFunLift`, `descMorphism`, `instInhabitedPrequotient`, `instRingColimitType`	36
Theorems `cocone_naturality`, `cocone_naturality_components`, `hasColimits_commRingCat`, `quot_add`, `quot_mul`, `quot_neg`, `quot_one`, `quot_zero`, `cocone_naturality`, `cocone_naturality_components`, `hasColimits_ringCat`, `quot_add`, `quot_mul`, `quot_neg`, `quot_one`, `quot_zero`	16
Total	52

CommRingCat.Colimits

Definitions

Name	Category	Theorems
`InhabitedColimitType` 📖	CompOp	—
`Prequotient` 📖	CompData	5 math math: `quot_add`, `quot_one`, `quot_zero`, `quot_mul`, `quot_neg`
`coconeFun` 📖	CompOp	—
`coconeMorphism` 📖	CompOp	2 math math: `cocone_naturality`, `cocone_naturality_components`
`colimit` 📖	CompOp	2 math math: `cocone_naturality`, `cocone_naturality_components`
`colimitCocone` 📖	CompOp	—
`colimitIsColimit` 📖	CompOp	—
`colimitSetoid` 📖	CompOp	5 math math: `quot_add`, `quot_one`, `quot_zero`, `quot_mul`, `quot_neg`
`descFun` 📖	CompOp	—
`descFunLift` 📖	CompOp	—
`descMorphism` 📖	CompOp	—
`instCommRingColimitType` 📖	CompOp	1 math math: `quot_mul`
`instInhabitedPrequotient` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cocone_naturality` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CommRingCat` `CategoryTheory.Category.toCategoryStruct` `CommRingCat.instCategory` `CategoryTheory.Functor.obj` `colimit` `CategoryTheory.Functor.map` `coconeMorphism`	—	`CommRingCat.hom_ext` `RingHom.ext`
`cocone_naturality_components` 📖	mathematical	—	`DFunLike.coe` `CategoryTheory.Functor.obj` `CommRingCat` `CommRingCat.instCategory` `colimit` `CommRingCat.carrier` `CategoryTheory.ConcreteCategory.hom` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `CommRingCat.commRing` `RingHom.instFunLike` `CommRingCat.instConcreteCategoryRingHomCarrier` `coconeMorphism` `CategoryTheory.Functor.map`	—	`cocone_naturality` `CommRingCat.comp_apply`
`hasColimits_commRingCat` 📖	mathematical	—	`CategoryTheory.Limits.HasColimits` `CommRingCat` `CommRingCat.instCategory`	—	—
`quot_add` 📖	mathematical	—	`Prequotient` `colimitSetoid` `Prequotient.add` `ColimitType` `ColimitType.instAdd`	—	—
`quot_mul` 📖	mathematical	—	`Prequotient` `colimitSetoid` `Prequotient.mul` `ColimitType` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `instCommRingColimitType`	—	—
`quot_neg` 📖	mathematical	—	`Prequotient` `colimitSetoid` `Prequotient.neg` `ColimitType` `ColimitType.instNeg`	—	—
`quot_one` 📖	mathematical	—	`Prequotient` `colimitSetoid` `Prequotient.one` `ColimitType` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `ColimitType.AddGroupWithOne`	—	—
`quot_zero` 📖	mathematical	—	`Prequotient` `colimitSetoid` `Prequotient.zero` `ColimitType` `ColimitType.instZero`	—	—

CommRingCat.Colimits.ColimitType

Definitions

Name	Category	Theorems
`AddGroup` 📖	CompOp	—
`AddGroupWithOne` 📖	CompOp	1 math math: `CommRingCat.Colimits.quot_one`
`instAdd` 📖	CompOp	1 math math: `CommRingCat.Colimits.quot_add`
`instNeg` 📖	CompOp	1 math math: `CommRingCat.Colimits.quot_neg`
`instZero` 📖	CompOp	1 math math: `CommRingCat.Colimits.quot_zero`

RingCat.Colimits

Definitions

Name	Category	Theorems
`InhabitedColimitType` 📖	CompOp	—
`Prequotient` 📖	CompData	5 math math: `quot_neg`, `quot_add`, `quot_mul`, `quot_one`, `quot_zero`
`coconeFun` 📖	CompOp	—
`coconeMorphism` 📖	CompOp	2 math math: `cocone_naturality_components`, `cocone_naturality`
`colimit` 📖	CompOp	2 math math: `cocone_naturality_components`, `cocone_naturality`
`colimitCocone` 📖	CompOp	—
`colimitIsColimit` 📖	CompOp	—
`colimitSetoid` 📖	CompOp	5 math math: `quot_neg`, `quot_add`, `quot_mul`, `quot_one`, `quot_zero`
`descFun` 📖	CompOp	—
`descFunLift` 📖	CompOp	—
`descMorphism` 📖	CompOp	—
`instInhabitedPrequotient` 📖	CompOp	—
`instRingColimitType` 📖	CompOp	1 math math: `quot_mul`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cocone_naturality` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `RingCat` `CategoryTheory.Category.toCategoryStruct` `RingCat.instCategory` `CategoryTheory.Functor.obj` `colimit` `CategoryTheory.Functor.map` `coconeMorphism`	—	`RingCat.hom_ext` `RingHom.ext`
`cocone_naturality_components` 📖	mathematical	—	`DFunLike.coe` `CategoryTheory.Functor.obj` `RingCat` `RingCat.instCategory` `colimit` `RingCat.carrier` `CategoryTheory.ConcreteCategory.hom` `RingHom` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `RingCat.ring` `RingHom.instFunLike` `RingCat.instConcreteCategoryRingHomCarrier` `coconeMorphism` `CategoryTheory.Functor.map`	—	`cocone_naturality` `RingCat.comp_apply`
`hasColimits_ringCat` 📖	mathematical	—	`CategoryTheory.Limits.HasColimits` `RingCat` `RingCat.instCategory`	—	—
`quot_add` 📖	mathematical	—	`Prequotient` `colimitSetoid` `Prequotient.add` `ColimitType` `ColimitType.instAdd`	—	—
`quot_mul` 📖	mathematical	—	`Prequotient` `colimitSetoid` `Prequotient.mul` `ColimitType` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `instRingColimitType`	—	—
`quot_neg` 📖	mathematical	—	`Prequotient` `colimitSetoid` `Prequotient.neg` `ColimitType` `ColimitType.instNeg`	—	—
`quot_one` 📖	mathematical	—	`Prequotient` `colimitSetoid` `Prequotient.one` `ColimitType` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `ColimitType.AddGroupWithOne`	—	—
`quot_zero` 📖	mathematical	—	`Prequotient` `colimitSetoid` `Prequotient.zero` `ColimitType` `ColimitType.instZero`	—	—

RingCat.Colimits.ColimitType

Definitions

Name	Category	Theorems
`AddGroup` 📖	CompOp	—
`AddGroupWithOne` 📖	CompOp	1 math math: `RingCat.Colimits.quot_one`
`instAdd` 📖	CompOp	1 math math: `RingCat.Colimits.quot_add`
`instNeg` 📖	CompOp	1 math math: `RingCat.Colimits.quot_neg`
`instZero` 📖	CompOp	1 math math: `RingCat.Colimits.quot_zero`

---

← Back to Index