colimitEquivQuotient — Mathlib

English

The colimit of J is equivalent to the quotient by the induced action, i.e., there is an equivalence with MulAction.orbitRel.Quotient(G, J(star G)).

Русский

Колимит J эквивалентен фактору по индуцированному действию, то есть существует эквивалентность с MulAction.orbitRel.Quotient(G, J(star G)).

LaTeX

$$$\\text{colimitEquivQuotient }(J) :\\; \\mathrm{colimit} J \\simeq \\mathrm{MulAction.orbitRel.Quotient}(G, J(\\mathrm{star} G))$$$

Lean4

/-- The colimit of `J : SingleObj G ⥤ Type u` is equivalent to the quotient of
`J.obj (SingleObj.star G)` by the induced action. -/
@[simps!]
noncomputable def colimitEquivQuotient : colimit J ≃ MulAction.orbitRel.Quotient G (J.obj (SingleObj.star G)) :=
  (Types.colimitEquivColimitType J).trans (colimitTypeRelEquivOrbitRelQuotient J)

Похожие утверждения