of_vert_isIso_mono — Mathlib

English

If the right edge is an isomorphism and the left edge is mono, then the square is a pullback.

Русский

Если правая стрелка изоморфизм и левая мономорфизм, то квадрат является пуллбаком.

LaTeX

$$$ [IsIso\\; snd] \\; [Mono\\; f] \\; (sq: CommSq fst snd f g) \\Rightarrow IsPullback fst snd f g $$$

Lean4

theorem of_vert_isIso_mono [IsIso snd] [Mono f] (sq : CommSq fst snd f g) : IsPullback fst snd f g :=
  IsPullback.flip (of_horiz_isIso_mono sq.flip)

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