Documentation Verification Report

Limits

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

Statistics

Metric	Count
Definitions `commRingObj`, `forget₂CommSemiRingPreservesLimitsAux`, `instCreatesLimitRingCatForget₂RingHomCarrierCarrier`, `limitCommRing`, `limitCone`, `limitConeIsLimit`, `commSemiringObj`, `instCreatesLimitSemiRingCatForget₂RingHomCarrierCarrier`, `limitCommSemiring`, `limitCone`, `limitConeIsLimit`, `«change_elaboration_strategy_with_`by_apply`»`, `forget₂AddCommGroupPreservesLimitsAux`, `instCreatesLimitSemiRingCatForget₂RingHomCarrierCarrier`, `limitCone`, `limitConeIsLimit`, `limitRing`, `ringObj`, `sectionsSubring`, `limitCone`, `limitConeIsLimit`, `forget₂AddCommMonPreservesLimitsAux`, `forget₂MonPreservesLimitsAux`, `limitSemiring`, `limitπRingHom`, `sectionsSemiring`, `sectionsSubsemiring`, `semiringObj`	28
Theorems `forget_preservesLimits`, `forget_preservesLimitsOfSize`, `forget₂CommSemiRing_preservesLimits`, `forget₂CommSemiRing_preservesLimitsOfSize`, `forget₂Ring_preservesLimits`, `forget₂Ring_preservesLimitsOfSize`, `hasLimit`, `hasLimits`, `hasLimitsOfShape`, `hasLimitsOfSize`, `forget_preservesLimits`, `forget_preservesLimitsOfSize`, `forget₂SemiRing_preservesLimits`, `forget₂SemiRing_preservesLimitsOfSize`, `hasLimit`, `hasLimits`, `hasLimitsOfShape`, `hasLimitsOfSize`, `forget_preservesLimits`, `forget_preservesLimitsOfSize`, `forget₂AddCommGroup_preservesLimits`, `forget₂AddCommGroup_preservesLimitsOfSize`, `forget₂SemiRing_preservesLimits`, `forget₂SemiRing_preservesLimitsOfSize`, `hasLimit`, `hasLimits`, `hasLimitsOfShape`, `hasLimitsOfSize`, `forget_preservesLimits`, `forget_preservesLimitsOfSize`, `forget₂AddCommMon_preservesLimits`, `forget₂AddCommMon_preservesLimitsOfSize`, `forget₂Mon_preservesLimits`, `forget₂Mon_preservesLimitsOfSize`, `hasLimit`, `hasLimits`, `hasLimitsOfShape`, `hasLimitsOfSize`	38
Total	66

CommRingCat

Definitions

Name	Category	Theorems
`commRingObj` 📖	CompOp	—
`forget₂CommSemiRingPreservesLimitsAux` 📖	CompOp	—
`instCreatesLimitRingCatForget₂RingHomCarrierCarrier` 📖	CompOp	—
`limitCommRing` 📖	CompOp	—
`limitCone` 📖	CompOp	—
`limitConeIsLimit` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`forget_preservesLimits` 📖	mathematical	—	`CategoryTheory.Limits.PreservesLimits` `CommRingCat` `instCategory` `CategoryTheory.types` `CategoryTheory.forget` `RingHom` `carrier` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `commRing` `RingHom.instFunLike` `instConcreteCategoryRingHomCarrier`	—	`forget_preservesLimitsOfSize` `UnivLE.self`
`forget_preservesLimitsOfSize` 📖	mathematical	—	`CategoryTheory.Limits.PreservesLimitsOfSize` `CommRingCat` `instCategory` `CategoryTheory.types` `CategoryTheory.forget` `RingHom` `carrier` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `commRing` `RingHom.instFunLike` `instConcreteCategoryRingHomCarrier`	—	`CategoryTheory.Limits.preservesLimit_of_preserves_limit_cone` `small_subtype` `small_Pi` `UnivLE.small` `UnivLE.self`
`forget₂CommSemiRing_preservesLimits` 📖	mathematical	—	`CategoryTheory.Limits.PreservesLimits` `CommRingCat` `instCategory` `CommSemiRingCat` `CommSemiRingCat.instCategory` `CategoryTheory.forget₂` `RingHom` `carrier` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `commRing` `RingHom.instFunLike` `instConcreteCategoryRingHomCarrier` `CommSemiRingCat.carrier` `CommSemiRingCat.commSemiring` `CommSemiRingCat.instConcreteCategoryRingHomCarrier` `hasForgetToAddCommMonCat`	—	`forget₂CommSemiRing_preservesLimitsOfSize` `UnivLE.self`
`forget₂CommSemiRing_preservesLimitsOfSize` 📖	mathematical	—	`CategoryTheory.Limits.PreservesLimitsOfSize` `CommRingCat` `instCategory` `CommSemiRingCat` `CommSemiRingCat.instCategory` `CategoryTheory.forget₂` `RingHom` `carrier` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `commRing` `RingHom.instFunLike` `instConcreteCategoryRingHomCarrier` `CommSemiRingCat.carrier` `CommSemiRingCat.commSemiring` `CommSemiRingCat.instConcreteCategoryRingHomCarrier` `hasForgetToAddCommMonCat`	—	`CategoryTheory.Limits.preservesLimit_of_preserves_limit_cone` `small_subtype` `small_Pi` `UnivLE.small` `UnivLE.self`
`forget₂Ring_preservesLimits` 📖	mathematical	—	`CategoryTheory.Limits.PreservesLimits` `CommRingCat` `instCategory` `RingCat` `RingCat.instCategory` `CategoryTheory.forget₂` `RingHom` `carrier` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `commRing` `RingHom.instFunLike` `instConcreteCategoryRingHomCarrier` `RingCat.carrier` `Ring.toSemiring` `RingCat.ring` `RingCat.instConcreteCategoryRingHomCarrier` `hasForgetToRingCat`	—	`forget₂Ring_preservesLimitsOfSize` `UnivLE.self`
`forget₂Ring_preservesLimitsOfSize` 📖	mathematical	—	`CategoryTheory.Limits.PreservesLimitsOfSize` `CommRingCat` `instCategory` `RingCat` `RingCat.instCategory` `CategoryTheory.forget₂` `RingHom` `carrier` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `commRing` `RingHom.instFunLike` `instConcreteCategoryRingHomCarrier` `RingCat.carrier` `Ring.toSemiring` `RingCat.ring` `RingCat.instConcreteCategoryRingHomCarrier` `hasForgetToRingCat`	—	`CategoryTheory.Limits.preservesLimit_of_preserves_limit_cone` `small_subtype` `small_Pi` `UnivLE.small` `UnivLE.self`
`hasLimit` 📖	mathematical	—	`CategoryTheory.Limits.HasLimit` `CommRingCat` `instCategory`	—	`CategoryTheory.hasLimit_of_created` `RingCat.hasLimit`
`hasLimits` 📖	mathematical	—	`CategoryTheory.Limits.HasLimits` `CommRingCat` `instCategory`	—	`hasLimitsOfSize` `UnivLE.self`
`hasLimitsOfShape` 📖	mathematical	—	`CategoryTheory.Limits.HasLimitsOfShape` `CommRingCat` `instCategory`	—	`hasLimit` `small_subtype` `small_Pi` `UnivLE.small` `UnivLE.self`
`hasLimitsOfSize` 📖	mathematical	—	`CategoryTheory.Limits.HasLimitsOfSize` `CommRingCat` `instCategory`	—	`hasLimitsOfShape` `UnivLE.small`

CommSemiRingCat

Definitions

Name	Category	Theorems
`commSemiringObj` 📖	CompOp	—
`instCreatesLimitSemiRingCatForget₂RingHomCarrierCarrier` 📖	CompOp	—
`limitCommSemiring` 📖	CompOp	—
`limitCone` 📖	CompOp	—
`limitConeIsLimit` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`forget_preservesLimits` 📖	mathematical	—	`CategoryTheory.Limits.PreservesLimits` `CommSemiRingCat` `instCategory` `CategoryTheory.types` `CategoryTheory.forget` `RingHom` `carrier` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `commSemiring` `RingHom.instFunLike` `instConcreteCategoryRingHomCarrier`	—	`forget_preservesLimitsOfSize` `UnivLE.self`
`forget_preservesLimitsOfSize` 📖	mathematical	—	`CategoryTheory.Limits.PreservesLimitsOfSize` `CommSemiRingCat` `instCategory` `CategoryTheory.types` `CategoryTheory.forget` `RingHom` `carrier` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `commSemiring` `RingHom.instFunLike` `instConcreteCategoryRingHomCarrier`	—	`CategoryTheory.Limits.preservesLimit_of_preserves_limit_cone` `small_subtype` `small_Pi` `UnivLE.small` `UnivLE.self`
`forget₂SemiRing_preservesLimits` 📖	mathematical	—	`CategoryTheory.Limits.PreservesLimits` `CommSemiRingCat` `instCategory` `SemiRingCat` `SemiRingCat.instCategory` `CategoryTheory.forget₂` `RingHom` `carrier` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `commSemiring` `RingHom.instFunLike` `instConcreteCategoryRingHomCarrier` `SemiRingCat.carrier` `SemiRingCat.semiring` `SemiRingCat.instConcreteCategoryRingHomCarrier` `hasForgetToSemiRingCat`	—	`forget₂SemiRing_preservesLimitsOfSize` `UnivLE.self`
`forget₂SemiRing_preservesLimitsOfSize` 📖	mathematical	—	`CategoryTheory.Limits.PreservesLimitsOfSize` `CommSemiRingCat` `instCategory` `SemiRingCat` `SemiRingCat.instCategory` `CategoryTheory.forget₂` `RingHom` `carrier` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `commSemiring` `RingHom.instFunLike` `instConcreteCategoryRingHomCarrier` `SemiRingCat.carrier` `SemiRingCat.semiring` `SemiRingCat.instConcreteCategoryRingHomCarrier` `hasForgetToSemiRingCat`	—	`CategoryTheory.Limits.preservesLimit_of_preserves_limit_cone` `small_subtype` `small_Pi` `UnivLE.small` `UnivLE.self`
`hasLimit` 📖	mathematical	—	`CategoryTheory.Limits.HasLimit` `CommSemiRingCat` `instCategory`	—	—
`hasLimits` 📖	mathematical	—	`CategoryTheory.Limits.HasLimits` `CommSemiRingCat` `instCategory`	—	`hasLimitsOfSize` `UnivLE.self`
`hasLimitsOfShape` 📖	mathematical	—	`CategoryTheory.Limits.HasLimitsOfShape` `CommSemiRingCat` `instCategory`	—	`hasLimit` `small_subtype` `small_Pi` `UnivLE.small` `UnivLE.self`
`hasLimitsOfSize` 📖	mathematical	—	`CategoryTheory.Limits.HasLimitsOfSize` `CommSemiRingCat` `instCategory`	—	`hasLimitsOfShape` `UnivLE.small`

LibraryNote

Definitions

Name	Category	Theorems
`«change_elaboration_strategy_with_`by_apply`»` 📖	CompOp	—

RingCat

Definitions

Name	Category	Theorems
`forget₂AddCommGroupPreservesLimitsAux` 📖	CompOp	—
`instCreatesLimitSemiRingCatForget₂RingHomCarrierCarrier` 📖	CompOp	—
`limitCone` 📖	CompOp	—
`limitConeIsLimit` 📖	CompOp	—
`limitRing` 📖	CompOp	—
`ringObj` 📖	CompOp	—
`sectionsSubring` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`forget_preservesLimits` 📖	mathematical	—	`CategoryTheory.Limits.PreservesLimits` `RingCat` `instCategory` `CategoryTheory.types` `CategoryTheory.forget` `RingHom` `carrier` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `ring` `RingHom.instFunLike` `instConcreteCategoryRingHomCarrier`	—	`forget_preservesLimitsOfSize` `UnivLE.self`
`forget_preservesLimitsOfSize` 📖	mathematical	—	`CategoryTheory.Limits.PreservesLimitsOfSize` `RingCat` `instCategory` `CategoryTheory.types` `CategoryTheory.forget` `RingHom` `carrier` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `ring` `RingHom.instFunLike` `instConcreteCategoryRingHomCarrier`	—	`CategoryTheory.Limits.preservesLimit_of_preserves_limit_cone` `small_subtype` `small_Pi` `UnivLE.small` `UnivLE.self`
`forget₂AddCommGroup_preservesLimits` 📖	mathematical	—	`CategoryTheory.Limits.PreservesLimits` `RingCat` `instCategory` `AddCommGrpCat` `AddCommGrpCat.instCategory` `CategoryTheory.forget₂` `RingHom` `carrier` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `ring` `RingHom.instFunLike` `instConcreteCategoryRingHomCarrier` `AddMonoidHom` `AddCommGrpCat.carrier` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `AddCommGrpCat.str` `AddMonoidHom.instFunLike` `AddCommGrpCat.instConcreteCategoryAddMonoidHomCarrier` `hasForgetToAddCommGrp`	—	`forget₂AddCommGroup_preservesLimitsOfSize` `UnivLE.self`
`forget₂AddCommGroup_preservesLimitsOfSize` 📖	mathematical	—	`CategoryTheory.Limits.PreservesLimitsOfSize` `RingCat` `instCategory` `AddCommGrpCat` `AddCommGrpCat.instCategory` `CategoryTheory.forget₂` `RingHom` `carrier` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `ring` `RingHom.instFunLike` `instConcreteCategoryRingHomCarrier` `AddMonoidHom` `AddCommGrpCat.carrier` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `AddCommGrpCat.str` `AddMonoidHom.instFunLike` `AddCommGrpCat.instConcreteCategoryAddMonoidHomCarrier` `hasForgetToAddCommGrp`	—	`CategoryTheory.Limits.preservesLimit_of_preserves_limit_cone` `small_subtype` `small_Pi` `UnivLE.small` `UnivLE.self`
`forget₂SemiRing_preservesLimits` 📖	mathematical	—	`CategoryTheory.Limits.PreservesLimits` `RingCat` `instCategory` `SemiRingCat` `SemiRingCat.instCategory` `CategoryTheory.forget₂` `RingHom` `carrier` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `ring` `RingHom.instFunLike` `instConcreteCategoryRingHomCarrier` `SemiRingCat.carrier` `SemiRingCat.semiring` `SemiRingCat.instConcreteCategoryRingHomCarrier` `hasForgetToSemiRingCat`	—	`forget₂SemiRing_preservesLimitsOfSize` `UnivLE.self`
`forget₂SemiRing_preservesLimitsOfSize` 📖	mathematical	—	`CategoryTheory.Limits.PreservesLimitsOfSize` `RingCat` `instCategory` `SemiRingCat` `SemiRingCat.instCategory` `CategoryTheory.forget₂` `RingHom` `carrier` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `ring` `RingHom.instFunLike` `instConcreteCategoryRingHomCarrier` `SemiRingCat.carrier` `SemiRingCat.semiring` `SemiRingCat.instConcreteCategoryRingHomCarrier` `hasForgetToSemiRingCat`	—	`CategoryTheory.Limits.preservesLimit_of_preserves_limit_cone` `small_subtype` `small_Pi` `UnivLE.small` `UnivLE.self`
`hasLimit` 📖	mathematical	—	`CategoryTheory.Limits.HasLimit` `RingCat` `instCategory`	—	`CategoryTheory.hasLimit_of_created` `SemiRingCat.hasLimit`
`hasLimits` 📖	mathematical	—	`CategoryTheory.Limits.HasLimits` `RingCat` `instCategory`	—	`hasLimitsOfSize` `UnivLE.self`
`hasLimitsOfShape` 📖	mathematical	—	`CategoryTheory.Limits.HasLimitsOfShape` `RingCat` `instCategory`	—	`hasLimit` `small_subtype` `small_Pi` `UnivLE.small` `UnivLE.self`
`hasLimitsOfSize` 📖	mathematical	—	`CategoryTheory.Limits.HasLimitsOfSize` `RingCat` `instCategory`	—	`hasLimitsOfShape` `UnivLE.small`

SemiRingCat

Definitions

Name	Category	Theorems
`forget₂AddCommMonPreservesLimitsAux` 📖	CompOp	—
`forget₂MonPreservesLimitsAux` 📖	CompOp	—
`limitSemiring` 📖	CompOp	—
`limitπRingHom` 📖	CompOp	—
`sectionsSemiring` 📖	CompOp	—
`sectionsSubsemiring` 📖	CompOp	—
`semiringObj` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`forget_preservesLimits` 📖	mathematical	—	`CategoryTheory.Limits.PreservesLimits` `SemiRingCat` `instCategory` `CategoryTheory.types` `CategoryTheory.forget` `RingHom` `carrier` `Semiring.toNonAssocSemiring` `semiring` `RingHom.instFunLike` `instConcreteCategoryRingHomCarrier`	—	`forget_preservesLimitsOfSize` `UnivLE.self`
`forget_preservesLimitsOfSize` 📖	mathematical	—	`CategoryTheory.Limits.PreservesLimitsOfSize` `SemiRingCat` `instCategory` `CategoryTheory.types` `CategoryTheory.forget` `RingHom` `carrier` `Semiring.toNonAssocSemiring` `semiring` `RingHom.instFunLike` `instConcreteCategoryRingHomCarrier`	—	`CategoryTheory.Limits.preservesLimit_of_preserves_limit_cone` `small_subtype` `small_Pi` `UnivLE.small` `UnivLE.self`
`forget₂AddCommMon_preservesLimits` 📖	mathematical	—	`CategoryTheory.Limits.PreservesLimits` `SemiRingCat` `instCategory` `AddCommMonCat` `AddCommMonCat.instCategory` `CategoryTheory.forget₂` `RingHom` `carrier` `Semiring.toNonAssocSemiring` `semiring` `RingHom.instFunLike` `instConcreteCategoryRingHomCarrier` `AddMonoidHom` `AddCommMonCat.carrier` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `AddCommMonCat.str` `AddMonoidHom.instFunLike` `AddCommMonCat.instConcreteCategoryAddMonoidHomCarrier` `hasForgetToAddCommMonCat`	—	`forget₂AddCommMon_preservesLimitsOfSize` `UnivLE.self`
`forget₂AddCommMon_preservesLimitsOfSize` 📖	mathematical	—	`CategoryTheory.Limits.PreservesLimitsOfSize` `SemiRingCat` `instCategory` `AddCommMonCat` `AddCommMonCat.instCategory` `CategoryTheory.forget₂` `RingHom` `carrier` `Semiring.toNonAssocSemiring` `semiring` `RingHom.instFunLike` `instConcreteCategoryRingHomCarrier` `AddMonoidHom` `AddCommMonCat.carrier` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `AddCommMonCat.str` `AddMonoidHom.instFunLike` `AddCommMonCat.instConcreteCategoryAddMonoidHomCarrier` `hasForgetToAddCommMonCat`	—	`CategoryTheory.Limits.preservesLimit_of_preserves_limit_cone` `small_subtype` `small_Pi` `UnivLE.small` `UnivLE.self`
`forget₂Mon_preservesLimits` 📖	mathematical	—	`CategoryTheory.Limits.PreservesLimits` `SemiRingCat` `instCategory` `MonCat` `MonCat.instCategory` `CategoryTheory.forget₂` `RingHom` `carrier` `Semiring.toNonAssocSemiring` `semiring` `RingHom.instFunLike` `instConcreteCategoryRingHomCarrier` `MonoidHom` `MonCat.carrier` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MonCat.str` `MonoidHom.instFunLike` `MonCat.instConcreteCategoryMonoidHomCarrier` `hasForgetToMonCat`	—	`forget₂Mon_preservesLimitsOfSize` `UnivLE.self`
`forget₂Mon_preservesLimitsOfSize` 📖	mathematical	—	`CategoryTheory.Limits.PreservesLimitsOfSize` `SemiRingCat` `instCategory` `MonCat` `MonCat.instCategory` `CategoryTheory.forget₂` `RingHom` `carrier` `Semiring.toNonAssocSemiring` `semiring` `RingHom.instFunLike` `instConcreteCategoryRingHomCarrier` `MonoidHom` `MonCat.carrier` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MonCat.str` `MonoidHom.instFunLike` `MonCat.instConcreteCategoryMonoidHomCarrier` `hasForgetToMonCat`	—	`CategoryTheory.Limits.preservesLimit_of_preserves_limit_cone` `small_subtype` `small_Pi` `UnivLE.small` `UnivLE.self`
`hasLimit` 📖	mathematical	—	`CategoryTheory.Limits.HasLimit` `SemiRingCat` `instCategory`	—	—
`hasLimits` 📖	mathematical	—	`CategoryTheory.Limits.HasLimits` `SemiRingCat` `instCategory`	—	`hasLimitsOfSize` `UnivLE.self`
`hasLimitsOfShape` 📖	mathematical	—	`CategoryTheory.Limits.HasLimitsOfShape` `SemiRingCat` `instCategory`	—	`hasLimit` `small_subtype` `small_Pi` `UnivLE.small` `UnivLE.self`
`hasLimitsOfSize` 📖	mathematical	—	`CategoryTheory.Limits.HasLimitsOfSize` `SemiRingCat` `instCategory`	—	`hasLimit` `small_subtype` `small_Pi` `UnivLE.small` `UnivLE.self`

SemiRingCat.HasLimits

Definitions

Name	Category	Theorems
`limitCone` 📖	CompOp	—
`limitConeIsLimit` 📖	CompOp	—

---

← Back to Index