hasCoequalizer_of_hasSplitCoequalizer

English

Explicit quotient construction of the colimit is equivalent to the quotient by the induced action on J(star G).

Русский

Явная конструкция колимита через фактор-множество эквивалентна фактору по индуцированному действию на J(star G).

LaTeX

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

Lean4

/-- If a pair has a split coequalizer, it has a coequalizer. -/
instance (priority := 1) hasCoequalizer_of_hasSplitCoequalizer [HasSplitCoequalizer f g] : HasCoequalizer f g :=
  HasColimit.mk ⟨_, (HasSplitCoequalizer.isSplitCoequalizer f g).isCoequalizer⟩

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