mono_fst_of_is_pullback_of_mono — Mathlib

English

Let f: X → Z and i: Z → W be a morphism with i mono. Then HasPullback i (f ≫ i).

Русский

Пусть f: X → Z и i: Z → W — моно-морфизм. Тогда существует pullback i (f ≫ i).

LaTeX

$$$HasPullback\ i\\ (f \circ i).$$$

Lean4

/-- Monomorphisms are stable under pullback in the second argument. -/
theorem mono_fst_of_is_pullback_of_mono {t : PullbackCone f g} (ht : IsLimit t) [Mono g] : Mono t.fst :=
  by
  refine ⟨fun {W} h k i => IsLimit.hom_ext ht i ?_⟩
  rw [← cancel_mono g, Category.assoc, Category.assoc, ← condition]
  apply reassoc_of% i

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