hasEqualizer_of_common_retraction

English

If there exists r: B → A with f ∘ r = id_B and g ∘ r = id_B, then HasEqualizer f g.

Русский

Если существует r: B → A с f ∘ r = id_B и g ∘ r = id_B, то HasEqualizer f g существует.

LaTeX

$$$\exists r: B \to A,\; (f \circ r = \mathrm{id}_B) \land (g \circ r = \mathrm{id}_B) \Rightarrow \text{HasEqualizer}(f,g)$$$

Lean4

theorem hasEqualizer_of_common_retraction [HasCoreflexiveEqualizers C] {A B : C} {f g : A ⟶ B} (r : B ⟶ A)
    (fr : f ≫ r = 𝟙 _) (gr : g ≫ r = 𝟙 _) : HasEqualizer f g :=
  by
  letI := IsCoreflexivePair.mk' r fr gr
  infer_instance

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