Theorems · Definition · category theory

CategoryTheory.Limits.SingleObj.colimitTypeRelEquivOrbitRelQuotient

{G : Type v} →
  [inst : Group G] →
    (J : CategoryTheory.Functor (CategoryTheory.SingleObj G) (Type u)) →
      J.ColimitType ≃ MulAction.orbitRel.Quotient G (J.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.

Defined in

Mathlib.CategoryTheory.Limits.Shapes.SingleObj

Cited by

2 results in Mathlib

Foundations

Depth 69 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

Group