of_horiz_isIso_mono — Mathlib

English

If the top horizontal arrow is an isomorphism and the right vertical arrow is mono, then a commutative square is a pullback.

Русский

Если верхняя горизонтальная стрелка изоморфизм, правая вертикальная стрелка моно, то данный квадрат является пределом.

LaTeX

$$$ \text{CommSq fst snd f g} \land [IsIso fst] \land [Mono g] \Rightarrow IsPullback fst snd f g $$$

Lean4

theorem of_horiz_isIso_mono [IsIso fst] [Mono g] (sq : CommSq fst snd f g) : IsPullback fst snd f g :=
  of_isLimit' sq
    (by
      refine PullbackCone.IsLimit.mk _ (fun s => s.fst ≫ inv fst) (by simp) (fun s => ?_) (by cat_disch)
      simp only [← cancel_mono g, Category.assoc, ← sq.w, IsIso.inv_hom_id_assoc, s.condition])

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