SingleObj

📁 Source: Mathlib/CategoryTheory/Limits/Shapes/SingleObj.lean

Statistics

Metric	Count
Definitions colimitEquivQuotient, limitEquivFixedPoints, equivFixedPoints, colimitTypeRelEquivOrbitRelQuotient, instMulActionObjSingleObjStar	5
Theorems colimitEquivQuotient_apply, colimitEquivQuotient_symm_apply, limitEquivFixedPoints_apply_coe, limitEquivFixedPoints_symm_apply, equivFixedPoints_apply_coe, equivFixedPoints_symm_apply_coe, colimitTypeRelEquivOrbitRelQuotient_apply, colimitTypeRelEquivOrbitRelQuotient_symm_apply, colimitTypeRel_iff_orbitRel	9
Total	14

CategoryTheory.Limits.SingleObj

Definitions

Name	Category	Theorems
colimitTypeRelEquivOrbitRelQuotient 📖	CompOp	2 math math: colimitTypeRelEquivOrbitRelQuotient_apply, colimitTypeRelEquivOrbitRelQuotient_symm_apply
instMulActionObjSingleObjStar 📖	CompOp	9 math math: Types.sections.equivFixedPoints_apply_coe, Types.colimitEquivQuotient_symm_apply, Types.colimitEquivQuotient_apply, Types.limitEquivFixedPoints_symm_apply, colimitTypeRelEquivOrbitRelQuotient_apply, colimitTypeRel_iff_orbitRel, Types.limitEquivFixedPoints_apply_coe, colimitTypeRelEquivOrbitRelQuotient_symm_apply, Types.sections.equivFixedPoints_symm_apply_coe

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
colimitTypeRelEquivOrbitRelQuotient_apply 📖	mathematical	—	DFunLike.coe Equiv CategoryTheory.Functor.ColimitType CategoryTheory.SingleObj CategoryTheory.SingleObj.category DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.orbitRel.Quotient CategoryTheory.Functor.obj CategoryTheory.types CategoryTheory.SingleObj.star instMulActionObjSingleObjStar EquivLike.toFunLike Equiv.instEquivLike colimitTypeRelEquivOrbitRelQuotient CategoryTheory.Functor.ColimitTypeRel MulAction.orbitRel	—	—
colimitTypeRelEquivOrbitRelQuotient_symm_apply 📖	mathematical	—	DFunLike.coe Equiv MulAction.orbitRel.Quotient CategoryTheory.Functor.obj CategoryTheory.SingleObj CategoryTheory.SingleObj.category DivInvMonoid.toMonoid Group.toDivInvMonoid CategoryTheory.types CategoryTheory.SingleObj.star instMulActionObjSingleObjStar CategoryTheory.Functor.ColimitType EquivLike.toFunLike Equiv.instEquivLike Equiv.symm colimitTypeRelEquivOrbitRelQuotient MulAction.orbitRel CategoryTheory.Functor.ColimitTypeRel	—	—
colimitTypeRel_iff_orbitRel 📖	mathematical	—	CategoryTheory.Functor.ColimitTypeRel CategoryTheory.SingleObj CategoryTheory.SingleObj.category DivInvMonoid.toMonoid Group.toDivInvMonoid CategoryTheory.Functor.obj CategoryTheory.types CategoryTheory.SingleObj.star MulAction.orbitRel instMulActionObjSingleObjStar	—	Setoid.comm'

CategoryTheory.Limits.SingleObj.Types

Definitions

Name	Category	Theorems
colimitEquivQuotient 📖	CompOp	2 math math: colimitEquivQuotient_symm_apply, colimitEquivQuotient_apply
limitEquivFixedPoints 📖	CompOp	2 math math: limitEquivFixedPoints_symm_apply, limitEquivFixedPoints_apply_coe

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
colimitEquivQuotient_apply 📖	mathematical	—	DFunLike.coe Equiv CategoryTheory.Limits.colimit CategoryTheory.SingleObj CategoryTheory.SingleObj.category DivInvMonoid.toMonoid Group.toDivInvMonoid CategoryTheory.types CategoryTheory.Limits.Types.hasColimit UnivLE.small univLE_of_max UnivLE.self MulAction.orbitRel.Quotient CategoryTheory.Functor.obj CategoryTheory.SingleObj.star CategoryTheory.Limits.SingleObj.instMulActionObjSingleObjStar EquivLike.toFunLike Equiv.instEquivLike colimitEquivQuotient CategoryTheory.Functor.ColimitTypeRel MulAction.orbitRel CategoryTheory.Functor.ColimitType CategoryTheory.Limits.Types.colimitEquivColimitType	—	CategoryTheory.Limits.Types.hasColimit UnivLE.small univLE_of_max UnivLE.self
colimitEquivQuotient_symm_apply 📖	mathematical	—	DFunLike.coe Equiv MulAction.orbitRel.Quotient CategoryTheory.Functor.obj CategoryTheory.SingleObj CategoryTheory.SingleObj.category DivInvMonoid.toMonoid Group.toDivInvMonoid CategoryTheory.types CategoryTheory.SingleObj.star CategoryTheory.Limits.SingleObj.instMulActionObjSingleObjStar CategoryTheory.Limits.colimit CategoryTheory.Limits.Types.hasColimit UnivLE.small univLE_of_max UnivLE.self EquivLike.toFunLike Equiv.instEquivLike Equiv.symm colimitEquivQuotient CategoryTheory.Functor.ColimitType CategoryTheory.Limits.Types.colimitEquivColimitType MulAction.orbitRel CategoryTheory.Functor.ColimitTypeRel	—	CategoryTheory.Limits.Types.hasColimit UnivLE.small univLE_of_max UnivLE.self
limitEquivFixedPoints_apply_coe 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.SingleObj CategoryTheory.SingleObj.category CategoryTheory.types CategoryTheory.SingleObj.star Set Set.instMembership MulAction.fixedPoints CategoryTheory.Limits.SingleObj.instMulActionObjSingleObjStar DFunLike.coe Equiv CategoryTheory.Limits.limit CategoryTheory.Limits.Types.hasLimit UnivLE.small univLE_of_max UnivLE.self Set.Elem EquivLike.toFunLike Equiv.instEquivLike limitEquivFixedPoints CategoryTheory.Limits.limit.π	—	CategoryTheory.Limits.Types.hasLimit UnivLE.small univLE_of_max UnivLE.self
limitEquivFixedPoints_symm_apply 📖	mathematical	—	DFunLike.coe Equiv Set.Elem CategoryTheory.Functor.obj CategoryTheory.SingleObj CategoryTheory.SingleObj.category CategoryTheory.types CategoryTheory.SingleObj.star MulAction.fixedPoints CategoryTheory.Limits.SingleObj.instMulActionObjSingleObjStar CategoryTheory.Limits.limit CategoryTheory.Limits.Types.hasLimit UnivLE.small univLE_of_max UnivLE.self EquivLike.toFunLike Equiv.instEquivLike Equiv.symm limitEquivFixedPoints CategoryTheory.Functor.sections CategoryTheory.Limits.Types.limitEquivSections sections.equivFixedPoints	—	CategoryTheory.Limits.Types.hasLimit UnivLE.small univLE_of_max UnivLE.self

CategoryTheory.Limits.SingleObj.Types.sections

Definitions

Name	Category	Theorems
equivFixedPoints 📖	CompOp	3 math math: equivFixedPoints_apply_coe, CategoryTheory.Limits.SingleObj.Types.limitEquivFixedPoints_symm_apply, equivFixedPoints_symm_apply_coe

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
equivFixedPoints_apply_coe 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.SingleObj CategoryTheory.SingleObj.category CategoryTheory.types CategoryTheory.SingleObj.star Set Set.instMembership MulAction.fixedPoints CategoryTheory.Limits.SingleObj.instMulActionObjSingleObjStar DFunLike.coe Equiv Set.Elem CategoryTheory.Functor.sections EquivLike.toFunLike Equiv.instEquivLike equivFixedPoints	—	—
equivFixedPoints_symm_apply_coe 📖	mathematical	—	Set Set.instMembership CategoryTheory.Functor.sections CategoryTheory.SingleObj CategoryTheory.SingleObj.category DFunLike.coe Equiv Set.Elem CategoryTheory.Functor.obj CategoryTheory.types CategoryTheory.SingleObj.star MulAction.fixedPoints CategoryTheory.Limits.SingleObj.instMulActionObjSingleObjStar EquivLike.toFunLike Equiv.instEquivLike Equiv.symm equivFixedPoints	—	—

---

← Back to Index