isIso_snd_iso_of_mono — Mathlib

English

If f is mono and h is a pullback with f on both legs, then snd is an isomorphism.

Русский

Если f моно и двойной предел по f,f, то snd является изоморфизмом.

LaTeX

$$$ {P X Y : C} {fst : P \to X} {snd : P \to X} {f : X \to Y} [Mono f] (h : IsPullback fst snd f f) : IsIso snd $$$

Lean4

theorem isIso_snd_iso_of_mono {P X Y : C} {fst : P ⟶ X} {snd : P ⟶ X} {f : X ⟶ Y} [Mono f]
    (h : IsPullback fst snd f f) : IsIso snd :=
  h.cone.isIso_snd_of_mono_of_isLimit h.isLimit

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