(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_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.Types.Quot.Rel.iff_orbitRel {G : Type v} [Group G] (J : Functor (SingleObj G) (Type u)) (x y : J.obj (SingleObj.star G)) : Types.Quot.Rel J ⟨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.Types.Quot.equivOrbitRelQuotient {G : Type v} [Group G] (J : Functor (SingleObj G) (Type u)) : Types.Quot J ≃ 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.Types.Quot.equivOrbitRelQuotient_symm_apply {G : Type v} [Group G] (J : Functor (SingleObj G) (Type u)) (a : Quot ⇑(MulAction.orbitRel G (J.obj (SingleObj.star G)))) : (equivOrbitRelQuotient J).symm a = Quot.lift (fun (x : J.obj (SingleObj.star G)) => Quot.mk (Types.Quot.Rel J) ⟨SingleObj.star G, x⟩) ⋯ a

@[simp]

theorem CategoryTheory.Limits.SingleObj.Types.Quot.equivOrbitRelQuotient_apply {G : Type v} [Group G] (J : Functor (SingleObj G) (Type u)) (a : Quot (Types.Quot.Rel J)) : (equivOrbitRelQuotient J) a = Quot.lift (fun (p : (j : SingleObj G) × J.obj j) => ⟦p.snd⟧) ⋯ 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.

Equations

• CategoryTheory.Limits.SingleObj.Types.colimitEquivQuotient J = (CategoryTheory.Limits.Types.colimitEquivQuot J).trans (CategoryTheory.Limits.SingleObj.Types.Quot.equivOrbitRelQuotient J)

@[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.colimitEquivQuot 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.colimitEquivQuot J).symm (Quot.lift (fun (x : J.obj (SingleObj.star G)) => Quot.mk (Types.Quot.Rel J) ⟨SingleObj.star G, x⟩) ⋯ a✝)