Documentation Verification Report

Limits

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

Statistics

Metric	Count
Definitions `limitCone`, `limitConeIsLimit`, `algebraObj`, `instAlgebraElemForallObjCompForgetAlgHomCarrierSections`, `instRingElemForallObjCompForgetAlgHomCarrierSections`, `limitAlgebra`, `limitSemiring`, `limitπAlgHom`, `sectionsSubalgebra`, `semiringObj`	10
Theorems `forget_preservesLimits`, `forget_preservesLimitsOfSize`, `forget₂Module_preservesLimits`, `forget₂Module_preservesLimitsOfSize`, `forget₂Ring_preservesLimits`, `forget₂Ring_preservesLimitsOfSize`, `hasLimits`, `hasLimitsOfSize`, `instSmallSubtypeForallCarrierObjMemSubalgebraSectionsSubalgebra`	9
Total	19

AlgCat

Definitions

Name	Category	Theorems
`algebraObj` 📖	CompOp	—
`instAlgebraElemForallObjCompForgetAlgHomCarrierSections` 📖	CompOp	—
`instRingElemForallObjCompForgetAlgHomCarrierSections` 📖	CompOp	—
`limitAlgebra` 📖	CompOp	—
`limitSemiring` 📖	CompOp	—
`limitπAlgHom` 📖	CompOp	—
`sectionsSubalgebra` 📖	CompOp	1 math math: `instSmallSubtypeForallCarrierObjMemSubalgebraSectionsSubalgebra`
`semiringObj` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`forget_preservesLimits` 📖	mathematical	—	`CategoryTheory.Limits.PreservesLimits` `AlgCat` `instCategory` `CategoryTheory.types` `CategoryTheory.forget` `AlgHom` `carrier` `CommRing.toCommSemiring` `Ring.toSemiring` `isRing` `isAlgebra` `AlgHom.funLike` `instConcreteCategoryAlgHomCarrier`	—	`forget_preservesLimitsOfSize` `UnivLE.self`
`forget_preservesLimitsOfSize` 📖	mathematical	—	`CategoryTheory.Limits.PreservesLimitsOfSize` `AlgCat` `instCategory` `CategoryTheory.types` `CategoryTheory.forget` `AlgHom` `carrier` `CommRing.toCommSemiring` `Ring.toSemiring` `isRing` `isAlgebra` `AlgHom.funLike` `instConcreteCategoryAlgHomCarrier`	—	`CategoryTheory.Limits.preservesLimit_of_preserves_limit_cone` `small_subtype` `small_Pi` `UnivLE.small` `UnivLE.self`
`forget₂Module_preservesLimits` 📖	mathematical	—	`CategoryTheory.Limits.PreservesLimits` `AlgCat` `instCategory` `ModuleCat` `CommRing.toRing` `ModuleCat.moduleCategory` `CategoryTheory.forget₂` `AlgHom` `carrier` `CommRing.toCommSemiring` `Ring.toSemiring` `isRing` `isAlgebra` `AlgHom.funLike` `instConcreteCategoryAlgHomCarrier` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `ModuleCat.carrier` `AddCommGroup.toAddCommMonoid` `ModuleCat.isAddCommGroup` `ModuleCat.isModule` `LinearMap.instFunLike` `ModuleCat.instConcreteCategoryLinearMapIdCarrier` `hasForgetToModule`	—	`forget₂Module_preservesLimitsOfSize` `UnivLE.self`
`forget₂Module_preservesLimitsOfSize` 📖	mathematical	—	`CategoryTheory.Limits.PreservesLimitsOfSize` `AlgCat` `instCategory` `ModuleCat` `CommRing.toRing` `ModuleCat.moduleCategory` `CategoryTheory.forget₂` `AlgHom` `carrier` `CommRing.toCommSemiring` `Ring.toSemiring` `isRing` `isAlgebra` `AlgHom.funLike` `instConcreteCategoryAlgHomCarrier` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `ModuleCat.carrier` `AddCommGroup.toAddCommMonoid` `ModuleCat.isAddCommGroup` `ModuleCat.isModule` `LinearMap.instFunLike` `ModuleCat.instConcreteCategoryLinearMapIdCarrier` `hasForgetToModule`	—	`CategoryTheory.Limits.preservesLimit_of_preserves_limit_cone` `small_subtype` `small_Pi` `UnivLE.small` `UnivLE.self`
`forget₂Ring_preservesLimits` 📖	mathematical	—	`CategoryTheory.Limits.PreservesLimits` `AlgCat` `instCategory` `RingCat` `RingCat.instCategory` `CategoryTheory.forget₂` `AlgHom` `carrier` `CommRing.toCommSemiring` `Ring.toSemiring` `isRing` `isAlgebra` `AlgHom.funLike` `instConcreteCategoryAlgHomCarrier` `RingHom` `RingCat.carrier` `Semiring.toNonAssocSemiring` `RingCat.ring` `RingHom.instFunLike` `RingCat.instConcreteCategoryRingHomCarrier` `hasForgetToRing`	—	`forget₂Ring_preservesLimitsOfSize` `UnivLE.self`
`forget₂Ring_preservesLimitsOfSize` 📖	mathematical	—	`CategoryTheory.Limits.PreservesLimitsOfSize` `AlgCat` `instCategory` `RingCat` `RingCat.instCategory` `CategoryTheory.forget₂` `AlgHom` `carrier` `CommRing.toCommSemiring` `Ring.toSemiring` `isRing` `isAlgebra` `AlgHom.funLike` `instConcreteCategoryAlgHomCarrier` `RingHom` `RingCat.carrier` `Semiring.toNonAssocSemiring` `RingCat.ring` `RingHom.instFunLike` `RingCat.instConcreteCategoryRingHomCarrier` `hasForgetToRing`	—	`CategoryTheory.Limits.preservesLimit_of_preserves_limit_cone` `small_subtype` `small_Pi` `UnivLE.small` `UnivLE.self`
`hasLimits` 📖	mathematical	—	`CategoryTheory.Limits.HasLimits` `AlgCat` `instCategory`	—	`hasLimitsOfSize` `UnivLE.self`
`hasLimitsOfSize` 📖	mathematical	—	`CategoryTheory.Limits.HasLimitsOfSize` `AlgCat` `instCategory`	—	`small_subtype` `small_Pi` `UnivLE.small` `UnivLE.self`
`instSmallSubtypeForallCarrierObjMemSubalgebraSectionsSubalgebra` 📖	mathematical	—	`Small` `Subalgebra` `CommRing.toCommSemiring` `Pi.semiring` `carrier` `CategoryTheory.Functor.obj` `AlgCat` `instCategory` `Ring.toSemiring` `isRing` `Pi.algebra` `isAlgebra` `SetLike.instMembership` `Subalgebra.instSetLike` `sectionsSubalgebra`	—	—

AlgCat.HasLimits

Definitions

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

---

← Back to Index