hasCoequalizer_of_common_section — Mathlib

English

Given a common section r: B→A with rf = id and rg = id, the coequalizer of f and g exists.

Русский

При наличии общего сектора r: B→A с rf = id и rg = id, существует коэквализатор для f и g.

LaTeX

$$$\\text{hasCoequalizer}(f,g) \\text{ under reflexive assumptions with } r: B \\to A, rf = id_A, rg = id_A$$$

Lean4

theorem hasCoequalizer_of_common_section [HasReflexiveCoequalizers C] {A B : C} {f g : A ⟶ B} (r : B ⟶ A)
    (rf : r ≫ f = 𝟙 _) (rg : r ≫ g = 𝟙 _) : HasCoequalizer f g :=
  by
  letI := IsReflexivePair.mk' r rf rg
  infer_instance

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