hasReflexiveCoequalizers_iff — Mathlib

English

There is an equivalence between having colimits of shape WalkingReflexivePair and having reflexive coequalizers.

Русский

Существование колимитов формы WalkingReflexivePair эквивалентно существованию рефлексивных кофокоров.

LaTeX

$$HasColimitsOfShape WalkingReflexivePair C ↔ HasReflexiveCoequalizers C$$

Lean4

/-- A category has coequalizers of reflexive pairs if and only if it has all colimits indexed by the
walking reflexive pair. -/
theorem hasReflexiveCoequalizers_iff : HasColimitsOfShape WalkingReflexivePair C ↔ HasReflexiveCoequalizers C :=
  ⟨fun _ ↦
    ⟨fun _ _ f g _ ↦
      (hasReflexiveCoequalizer_iff_hasCoequalizer (reflexivePair f g (commonSection f g))).1 inferInstance⟩,
    fun _ ↦ ⟨inferInstance⟩⟩

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