Colimit of functor from `SingleObj` is quotient

Stream: Is there code for X?

[Christian Merten]

Do we have that the colimit of some SingleObj G ⥤ Type* is the quotient by the induced MulAction?

import Mathlib

open CategoryTheory Limits

variable {G : Type*} [Group G] (J : SingleObj G ⥤ Type*)

instance : MulAction G (J.obj (SingleObj.star G)) where
  smul g x := J.map g x
  one_smul x := by
    show J.map (𝟙 _) x = x
    simp only [FunctorToTypes.map_id_apply]
  mul_smul g h x := by
    show J.map (g * h) x = (J.map h ≫ J.map g) x
    rw [← SingleObj.comp_as_mul]
    simp only [FunctorToTypes.map_comp_apply, types_comp_apply]
    rfl

def quotCocone : Cocone J where
  pt := MulAction.orbitRel.Quotient G (J.obj (SingleObj.star G))
  ι := by
    apply SingleObj.natTrans
    intro g
    show J.map g ≫ (fun x ↦ ⟦x⟧) = (fun x ↦ ⟦x⟧)
    ext x
    simp only [types_comp_apply]
    apply Quotient.sound
    exact Exists.intro g rfl

def quotCoconeIsColimit : IsColimit (quotCocone J) where
  desc s := sorry
  fac := sorry
  uniq := sorry

Loogling for MulAction.orbitRel and CategoryTheory.Limits.IsColimit did not yield anything, but I wanted to make sure, I am not missing something.

[Adam Topaz]

I don't think we have this.

[Kim Morrison]

Can you reuse anything from Mathlib.CategoryTheory.Limits.Types?

[Kim Morrison]

It's straightforward enough there's no particular need to reuse anything, I guess.

[Adam Topaz]

docs#CategoryTheory.Limits.Types.colimitCocone essentially gives this, except for identifying the sigma type over Unit with a single type.

[Adam Topaz]

Maybe we should develop some API for (co)limits of categories with a single isomorphism class of objects?

[Christian Merten]

The equivalence relation defined for docs#CategoryTheory.Limits.Types.Quot should be the same as the one from orbitRel right?

[Adam Topaz]

I think so, yes.

[Christian Merten]

Adam Topaz said:

Maybe we should develop some API for (co)limits of categories with a single isomorphism class of objects?

You mean with target Type or more generally?

[Adam Topaz]

Mostly for type (or more generally concrete cats satisfying some (co)limit preservation condition), but maybe there are interesting things one can say more generally?

[Adam Topaz]

I guess it's true in general that when $M$ is a monoid acting on some object $X$ in a category, that one gets a functor as you describe above, and if the categorical quotient $X/M$ exists then it is the colimit of this functor. That would be a nice thing to formalize! I guess the limit is the categorical "fixed points" construction?

[Adam Topaz]

I don't think mathlib knows about quotients of objects in general categories.

[Christian Merten]

Isn't a categorical quotient (if it exists), by definition the colimit of some SingleObj G ⥤ C?

[Adam Topaz]

Well, it depends on how you define it :)

[Adam Topaz]

It's also the universal object $Q$ with a map $X \to Q$ which is equivariant where the action on $Q$ is trivial.

[Christian Merten]

I think I prefer the colimit definition though, since you need to have the functor SingleObj G ⥤ C to define the action anyway.

[Adam Topaz]

Well here one could define it as a morphism of monoids from $M$ to $End(X)$.

[Christian Merten]

This is all about single object categories though, not as you initially suggested, about connected groupoids categories with a single isomorphism class, I don't know if there is anything intersting to say about that.
(connected groupoids are only one case of these)

[Christian Merten]

Btw, yes Types.Quot.Rel and MulAction.orbitRel agree up to twisting arguments and inverting morphisms:

lemma foo (x y : J.obj (SingleObj.star G)) :
    Types.Quot.Rel J ⟨SingleObj.star G, x⟩ ⟨SingleObj.star G, y⟩
    ↔ Setoid.Rel (MulAction.orbitRel G (J.obj (SingleObj.star G))) x y := by
  conv => rhs; rw [Setoid.comm']
  show (∃ g : G, y = g • x) ↔ (∃ g : G, g • x = y)
  aesop

[Christian Merten]

Where should this go?

lemma Types.Quot.Rel.iff_orbitRel (x y : J.obj (SingleObj.star G)) :
    Types.Quot.Rel J ⟨SingleObj.star G, x⟩ ⟨SingleObj.star G, y⟩
    ↔ Setoid.Rel (MulAction.orbitRel G (J.obj (SingleObj.star G))) x y := by
  have h (g : G) : y = g • x ↔ g • x = y := ⟨symm, symm⟩
  conv => rhs; rw [Setoid.comm']
  show (∃ g : G, y = g • x) ↔ (∃ g : G, g • x = y)
  conv => lhs; simp only [h]

def Types.Quot.equivOrbitRelQuotient :
    Types.Quot J ≃ MulAction.orbitRel.Quotient G (J.obj (SingleObj.star G)) where
  toFun := Quot.lift (fun p => ⟦p.2⟧) <| fun a b h => Quotient.sound <|
    (Types.Quot.Rel.iff_orbitRel J a.2 b.2).mp h
  invFun := Quot.lift (fun x => Quot.mk _ ⟨SingleObj.star G, x⟩) <| fun a b h =>
    Quot.sound <| (Types.Quot.Rel.iff_orbitRel J a b).mpr h
  left_inv := fun x => Quot.inductionOn x (fun _ ↦ rfl)
  right_inv := fun x => Quot.inductionOn x (fun _ ↦ rfl)

noncomputable def Types.quotientEquiv :
    colimit J ≃ MulAction.orbitRel.Quotient G (J.obj (SingleObj.star G)) :=
  (Types.colimitEquivQuot J).trans (Types.Quot.equivOrbitRelQuotient J)

New file in a new folder, e.g. Mathlib.CategoryTheory.Limits.Shapes.Quotients.Types?

[Christian Merten]

We could add the characterisation that @Adam Topaz suggested yesterday in that folder as well.

[Christian Merten]

And maybe name the folder SingleObj instead of Quotients to not discriminate against limits.

[Christian Merten]

Adam Topaz said:

It's also the universal object $Q$ with a map $X \to Q$ which is equivariant where the action on $Q$ is trivial.

Is this what you had in mind?

variable {M : Type v} [Monoid M] {C : Type u₁} [Category.{u₂} C]

structure IsQuotient {X : C} (f : M →* End X) where
  Q : C
  π : X ⟶ Q
  inv : ∀ m, f m ≫ π = π
  desc {Y : C} (g : X ⟶ Y) (h : ∀ m, f m ≫ g = g) : Q ⟶ Y
  fac {Y : C} (g : X ⟶ Y) (h : ∀ m, f m ≫ g = g) : π ≫ desc g h = g
  uniq {Y : C} (g : X ⟶ Y) (h : ∀ m, f m ≫ g = g) (g' : Q ⟶ Y) (hf : π ≫ g' = g) :
    g' = desc g h

[Kim Morrison]

I think just Mathlib.CategoryTheory.Limits.Shapes.SingleObj is right.

[Christian Merten]

This is #10213.