Documentation Verification Report

Limits

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

Statistics

Metric	Count
Definitions `forget₂CreatesLimit`, `instCreatesLimitsOfShapeModuleCatForget₂LinearMapIdCarrierObjIsFG`	2
Theorems `instFiniteCarrierLimitModuleCatCompForget₂LinearMapIdObjIsFG`, `instFiniteCarrierPiObjModuleCatOfFinite`, `instHasFiniteLimits`, `instHasLimitsOfShapeOfFinCategory`, `instPreservesFiniteLimitsModuleCatForget₂LinearMapIdCarrierObjIsFG`	5
Total	7

FGModuleCat

Definitions

Name	Category	Theorems
`forget₂CreatesLimit` 📖	CompOp	—
`instCreatesLimitsOfShapeModuleCatForget₂LinearMapIdCarrierObjIsFG` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instFiniteCarrierLimitModuleCatCompForget₂LinearMapIdObjIsFG` 📖	mathematical	—	`Module.Finite` `ModuleCat.carrier` `CategoryTheory.Limits.limit` `ModuleCat` `ModuleCat.moduleCategory` `CategoryTheory.Functor.comp` `FGModuleCat` `CategoryTheory.ObjectProperty.FullSubcategory.category` `ModuleCat.isFG` `CategoryTheory.forget₂` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `CategoryTheory.ObjectProperty.FullSubcategory.obj` `AddCommGroup.toAddCommMonoid` `ModuleCat.isAddCommGroup` `ModuleCat.isModule` `LinearMap.instFunLike` `CategoryTheory.FullSubcategory.concreteCategory` `ModuleCat.instConcreteCategoryLinearMapIdCarrier` `CategoryTheory.FullSubcategory.hasForget₂` `ModuleCat.hasLimit` `small_subtype` `small_Pi` `CategoryTheory.Functor.obj` `CategoryTheory.types` `CategoryTheory.forget` `UnivLE.small` `univLE_of_max` `UnivLE.self` `Set` `Set.instMembership` `CategoryTheory.Functor.sections`	—	`Module.Finite.of_injective` `ModuleCat.hasLimit` `small_subtype` `small_Pi` `UnivLE.small` `univLE_of_max` `UnivLE.self` `CategoryTheory.Limits.hasLimitOfHasLimitsOfShape` `CategoryTheory.Limits.hasProductsOfShape_of_hasProducts` `CategoryTheory.Limits.hasLimitsOfShapeOfHasLimits` `CategoryTheory.Limits.hasSmallestLimitsOfHasLimits` `ModuleCat.hasLimits` `isNoetherian_of_isNoetherianRing_of_finite` `instFiniteCarrierPiObjModuleCatOfFinite` `Finite.of_fintype` `instFiniteCarrier` `ModuleCat.mono_iff_injective` `CategoryTheory.Limits.limitSubobjectProduct_mono`
`instFiniteCarrierPiObjModuleCatOfFinite` 📖	mathematical	`Module.Finite` `ModuleCat.carrier` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `ModuleCat.isAddCommGroup` `ModuleCat.isModule`	`CategoryTheory.Limits.piObj` `ModuleCat` `ModuleCat.moduleCategory` `ModuleCat.hasLimit` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Discrete.functor` `small_subtype` `small_Pi` `CategoryTheory.Functor.obj` `CategoryTheory.types` `CategoryTheory.Functor.comp` `CategoryTheory.forget` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `LinearMap.instFunLike` `ModuleCat.instConcreteCategoryLinearMapIdCarrier` `CategoryTheory.instSmallDiscrete` `UnivLE.small` `univLE_of_max` `UnivLE.self` `Set` `Set.instMembership` `CategoryTheory.Functor.sections`	—	`ModuleCat.hasLimit` `small_subtype` `small_Pi` `CategoryTheory.instSmallDiscrete` `UnivLE.small` `univLE_of_max` `UnivLE.self` `Module.Finite.equiv_iff` `Module.Finite.pi`
`instHasFiniteLimits` 📖	mathematical	—	`CategoryTheory.Limits.HasFiniteLimits` `FGModuleCat` `CategoryTheory.ObjectProperty.FullSubcategory.category` `ModuleCat` `ModuleCat.moduleCategory` `ModuleCat.isFG`	—	`instHasLimitsOfShapeOfFinCategory`
`instHasLimitsOfShapeOfFinCategory` 📖	mathematical	—	`CategoryTheory.Limits.HasLimitsOfShape` `FGModuleCat` `CategoryTheory.ObjectProperty.FullSubcategory.category` `ModuleCat` `ModuleCat.moduleCategory` `ModuleCat.isFG`	—	`CategoryTheory.hasLimitsOfShape_of_hasLimitsOfShape_createsLimitsOfShape` `CategoryTheory.Limits.hasLimitsOfShape_of_hasFiniteLimits` `CategoryTheory.Limits.hasFiniteLimits_of_hasLimits` `ModuleCat.hasLimits`
`instPreservesFiniteLimitsModuleCatForget₂LinearMapIdCarrierObjIsFG` 📖	mathematical	—	`CategoryTheory.Limits.PreservesFiniteLimits` `FGModuleCat` `CategoryTheory.ObjectProperty.FullSubcategory.category` `ModuleCat` `ModuleCat.moduleCategory` `ModuleCat.isFG` `CategoryTheory.forget₂` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `ModuleCat.carrier` `CategoryTheory.ObjectProperty.FullSubcategory.obj` `AddCommGroup.toAddCommMonoid` `ModuleCat.isAddCommGroup` `ModuleCat.isModule` `LinearMap.instFunLike` `CategoryTheory.FullSubcategory.concreteCategory` `ModuleCat.instConcreteCategoryLinearMapIdCarrier` `CategoryTheory.FullSubcategory.hasForget₂`	—	`CategoryTheory.preservesLimitOfShape_of_createsLimitsOfShape_and_hasLimitsOfShape` `CategoryTheory.Limits.hasLimitsOfShape_of_hasFiniteLimits` `CategoryTheory.Limits.hasFiniteLimits_of_hasLimits` `ModuleCat.hasLimits`

---

← Back to Index