English
The colimit of J: SingleObj G ⥤ Type is equivalent to the quotient of J(star G) by the induced G-action.
Русский
Колимит J: SingleObj G ⥤ Type эквивалентен фактор-множество J(star G) по индуцированному действию G.
LaTeX
$$$\\mathrm{colimit} J \\simeq \\mathrm{MulAction.orbitRel.Quotient}(G, J(\\mathrm{star} G))$$$
Lean4
/-- 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. -/
@[simps]
def colimitTypeRelEquivOrbitRelQuotient : J.ColimitType ≃ MulAction.orbitRel.Quotient G (J.obj (SingleObj.star G))
where
toFun := Quot.lift (fun p => ⟦p.2⟧) <| fun a b h => Quotient.sound <| (colimitTypeRel_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 <| (colimitTypeRel_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)
