preserves_mono_of_preservesLimit — Mathlib

English

If F preserves pullbacks, then it preserves monomorphisms.

Русский

Если F сохраняет вытягивания (pullbacks), то он сохраняет мономорфизмы.

LaTeX

$$$\\forall f:X\\to Y,\\ mono(f)\\implies mono(F(map\\ f))$$$

Lean4

/-- If `F` preserves pullbacks, then it preserves monomorphisms. -/
theorem preserves_mono_of_preservesLimit {X Y : C} (f : X ⟶ Y) [PreservesLimit (cospan f f) F] [Mono f] :
    Mono (F.map f) := by
  have := isLimitPullbackConeMapOfIsLimit F _ (PullbackCone.isLimitMkIdId f)
  simp_rw [F.map_id] at this
  apply PullbackCone.mono_of_isLimitMkIdId _ this

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