GrpLimits

📁 Source: Mathlib/CategoryTheory/Monoidal/Cartesian/GrpLimits.lean

Statistics

Metric	Count
Definitions limitAux, instCreatesLimitsOfShapeGrpForget, instCreatesLimitsOfShapeGrpMonForget₂Mon	3
Theorems instHasLimitsOfShapeGrp, instPreservesLimitsOfShapeMonFunctorOppositeMonCatShrinkYonedaMon	2
Total	5

CategoryTheory

Definitions

Name	Category	Theorems
instCreatesLimitsOfShapeGrpForget 📖	CompOp	—
instCreatesLimitsOfShapeGrpMonForget₂Mon 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instHasLimitsOfShapeGrp 📖	mathematical	—	Limits.HasLimitsOfShape Grp Grp.instCategory	—	hasLimitsOfShape_of_hasLimitsOfShape_createsLimitsOfShape
instPreservesLimitsOfShapeMonFunctorOppositeMonCatShrinkYonedaMon 📖	mathematical	—	Limits.PreservesLimitsOfShape Mon SemiCartesianMonoidalCategory.toMonoidalCategory CartesianMonoidalCategory.toSemiCartesianMonoidalCategory Mon.instCategory Functor Opposite Category.opposite MonCat MonCat.instCategory Functor.category shrinkYonedaMon locallySmall_of_univLE univLE_of_max UnivLE.self	—	locallySmall_of_univLE univLE_of_max UnivLE.self Limits.comp_preservesLimitsOfShape Mon.instPreservesLimitsOfShapeForgetOfHasLimitsOfShape Limits.PreservesLimitsOfSize.preservesLimitsOfShape instPreservesLimitsOfSizeFunctorOppositeTypeShrinkYoneda Limits.preservesLimitsOfShape_of_reflects_of_preserves instReflectsLimitsOfShapeFunctorObjWhiskeringRightOfHasLimitsOfShape Limits.Types.hasLimitsOfShape UnivLE.small Limits.reflectsLimitsOfShape_of_reflectsLimits reflectsLimitsOfCreatesLimits

CategoryTheory.Grp

Definitions

Name	Category	Theorems
limitAux 📖	CompOp	—

---

← Back to Index