(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.instMulActionObjSingleObjToQuiverToCategoryStructCategoryTypeToQuiverToCategoryStructTypesToPrefunctorStar {M : Type v} [Monoid M] (J : CategoryTheory.Functor (CategoryTheory.SingleObj M) (Type u)) : MulAction M (J.toPrefunctor.obj (CategoryTheory.SingleObj.star M))

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

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 : CategoryTheory.Functor (CategoryTheory.SingleObj M) (Type u)) (p : ↑(MulAction.fixedPoints M (J.toPrefunctor.obj (CategoryTheory.SingleObj.star M)))) : ∀ (x : CategoryTheory.SingleObj M), ↑((CategoryTheory.Limits.SingleObj.Types.sections.equivFixedPoints J).symm p) x = ↑p

@[simp]

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

def CategoryTheory.Limits.SingleObj.Types.sections.equivFixedPoints {M : Type v} [Monoid M] (J : CategoryTheory.Functor (CategoryTheory.SingleObj M) (Type u)) : ↑(CategoryTheory.Functor.sections J) ≃ ↑(MulAction.fixedPoints M (J.toPrefunctor.obj (CategoryTheory.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.limitEquivFixedPoints_apply_coe {M : Type v} [Monoid M] (J : CategoryTheory.Functor (CategoryTheory.SingleObj M) (Type u)) : ∀ (a : CategoryTheory.Limits.limit J), ↑((CategoryTheory.Limits.SingleObj.Types.limitEquivFixedPoints J) a) = CategoryTheory.Limits.limit.π J (CategoryTheory.SingleObj.star M) a

@[simp]

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

noncomputable def CategoryTheory.Limits.SingleObj.Types.limitEquivFixedPoints {M : Type v} [Monoid M] (J : CategoryTheory.Functor (CategoryTheory.SingleObj M) (Type u)) : CategoryTheory.Limits.limit J ≃ ↑(MulAction.fixedPoints M (J.toPrefunctor.obj (CategoryTheory.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)

theorem CategoryTheory.Limits.SingleObj.Types.Quot.Rel.iff_orbitRel {G : Type v} [Group G] (J : CategoryTheory.Functor (CategoryTheory.SingleObj G) (Type u)) (x : J.toPrefunctor.obj (CategoryTheory.SingleObj.star G)) (y : J.toPrefunctor.obj (CategoryTheory.SingleObj.star G)) : CategoryTheory.Limits.Types.Quot.Rel J { fst := CategoryTheory.SingleObj.star G, snd := x } { fst := CategoryTheory.SingleObj.star G, snd := y } ↔ Setoid.Rel (MulAction.orbitRel G (J.toPrefunctor.obj (CategoryTheory.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).

@[simp]

theorem CategoryTheory.Limits.SingleObj.Types.Quot.equivOrbitRelQuotient_apply {G : Type v} [Group G] (J : CategoryTheory.Functor (CategoryTheory.SingleObj G) (Type u)) (a : Quot (CategoryTheory.Limits.Types.Quot.Rel J)) : (CategoryTheory.Limits.SingleObj.Types.Quot.equivOrbitRelQuotient J) a = Quot.lift (fun (p : (j : CategoryTheory.SingleObj G) × J.toPrefunctor.obj j) => ⟦p.snd⟧) (_ : ∀ (a b : (j : CategoryTheory.SingleObj G) × J.toPrefunctor.obj j), CategoryTheory.Limits.Types.Quot.Rel J a b → ⟦a.snd⟧ = ⟦b.snd⟧) a

@[simp]

theorem CategoryTheory.Limits.SingleObj.Types.Quot.equivOrbitRelQuotient_symm_apply {G : Type v} [Group G] (J : CategoryTheory.Functor (CategoryTheory.SingleObj G) (Type u)) (a : Quot Setoid.r) : (CategoryTheory.Limits.SingleObj.Types.Quot.equivOrbitRelQuotient J).symm a = Quot.lift (fun (x : J.toPrefunctor.obj (CategoryTheory.SingleObj.star G)) => Quot.mk (CategoryTheory.Limits.Types.Quot.Rel J) { fst := CategoryTheory.SingleObj.star G, snd := x }) (_ : ∀ (a b : J.toPrefunctor.obj (CategoryTheory.SingleObj.star G)), Setoid.r a b → Quot.mk (CategoryTheory.Limits.Types.Quot.Rel J) { fst := CategoryTheory.SingleObj.star G, snd := a } = Quot.mk (CategoryTheory.Limits.Types.Quot.Rel J) { fst := CategoryTheory.SingleObj.star G, snd := b }) a

def CategoryTheory.Limits.SingleObj.Types.Quot.equivOrbitRelQuotient {G : Type v} [Group G] (J : CategoryTheory.Functor (CategoryTheory.SingleObj G) (Type u)) : CategoryTheory.Limits.Types.Quot J ≃ MulAction.orbitRel.Quotient G (J.toPrefunctor.obj (CategoryTheory.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.colimitEquivQuotient_symm_apply {G : Type v} [Group G] (J : CategoryTheory.Functor (CategoryTheory.SingleObj G) (Type u)) : ∀ (a : MulAction.orbitRel.Quotient G (J.toPrefunctor.obj (CategoryTheory.SingleObj.star G))), (CategoryTheory.Limits.SingleObj.Types.colimitEquivQuotient J).symm a = (CategoryTheory.Limits.Types.colimitEquivQuot J).symm (Quot.lift (fun (x : J.toPrefunctor.obj (CategoryTheory.SingleObj.star G)) => Quot.mk (CategoryTheory.Limits.Types.Quot.Rel J) { fst := CategoryTheory.SingleObj.star G, snd := x }) (_ : ∀ (a b : J.toPrefunctor.obj (CategoryTheory.SingleObj.star G)), Setoid.r a b → Quot.mk (CategoryTheory.Limits.Types.Quot.Rel J) { fst := CategoryTheory.SingleObj.star G, snd := a } = Quot.mk (CategoryTheory.Limits.Types.Quot.Rel J) { fst := CategoryTheory.SingleObj.star G, snd := b }) a)

@[simp]

theorem CategoryTheory.Limits.SingleObj.Types.colimitEquivQuotient_apply {G : Type v} [Group G] (J : CategoryTheory.Functor (CategoryTheory.SingleObj G) (Type u)) : ∀ (a : CategoryTheory.Limits.colimit J), (CategoryTheory.Limits.SingleObj.Types.colimitEquivQuotient J) a = Quot.lift (fun (p : (j : CategoryTheory.SingleObj G) × J.toPrefunctor.obj j) => ⟦p.snd⟧) (_ : ∀ (a b : (j : CategoryTheory.SingleObj G) × J.toPrefunctor.obj j), CategoryTheory.Limits.Types.Quot.Rel J a b → ⟦a.snd⟧ = ⟦b.snd⟧) ((CategoryTheory.Limits.Types.colimitEquivQuot J) a)

noncomputable def CategoryTheory.Limits.SingleObj.Types.colimitEquivQuotient {G : Type v} [Group G] (J : CategoryTheory.Functor (CategoryTheory.SingleObj G) (Type u)) : CategoryTheory.Limits.colimit J ≃ MulAction.orbitRel.Quotient G (J.toPrefunctor.obj (CategoryTheory.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)