Limits

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

Statistics

Metric	Count
Definitions createsLimit, addCommGroupObj, forget_createsLimit, forget_createsLimitsOfShape, forget_createsLimitsOfSize, forget₂AddCommMon_preservesLimitsAux, kernelIsoKer, kernelIsoKerOver, limitAddCommGroup, limitCone, limitConeIsLimit, createsLimit, addGroupObj, forget_createsLimit, forget_createsLimitsOfShape, forget_createsLimitsOfSize, limitAddGroup, limitCone, limitConeIsLimit, sectionsAddGroup, sectionsAddSubgroup, sectionsπAddMonoidHom, createsLimit, commGroupObj, forget_createsLimit, forget_createsLimitsOfShape, forget_createsLimitsOfSize, forget₂CommMon_preservesLimitsAux, limitCommGroup, limitCone, limitConeIsLimit, createsLimit, forget_createsLimit, forget_createsLimitsOfShape, forget_createsLimitsOfSize, groupObj, limitCone, limitConeIsLimit, limitGroup, sectionsGroup, sectionsSubgroup, sectionsπMonoidHom	42
Theorems forget_preservesLimits, forget_preservesLimitsOfShape, forget_preservesLimitsOfSize, forget₂AddCommMon_preservesLimitsOfShape, forget₂AddCommMon_preservesLimitsOfSize, forget₂AddGroup_preservesLimit, forget₂AddGroup_preservesLimits, forget₂AddGroup_preservesLimitsOfShape, forget₂AddGroup_preservesLimitsOfSize, hasLimit, hasLimit_iff_small_sections, hasLimits, hasLimitsOfShape, hasLimitsOfSize, instReflectsIsomorphismsAddGrpCatForget₂AddMonoidHomCarrierCarrier, kernelIsoKer_hom_comp_subtype, kernelIsoKer_inv_comp_ι, forget_preservesLimits, forget_preservesLimitsOfShape, forget_preservesLimitsOfSize, forget₂AddMonPreservesLimitsOfSize, forget₂Mon_preservesLimits, hasLimit, hasLimit_iff_small_sections, hasLimits, hasLimitsOfShape, hasLimitsOfSize, instSmallElemForallObjCompMonCatForget₂AddMonoidHomCarrierCarrierForgetSections, forget_preservesLimits, forget_preservesLimitsOfShape, forget_preservesLimitsOfSize, forget₂CommMon_preservesLimitsOfShape, forget₂CommMon_preservesLimitsOfSize, forget₂Group_preservesLimit, forget₂Group_preservesLimits, forget₂Group_preservesLimitsOfShape, forget₂Group_preservesLimitsOfSize, hasLimit, hasLimit_iff_small_sections, hasLimits, hasLimitsOfShape, hasLimitsOfSize, instReflectsIsomorphismsGrpCatForget₂MonoidHomCarrierCarrier, forget_preservesLimits, forget_preservesLimitsOfShape, forget_preservesLimitsOfSize, forget₂Mon_preservesLimits, forget₂Mon_preservesLimitsOfSize, hasLimit, hasLimit_iff_small_sections, hasLimits, hasLimitsOfShape, hasLimitsOfSize, instSmallElemForallObjCompMonCatForget₂MonoidHomCarrierCarrierForgetSections	54
Total	96

AddCommGrpCat

Definitions

Name	Category	Theorems
addCommGroupObj 📖	CompOp	—
forget_createsLimit 📖	CompOp	—
forget_createsLimitsOfShape 📖	CompOp	—
forget_createsLimitsOfSize 📖	CompOp	—
forget₂AddCommMon_preservesLimitsAux 📖	CompOp	—
kernelIsoKer 📖	CompOp	2 math math: kernelIsoKer_inv_comp_ι, kernelIsoKer_hom_comp_subtype
kernelIsoKerOver 📖	CompOp	—
limitAddCommGroup 📖	CompOp	—
limitCone 📖	CompOp	—
limitConeIsLimit 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
forget_preservesLimits 📖	mathematical	—	CategoryTheory.Limits.PreservesLimits AddCommGrpCat instCategory CategoryTheory.types CategoryTheory.forget AddMonoidHom carrier AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup str AddMonoidHom.instFunLike instConcreteCategoryAddMonoidHomCarrier	—	forget_preservesLimitsOfSize
forget_preservesLimitsOfShape 📖	mathematical	—	CategoryTheory.Limits.PreservesLimitsOfShape AddCommGrpCat instCategory CategoryTheory.types CategoryTheory.forget AddMonoidHom carrier AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup str AddMonoidHom.instFunLike instConcreteCategoryAddMonoidHomCarrier	—	CategoryTheory.Limits.preservesLimit_of_preserves_limit_cone small_subtype small_Pi UnivLE.small UnivLE.self
forget_preservesLimitsOfSize 📖	mathematical	—	CategoryTheory.Limits.PreservesLimitsOfSize AddCommGrpCat instCategory CategoryTheory.types CategoryTheory.forget AddMonoidHom carrier AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup str AddMonoidHom.instFunLike instConcreteCategoryAddMonoidHomCarrier	—	CategoryTheory.Functor.corepresentable_preservesLimits forget_isCorepresentable
forget₂AddCommMon_preservesLimitsOfShape 📖	mathematical	—	CategoryTheory.Limits.PreservesLimitsOfShape AddCommGrpCat instCategory AddCommMonCat AddCommMonCat.instCategory CategoryTheory.forget₂ AddMonoidHom carrier AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup str AddMonoidHom.instFunLike instConcreteCategoryAddMonoidHomCarrier AddCommMonCat.carrier AddCommMonoid.toAddMonoid AddCommMonCat.str AddCommMonCat.instConcreteCategoryAddMonoidHomCarrier hasForgetToAddCommMonCat	—	CategoryTheory.Limits.preservesLimit_of_preserves_limit_cone small_subtype small_Pi UnivLE.small UnivLE.self
forget₂AddCommMon_preservesLimitsOfSize 📖	mathematical	—	CategoryTheory.Limits.PreservesLimitsOfSize AddCommGrpCat instCategory AddCommMonCat AddCommMonCat.instCategory CategoryTheory.forget₂ AddMonoidHom carrier AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup str AddMonoidHom.instFunLike instConcreteCategoryAddMonoidHomCarrier AddCommMonCat.carrier AddCommMonoid.toAddMonoid AddCommMonCat.str AddCommMonCat.instConcreteCategoryAddMonoidHomCarrier hasForgetToAddCommMonCat	—	CategoryTheory.Limits.PreservesLimitsOfShape.preservesLimit forget₂AddCommMon_preservesLimitsOfShape UnivLE.small
forget₂AddGroup_preservesLimit 📖	mathematical	—	CategoryTheory.Limits.PreservesLimit AddCommGrpCat instCategory AddGrpCat AddGrpCat.instCategory CategoryTheory.forget₂ AddMonoidHom carrier AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup str AddMonoidHom.instFunLike instConcreteCategoryAddMonoidHomCarrier AddGrpCat.carrier AddGrpCat.str AddGrpCat.instConcreteCategoryAddMonoidHomCarrier hasForgetToAddGroup	—	AddGrpCat.hasLimit_iff_small_sections hasLimit_iff_small_sections CategoryTheory.preservesLimit_of_createsLimit_and_hasLimit
forget₂AddGroup_preservesLimits 📖	mathematical	—	CategoryTheory.Limits.PreservesLimits AddCommGrpCat instCategory AddGrpCat AddGrpCat.instCategory CategoryTheory.forget₂ AddMonoidHom carrier AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup str AddMonoidHom.instFunLike instConcreteCategoryAddMonoidHomCarrier AddGrpCat.carrier AddGrpCat.str AddGrpCat.instConcreteCategoryAddMonoidHomCarrier hasForgetToAddGroup	—	forget₂AddGroup_preservesLimitsOfSize
forget₂AddGroup_preservesLimitsOfShape 📖	mathematical	—	CategoryTheory.Limits.PreservesLimitsOfShape AddCommGrpCat instCategory AddGrpCat AddGrpCat.instCategory CategoryTheory.forget₂ AddMonoidHom carrier AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup str AddMonoidHom.instFunLike instConcreteCategoryAddMonoidHomCarrier AddGrpCat.carrier AddGrpCat.str AddGrpCat.instConcreteCategoryAddMonoidHomCarrier hasForgetToAddGroup	—	forget₂AddGroup_preservesLimit
forget₂AddGroup_preservesLimitsOfSize 📖	mathematical	—	CategoryTheory.Limits.PreservesLimitsOfSize AddCommGrpCat instCategory AddGrpCat AddGrpCat.instCategory CategoryTheory.forget₂ AddMonoidHom carrier AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup str AddMonoidHom.instFunLike instConcreteCategoryAddMonoidHomCarrier AddGrpCat.carrier AddGrpCat.str AddGrpCat.instConcreteCategoryAddMonoidHomCarrier hasForgetToAddGroup	—	forget₂AddGroup_preservesLimitsOfShape
hasLimit 📖	mathematical	—	CategoryTheory.Limits.HasLimit AddCommGrpCat instCategory	—	—
hasLimit_iff_small_sections 📖	mathematical	—	CategoryTheory.Limits.HasLimit AddCommGrpCat instCategory Small Set.Elem CategoryTheory.Functor.sections CategoryTheory.Functor.comp CategoryTheory.types CategoryTheory.forget AddMonoidHom carrier AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup str AddMonoidHom.instFunLike instConcreteCategoryAddMonoidHomCarrier	—	CategoryTheory.Limits.Concrete.small_sections_of_hasLimit forget_isCorepresentable hasLimit
hasLimits 📖	mathematical	—	CategoryTheory.Limits.HasLimits AddCommGrpCat instCategory	—	hasLimitsOfSize UnivLE.self
hasLimitsOfShape 📖	mathematical	—	CategoryTheory.Limits.HasLimitsOfShape AddCommGrpCat instCategory	—	hasLimit small_subtype small_Pi UnivLE.small UnivLE.self
hasLimitsOfSize 📖	mathematical	—	CategoryTheory.Limits.HasLimitsOfSize AddCommGrpCat instCategory	—	hasLimit small_subtype small_Pi UnivLE.small UnivLE.self
instReflectsIsomorphismsAddGrpCatForget₂AddMonoidHomCarrierCarrier 📖	mathematical	—	CategoryTheory.Functor.ReflectsIsomorphisms AddCommGrpCat instCategory AddGrpCat AddGrpCat.instCategory CategoryTheory.forget₂ AddMonoidHom carrier AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup str AddMonoidHom.instFunLike instConcreteCategoryAddMonoidHomCarrier AddGrpCat.carrier AddGrpCat.str AddGrpCat.instConcreteCategoryAddMonoidHomCarrier hasForgetToAddGroup	—	CategoryTheory.reflectsIsomorphisms_forget₂ forget_reflects_isos
kernelIsoKer_hom_comp_subtype 📖	mathematical	—	CategoryTheory.CategoryStruct.comp AddCommGrpCat CategoryTheory.Category.toCategoryStruct instCategory CategoryTheory.Limits.kernel CategoryTheory.Preadditive.preadditiveHasZeroMorphisms instPreadditive hasLimit CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory CategoryTheory.Limits.parallelPair Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero small_subtype small_Pi CategoryTheory.Functor.obj CategoryTheory.types CategoryTheory.Functor.comp CategoryTheory.forget AddMonoidHom carrier AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup str AddMonoidHom.instFunLike instConcreteCategoryAddMonoidHomCarrier UnivLE.small univLE_of_max UnivLE.self Set Set.instMembership CategoryTheory.Functor.sections of AddSubgroup SetLike.instMembership AddSubgroup.instSetLike AddMonoidHom.ker Hom.hom AddSubgroup.toAddCommGroup CategoryTheory.Iso.hom kernelIsoKer ofHom AddSubgroup.subtype CategoryTheory.Limits.kernel.ι	—	hom_ext hasLimit small_subtype small_Pi UnivLE.small univLE_of_max UnivLE.self AddMonoidHom.ext
kernelIsoKer_inv_comp_ι 📖	mathematical	—	CategoryTheory.CategoryStruct.comp AddCommGrpCat CategoryTheory.Category.toCategoryStruct instCategory of carrier AddSubgroup AddCommGroup.toAddGroup str SetLike.instMembership AddSubgroup.instSetLike AddMonoidHom.ker AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid Hom.hom AddSubgroup.toAddCommGroup CategoryTheory.Limits.kernel CategoryTheory.Preadditive.preadditiveHasZeroMorphisms instPreadditive hasLimit CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory CategoryTheory.Limits.parallelPair Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero small_subtype small_Pi CategoryTheory.Functor.obj CategoryTheory.types CategoryTheory.Functor.comp CategoryTheory.forget AddMonoidHom AddZeroClass.toAddZero AddMonoidHom.instFunLike instConcreteCategoryAddMonoidHomCarrier UnivLE.small univLE_of_max UnivLE.self Set Set.instMembership CategoryTheory.Functor.sections CategoryTheory.Iso.inv kernelIsoKer CategoryTheory.Limits.kernel.ι ofHom AddSubgroup.subtype	—	hasLimit small_subtype small_Pi UnivLE.small univLE_of_max UnivLE.self CategoryTheory.Limits.kernel.lift_ι

AddCommGrpCat.Forget₂

Definitions

Name	Category	Theorems
createsLimit 📖	CompOp	—

AddGrpCat

Definitions

Name	Category	Theorems
addGroupObj 📖	CompOp	—
forget_createsLimit 📖	CompOp	—
forget_createsLimitsOfShape 📖	CompOp	—
forget_createsLimitsOfSize 📖	CompOp	—
limitAddGroup 📖	CompOp	—
limitCone 📖	CompOp	—
limitConeIsLimit 📖	CompOp	—
sectionsAddGroup 📖	CompOp	—
sectionsAddSubgroup 📖	CompOp	—
sectionsπAddMonoidHom 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
forget_preservesLimits 📖	mathematical	—	CategoryTheory.Limits.PreservesLimits AddGrpCat instCategory CategoryTheory.types CategoryTheory.forget AddMonoidHom carrier AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid str AddMonoidHom.instFunLike instConcreteCategoryAddMonoidHomCarrier	—	forget_preservesLimitsOfSize
forget_preservesLimitsOfShape 📖	mathematical	—	CategoryTheory.Limits.PreservesLimitsOfShape AddGrpCat instCategory CategoryTheory.types CategoryTheory.forget AddMonoidHom carrier AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid str AddMonoidHom.instFunLike instConcreteCategoryAddMonoidHomCarrier	—	CategoryTheory.Limits.preservesLimit_of_preserves_limit_cone small_subtype small_Pi UnivLE.small UnivLE.self
forget_preservesLimitsOfSize 📖	mathematical	—	CategoryTheory.Limits.PreservesLimitsOfSize AddGrpCat instCategory CategoryTheory.types CategoryTheory.forget AddMonoidHom carrier AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid str AddMonoidHom.instFunLike instConcreteCategoryAddMonoidHomCarrier	—	CategoryTheory.Functor.corepresentable_preservesLimits forget_isCorepresentable
forget₂AddMonPreservesLimitsOfSize 📖	mathematical	—	CategoryTheory.Limits.PreservesLimitsOfSize AddGrpCat instCategory AddMonCat AddMonCat.instCategory CategoryTheory.forget₂ AddMonoidHom carrier AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid str AddMonoidHom.instFunLike instConcreteCategoryAddMonoidHomCarrier AddMonCat.carrier AddMonCat.str AddMonCat.instConcreteCategoryAddMonoidHomCarrier hasForgetToAddMonCat	—	CategoryTheory.preservesLimit_of_createsLimit_and_hasLimit AddMonCat.HasLimits.hasLimit instSmallElemForallObjCompMonCatForget₂AddMonoidHomCarrierCarrierForgetSections small_subtype small_Pi UnivLE.small UnivLE.self
forget₂Mon_preservesLimits 📖	mathematical	—	CategoryTheory.Limits.PreservesLimits AddGrpCat instCategory AddMonCat AddMonCat.instCategory CategoryTheory.forget₂ AddMonoidHom carrier AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid str AddMonoidHom.instFunLike instConcreteCategoryAddMonoidHomCarrier AddMonCat.carrier AddMonCat.str AddMonCat.instConcreteCategoryAddMonoidHomCarrier hasForgetToAddMonCat	—	forget₂AddMonPreservesLimitsOfSize UnivLE.self
hasLimit 📖	mathematical	—	CategoryTheory.Limits.HasLimit AddGrpCat instCategory	—	—
hasLimit_iff_small_sections 📖	mathematical	—	CategoryTheory.Limits.HasLimit AddGrpCat instCategory Small Set.Elem CategoryTheory.Functor.sections CategoryTheory.Functor.comp CategoryTheory.types CategoryTheory.forget AddMonoidHom carrier AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid str AddMonoidHom.instFunLike instConcreteCategoryAddMonoidHomCarrier	—	CategoryTheory.Limits.Concrete.small_sections_of_hasLimit forget_isCorepresentable hasLimit
hasLimits 📖	mathematical	—	CategoryTheory.Limits.HasLimits AddGrpCat instCategory	—	hasLimitsOfSize UnivLE.self
hasLimitsOfShape 📖	mathematical	—	CategoryTheory.Limits.HasLimitsOfShape AddGrpCat instCategory	—	hasLimit small_subtype small_Pi UnivLE.small UnivLE.self
hasLimitsOfSize 📖	mathematical	—	CategoryTheory.Limits.HasLimitsOfSize AddGrpCat instCategory	—	hasLimit small_subtype small_Pi UnivLE.small UnivLE.self
instSmallElemForallObjCompMonCatForget₂AddMonoidHomCarrierCarrierForgetSections 📖	mathematical	—	Small Set.Elem CategoryTheory.Functor.sections CategoryTheory.Functor.comp AddMonCat AddMonCat.instCategory CategoryTheory.types AddGrpCat instCategory CategoryTheory.forget₂ AddMonoidHom carrier AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid str AddMonoidHom.instFunLike instConcreteCategoryAddMonoidHomCarrier AddMonCat.carrier AddMonCat.str AddMonCat.instConcreteCategoryAddMonoidHomCarrier hasForgetToAddMonCat CategoryTheory.forget	—	—

AddGrpCat.Forget₂

Definitions

Name	Category	Theorems
createsLimit 📖	CompOp	—

CommGrpCat

Definitions

Name	Category	Theorems
commGroupObj 📖	CompOp	—
forget_createsLimit 📖	CompOp	—
forget_createsLimitsOfShape 📖	CompOp	—
forget_createsLimitsOfSize 📖	CompOp	—
forget₂CommMon_preservesLimitsAux 📖	CompOp	—
limitCommGroup 📖	CompOp	—
limitCone 📖	CompOp	—
limitConeIsLimit 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
forget_preservesLimits 📖	mathematical	—	CategoryTheory.Limits.PreservesLimits CommGrpCat instCategory CategoryTheory.types CategoryTheory.forget MonoidHom carrier MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup str MonoidHom.instFunLike instConcreteCategoryMonoidHomCarrier	—	forget_preservesLimitsOfSize
forget_preservesLimitsOfShape 📖	mathematical	—	CategoryTheory.Limits.PreservesLimitsOfShape CommGrpCat instCategory CategoryTheory.types CategoryTheory.forget MonoidHom carrier MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup str MonoidHom.instFunLike instConcreteCategoryMonoidHomCarrier	—	CategoryTheory.Limits.preservesLimit_of_preserves_limit_cone small_subtype small_Pi UnivLE.small UnivLE.self
forget_preservesLimitsOfSize 📖	mathematical	—	CategoryTheory.Limits.PreservesLimitsOfSize CommGrpCat instCategory CategoryTheory.types CategoryTheory.forget MonoidHom carrier MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup str MonoidHom.instFunLike instConcreteCategoryMonoidHomCarrier	—	CategoryTheory.Functor.corepresentable_preservesLimits forget_isCorepresentable
forget₂CommMon_preservesLimitsOfShape 📖	mathematical	—	CategoryTheory.Limits.PreservesLimitsOfShape CommGrpCat instCategory CommMonCat CommMonCat.instCategory CategoryTheory.forget₂ MonoidHom carrier MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup str MonoidHom.instFunLike instConcreteCategoryMonoidHomCarrier CommMonCat.carrier CommMonoid.toMonoid CommMonCat.str CommMonCat.instConcreteCategoryMonoidHomCarrier hasForgetToCommMonCat	—	CategoryTheory.Limits.preservesLimit_of_preserves_limit_cone small_subtype small_Pi UnivLE.small UnivLE.self
forget₂CommMon_preservesLimitsOfSize 📖	mathematical	—	CategoryTheory.Limits.PreservesLimitsOfSize CommGrpCat instCategory CommMonCat CommMonCat.instCategory CategoryTheory.forget₂ MonoidHom carrier MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup str MonoidHom.instFunLike instConcreteCategoryMonoidHomCarrier CommMonCat.carrier CommMonoid.toMonoid CommMonCat.str CommMonCat.instConcreteCategoryMonoidHomCarrier hasForgetToCommMonCat	—	CategoryTheory.Limits.PreservesLimitsOfShape.preservesLimit forget₂CommMon_preservesLimitsOfShape UnivLE.small
forget₂Group_preservesLimit 📖	mathematical	—	CategoryTheory.Limits.PreservesLimit CommGrpCat instCategory GrpCat GrpCat.instCategory CategoryTheory.forget₂ MonoidHom carrier MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup str MonoidHom.instFunLike instConcreteCategoryMonoidHomCarrier GrpCat.carrier GrpCat.str GrpCat.instConcreteCategoryMonoidHomCarrier hasForgetToGroup	—	GrpCat.hasLimit_iff_small_sections hasLimit_iff_small_sections CategoryTheory.preservesLimit_of_createsLimit_and_hasLimit
forget₂Group_preservesLimits 📖	mathematical	—	CategoryTheory.Limits.PreservesLimits CommGrpCat instCategory GrpCat GrpCat.instCategory CategoryTheory.forget₂ MonoidHom carrier MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup str MonoidHom.instFunLike instConcreteCategoryMonoidHomCarrier GrpCat.carrier GrpCat.str GrpCat.instConcreteCategoryMonoidHomCarrier hasForgetToGroup	—	forget₂Group_preservesLimitsOfSize
forget₂Group_preservesLimitsOfShape 📖	mathematical	—	CategoryTheory.Limits.PreservesLimitsOfShape CommGrpCat instCategory GrpCat GrpCat.instCategory CategoryTheory.forget₂ MonoidHom carrier MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup str MonoidHom.instFunLike instConcreteCategoryMonoidHomCarrier GrpCat.carrier GrpCat.str GrpCat.instConcreteCategoryMonoidHomCarrier hasForgetToGroup	—	forget₂Group_preservesLimit
forget₂Group_preservesLimitsOfSize 📖	mathematical	—	CategoryTheory.Limits.PreservesLimitsOfSize CommGrpCat instCategory GrpCat GrpCat.instCategory CategoryTheory.forget₂ MonoidHom carrier MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup str MonoidHom.instFunLike instConcreteCategoryMonoidHomCarrier GrpCat.carrier GrpCat.str GrpCat.instConcreteCategoryMonoidHomCarrier hasForgetToGroup	—	forget₂Group_preservesLimitsOfShape
hasLimit 📖	mathematical	—	CategoryTheory.Limits.HasLimit CommGrpCat instCategory	—	—
hasLimit_iff_small_sections 📖	mathematical	—	CategoryTheory.Limits.HasLimit CommGrpCat instCategory Small Set.Elem CategoryTheory.Functor.sections CategoryTheory.Functor.comp CategoryTheory.types CategoryTheory.forget MonoidHom carrier MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup str MonoidHom.instFunLike instConcreteCategoryMonoidHomCarrier	—	CategoryTheory.Limits.Concrete.small_sections_of_hasLimit forget_isCorepresentable hasLimit
hasLimits 📖	mathematical	—	CategoryTheory.Limits.HasLimits CommGrpCat instCategory	—	hasLimitsOfSize UnivLE.self
hasLimitsOfShape 📖	mathematical	—	CategoryTheory.Limits.HasLimitsOfShape CommGrpCat instCategory	—	hasLimit small_subtype small_Pi UnivLE.small UnivLE.self
hasLimitsOfSize 📖	mathematical	—	CategoryTheory.Limits.HasLimitsOfSize CommGrpCat instCategory	—	hasLimit small_subtype small_Pi UnivLE.small UnivLE.self
instReflectsIsomorphismsGrpCatForget₂MonoidHomCarrierCarrier 📖	mathematical	—	CategoryTheory.Functor.ReflectsIsomorphisms CommGrpCat instCategory GrpCat GrpCat.instCategory CategoryTheory.forget₂ MonoidHom carrier MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup str MonoidHom.instFunLike instConcreteCategoryMonoidHomCarrier GrpCat.carrier GrpCat.str GrpCat.instConcreteCategoryMonoidHomCarrier hasForgetToGroup	—	CategoryTheory.reflectsIsomorphisms_forget₂ forget_reflects_isos

CommGrpCat.Forget₂

Definitions

Name	Category	Theorems
createsLimit 📖	CompOp	—

GrpCat

Definitions

Name	Category	Theorems
forget_createsLimit 📖	CompOp	—
forget_createsLimitsOfShape 📖	CompOp	—
forget_createsLimitsOfSize 📖	CompOp	—
groupObj 📖	CompOp	—
limitCone 📖	CompOp	—
limitConeIsLimit 📖	CompOp	—
limitGroup 📖	CompOp	—
sectionsGroup 📖	CompOp	—
sectionsSubgroup 📖	CompOp	—
sectionsπMonoidHom 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
forget_preservesLimits 📖	mathematical	—	CategoryTheory.Limits.PreservesLimits GrpCat instCategory CategoryTheory.types CategoryTheory.forget MonoidHom carrier MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid str MonoidHom.instFunLike instConcreteCategoryMonoidHomCarrier	—	forget_preservesLimitsOfSize
forget_preservesLimitsOfShape 📖	mathematical	—	CategoryTheory.Limits.PreservesLimitsOfShape GrpCat instCategory CategoryTheory.types CategoryTheory.forget MonoidHom carrier MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid str MonoidHom.instFunLike instConcreteCategoryMonoidHomCarrier	—	CategoryTheory.Limits.preservesLimit_of_preserves_limit_cone small_subtype small_Pi UnivLE.small UnivLE.self
forget_preservesLimitsOfSize 📖	mathematical	—	CategoryTheory.Limits.PreservesLimitsOfSize GrpCat instCategory CategoryTheory.types CategoryTheory.forget MonoidHom carrier MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid str MonoidHom.instFunLike instConcreteCategoryMonoidHomCarrier	—	CategoryTheory.Functor.corepresentable_preservesLimits forget_isCorepresentable
forget₂Mon_preservesLimits 📖	mathematical	—	CategoryTheory.Limits.PreservesLimits GrpCat instCategory MonCat MonCat.instCategory CategoryTheory.forget₂ MonoidHom carrier MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid str MonoidHom.instFunLike instConcreteCategoryMonoidHomCarrier MonCat.carrier MonCat.str MonCat.instConcreteCategoryMonoidHomCarrier hasForgetToMonCat	—	forget₂Mon_preservesLimitsOfSize UnivLE.self
forget₂Mon_preservesLimitsOfSize 📖	mathematical	—	CategoryTheory.Limits.PreservesLimitsOfSize GrpCat instCategory MonCat MonCat.instCategory CategoryTheory.forget₂ MonoidHom carrier MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid str MonoidHom.instFunLike instConcreteCategoryMonoidHomCarrier MonCat.carrier MonCat.str MonCat.instConcreteCategoryMonoidHomCarrier hasForgetToMonCat	—	CategoryTheory.preservesLimit_of_createsLimit_and_hasLimit MonCat.HasLimits.hasLimit instSmallElemForallObjCompMonCatForget₂MonoidHomCarrierCarrierForgetSections small_subtype small_Pi UnivLE.small UnivLE.self
hasLimit 📖	mathematical	—	CategoryTheory.Limits.HasLimit GrpCat instCategory	—	—
hasLimit_iff_small_sections 📖	mathematical	—	CategoryTheory.Limits.HasLimit GrpCat instCategory Small Set.Elem CategoryTheory.Functor.sections CategoryTheory.Functor.comp CategoryTheory.types CategoryTheory.forget MonoidHom carrier MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid str MonoidHom.instFunLike instConcreteCategoryMonoidHomCarrier	—	CategoryTheory.Limits.Concrete.small_sections_of_hasLimit forget_isCorepresentable hasLimit
hasLimits 📖	mathematical	—	CategoryTheory.Limits.HasLimits GrpCat instCategory	—	hasLimitsOfSize UnivLE.self
hasLimitsOfShape 📖	mathematical	—	CategoryTheory.Limits.HasLimitsOfShape GrpCat instCategory	—	hasLimit small_subtype small_Pi UnivLE.small UnivLE.self
hasLimitsOfSize 📖	mathematical	—	CategoryTheory.Limits.HasLimitsOfSize GrpCat instCategory	—	hasLimit small_subtype small_Pi UnivLE.small UnivLE.self
instSmallElemForallObjCompMonCatForget₂MonoidHomCarrierCarrierForgetSections 📖	mathematical	—	Small Set.Elem CategoryTheory.Functor.sections CategoryTheory.Functor.comp MonCat MonCat.instCategory CategoryTheory.types GrpCat instCategory CategoryTheory.forget₂ MonoidHom carrier MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid str MonoidHom.instFunLike instConcreteCategoryMonoidHomCarrier MonCat.carrier MonCat.str MonCat.instConcreteCategoryMonoidHomCarrier hasForgetToMonCat CategoryTheory.forget	—	—

GrpCat.Forget₂

Definitions

Name	Category	Theorems
createsLimit 📖	CompOp	—

---

← Back to Index