hasCoequalizers_of_hasWideCoequalizers

English

In any colimit cocone over a parallelFamily, the component at one is epi.

Русский

В любом колимитном когломе параллельной семьи компонент на единице является эпиморфизмом.

LaTeX

$$$(c.ι_{one}) \text{ is epi}$$$

Lean4

instance (priority := 10) hasCoequalizers_of_hasWideCoequalizers [HasWideCoequalizers.{w} C] : HasCoequalizers C :=
  hasColimitsOfShape_of_equivalence.{w} walkingParallelFamilyEquivWalkingParallelPair

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