isPullback_of_mono_left — Mathlib

English

In an adhesive category, if a pushout square is van Kampen and the left leg is mono, then the square is a pullback.

Русский

В адгезивной категории, если квадрат pushout является ван-Кемпен и левая стрелка моно, то квадрат является pullback.

LaTeX

$$$[Mono f] \Rightarrow IsPushout\ f g h i \Rightarrow IsPullback f g h i$$

Lean4

theorem isPullback_of_mono_left [Mono f] {H : IsPushout f g h i} (H' : H.IsVanKampen) : IsPullback f g h i :=
  ((H' (𝟙 _) g g (𝟙 Y) (𝟙 _) f (𝟙 _) i (IsKernelPair.id_of_mono f) (IsPullback.of_vert_isIso ⟨by simp⟩) H.1.flip ⟨rfl⟩
            ⟨by simp⟩).mp
        (IsPushout.of_horiz_isIso ⟨by simp⟩)).1.flip

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