(Co)limits of functors out of SingleObj M

We characterise (co)limits of shape SingleObj M. Currently only in the category of types.

Main results

• SingleObj.Types.limitEquivFixedPoints: The limit of J : SingleObj G ⥤ Type u is the fixed points of J.obj (SingleObj.star G) under the induced action.

• SingleObj.Types.colimitEquivQuotient: The colimit of J : SingleObj G ⥤ Type u is the quotient of J.obj (SingleObj.star G) by the induced action.

instance CategoryTheory.Limits.SingleObj.instMulActionObjSingleObjStar {M : Type v} [Monoid M] (J : Functor (SingleObj M) (Type u)) : MulAction M (J.obj (SingleObj.star M))

The induced G-action on the target of J : SingleObj G ⥤ Type u.

Equations

• CategoryTheory.Limits.SingleObj.instMulActionObjSingleObjStar J = { smul := fun (g : M) (x : J.obj (CategoryTheory.SingleObj.star M)) => J.map g x, one_smul := ⋯, mul_smul := ⋯ }

def CategoryTheory.Limits.SingleObj.Types.sections.equivFixedPoints {M : Type v} [Monoid M] (J : Functor (SingleObj M) (Type u)) : ↑J.sections ≃ ↑(MulAction.fixedPoints M (J.obj (SingleObj.star M)))

The equivalence between sections of J : SingleObj M ⥤ Type u and fixed points of the induced action on J.obj (SingleObj.star M).

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Limits.SingleObj.Types.sections.equivFixedPoints_symm_apply_coe {M : Type v} [Monoid M] (J : Functor (SingleObj M) (Type u)) (p : ↑(MulAction.fixedPoints M (J.obj (SingleObj.star M)))) (x✝ : SingleObj M) : ↑((equivFixedPoints J).symm p) x✝ = ↑p

@[simp]

theorem CategoryTheory.Limits.SingleObj.Types.sections.equivFixedPoints_apply_coe {M : Type v} [Monoid M] (J : Functor (SingleObj M) (Type u)) (s : ↑J.sections) : ↑((equivFixedPoints J) s) = ↑s (SingleObj.star M)

noncomputable def CategoryTheory.Limits.SingleObj.Types.limitEquivFixedPoints {M : Type v} [Monoid M] (J : Functor (SingleObj M) (Type u)) : limit J ≃ ↑(MulAction.fixedPoints M (J.obj (SingleObj.star M)))

The limit of J : SingleObj M ⥤ Type u is equivalent to the fixed points of the induced action on J.obj (SingleObj.star M).

Equations

• CategoryTheory.Limits.SingleObj.Types.limitEquivFixedPoints J = (CategoryTheory.Limits.Types.limitEquivSections J).trans (CategoryTheory.Limits.SingleObj.Types.sections.equivFixedPoints J)

@[simp]

theorem CategoryTheory.Limits.SingleObj.Types.limitEquivFixedPoints_symm_apply {M : Type v} [Monoid M] (J : Functor (SingleObj M) (Type u)) (a✝ : ↑(MulAction.fixedPoints M (J.obj (SingleObj.star M)))) : (limitEquivFixedPoints J).symm a✝ = (Types.limitEquivSections J).symm ((sections.equivFixedPoints J).symm a✝)

@[simp]

theorem CategoryTheory.Limits.SingleObj.Types.limitEquivFixedPoints_apply_coe {M : Type v} [Monoid M] (J : Functor (SingleObj M) (Type u)) (a✝ : limit J) : ↑((limitEquivFixedPoints J) a✝) = limit.π J (SingleObj.star M) a✝

theorem CategoryTheory.Limits.SingleObj.colimitTypeRel_iff_orbitRel {G : Type v} [Group G] (J : Functor (SingleObj G) (Type u)) (x y : J.obj (SingleObj.star G)) : J.ColimitTypeRel ⟨SingleObj.star G, x⟩ ⟨SingleObj.star G, y⟩ ↔ (MulAction.orbitRel G (J.obj (SingleObj.star G))) x y

The relation used to construct colimits in types for J : SingleObj G ⥤ Type u is equivalent to the MulAction.orbitRel equivalence relation on J.obj (SingleObj.star G).

@[deprecated CategoryTheory.Limits.SingleObj.colimitTypeRel_iff_orbitRel (since := "2025-06-22")]

theorem CategoryTheory.Limits.SingleObj.Types.Quot.Rel.iff_orbitRel {G : Type v} [Group G] (J : Functor (SingleObj G) (Type u)) (x y : J.obj (SingleObj.star G)) : J.ColimitTypeRel ⟨SingleObj.star G, x⟩ ⟨SingleObj.star G, y⟩ ↔ (MulAction.orbitRel G (J.obj (SingleObj.star G))) x y

Alias of CategoryTheory.Limits.SingleObj.colimitTypeRel_iff_orbitRel.

---

The relation used to construct colimits in types for J : SingleObj G ⥤ Type u is equivalent to the MulAction.orbitRel equivalence relation on J.obj (SingleObj.star G).

def CategoryTheory.Limits.SingleObj.colimitTypeRelEquivOrbitRelQuotient {G : Type v} [Group G] (J : Functor (SingleObj G) (Type u)) : J.ColimitType ≃ MulAction.orbitRel.Quotient G (J.obj (SingleObj.star G))

The explicit quotient construction of the colimit of J : SingleObj G ⥤ Type u is equivalent to the quotient of J.obj (SingleObj.star G) by the induced action.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Limits.SingleObj.colimitTypeRelEquivOrbitRelQuotient_symm_apply {G : Type v} [Group G] (J : Functor (SingleObj G) (Type u)) (a : Quot ⇑(MulAction.orbitRel G (J.obj (SingleObj.star G)))) : (colimitTypeRelEquivOrbitRelQuotient J).symm a = Quot.lift (fun (x : J.obj (SingleObj.star G)) => Quot.mk J.ColimitTypeRel ⟨SingleObj.star G, x⟩) ⋯ a

@[simp]

theorem CategoryTheory.Limits.SingleObj.colimitTypeRelEquivOrbitRelQuotient_apply {G : Type v} [Group G] (J : Functor (SingleObj G) (Type u)) (a : Quot J.ColimitTypeRel) : (colimitTypeRelEquivOrbitRelQuotient J) a = Quot.lift (fun (p : (j : SingleObj G) × J.obj j) => ⟦p.snd⟧) ⋯ a

@[deprecated CategoryTheory.Limits.SingleObj.colimitTypeRelEquivOrbitRelQuotient (since := "2025-06-22")]

def CategoryTheory.Limits.SingleObj.Types.Quot.equivOrbitRelQuotient {G : Type v} [Group G] (J : Functor (SingleObj G) (Type u)) : J.ColimitType ≃ MulAction.orbitRel.Quotient G (J.obj (SingleObj.star G))

Alias of CategoryTheory.Limits.SingleObj.colimitTypeRelEquivOrbitRelQuotient.

---

The explicit quotient construction of the colimit of J : SingleObj G ⥤ Type u is equivalent to the quotient of J.obj (SingleObj.star G) by the induced action.

Equations

• @CategoryTheory.Limits.SingleObj.Types.Quot.equivOrbitRelQuotient = @CategoryTheory.Limits.SingleObj.colimitTypeRelEquivOrbitRelQuotient

noncomputable def CategoryTheory.Limits.SingleObj.Types.colimitEquivQuotient {G : Type v} [Group G] (J : Functor (SingleObj G) (Type u)) : colimit J ≃ MulAction.orbitRel.Quotient G (J.obj (SingleObj.star G))

The colimit of J : SingleObj G ⥤ Type u is equivalent to the quotient of J.obj (SingleObj.star G) by the induced action.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Limits.SingleObj.Types.colimitEquivQuotient_apply {G : Type v} [Group G] (J : Functor (SingleObj G) (Type u)) (a✝ : colimit J) : (colimitEquivQuotient J) a✝ = Quot.lift (fun (p : (j : SingleObj G) × J.obj j) => ⟦p.snd⟧) ⋯ ((Types.colimitEquivColimitType J) a✝)

@[simp]

theorem CategoryTheory.Limits.SingleObj.Types.colimitEquivQuotient_symm_apply {G : Type v} [Group G] (J : Functor (SingleObj G) (Type u)) (a✝ : MulAction.orbitRel.Quotient G (J.obj (SingleObj.star G))) : (colimitEquivQuotient J).symm a✝ = (Types.colimitEquivColimitType J).symm (Quot.lift (fun (x : J.obj (SingleObj.star G)) => Quot.mk J.ColimitTypeRel ⟨SingleObj.star G, x⟩) ⋯ a✝)