mono_of_mono_right — Mathlib

English

In a pushout diagram with van Kampen property, if the left leg is mono then i is mono; likewise, if the right leg is mono then h is mono. These are corollaries of the van Kampen framework.

Русский

В диаграмме pushout с свойством ван-Кемпен, если левая стрелка моно, то i моно; аналогично для правой стрелки и h. Это следствия ван-Кемпена.

LaTeX

$$$[Mono f] \Rightarrow (H.IsVanKampen) \Rightarrow Mono i$ and $[ Mono g ] \Rightarrow Mono h$$$

Lean4

theorem mono_of_mono_right [Mono g] {H : IsPushout f g h i} (H' : H.IsVanKampen) : Mono h :=
  IsKernelPair.mono_of_isIso_fst
    ((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⟩)).1

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