(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.

@[implicit_reducible]

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.

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).

@[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).

@[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✝

@[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✝)

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).

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.

@[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

@[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

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.

@[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✝)

@[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✝)