mono_of_isLimitMkIdId — Mathlib

English

Let f: X → Z and i: Z → W with i mono. Then HasPullback (f ≫ i) i.

Русский

Пусть f: X → Z и i: Z → W — моно. Тогда HasPullback (f ≫ i) i.

LaTeX

$$$HasPullback (f \circ i) i.$$$

Lean4

/-- `f` is a mono if the pullback cone `(𝟙 X, 𝟙 X)` is a limit for the pair `(f, f)`. The converse is
given in `PullbackCone.is_id_of_mono`.
-/
theorem mono_of_isLimitMkIdId (f : X ⟶ Y) (t : IsLimit (mk (𝟙 X) (𝟙 X) rfl : PullbackCone f f)) : Mono f :=
  ⟨fun {Z} g h eq => by
    rcases PullbackCone.IsLimit.lift' t _ _ eq with ⟨_, rfl, rfl⟩
    rfl⟩

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