isPullback_of_mono_right — Mathlib

English

Dual to the left version: in an adhesive category, if a pushout square has the right leg mono and is van Kampen, then the square is a pullback.

Русский

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

LaTeX

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

Lean4

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

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