mono_left_of_mono — Mathlib

English

If k is mono, then k.left is mono.

Русский

Если k моно, то k.left моно.

LaTeX

$$$\\operatorname{Mono}(k) \\Rightarrow \\operatorname{Mono}(k.\\text{left})$$$

Lean4

/-- If `k` is a monomorphism, then `k.left` is a monomorphism. In other words, `Over.forget X` preserves
monomorphisms.
The converse of `CategoryTheory.Over.mono_of_mono_left`.
-/
instance mono_left_of_mono {f g : Over X} (k : f ⟶ g) [Mono k] : Mono k.left :=
  by
  refine ⟨fun {Y : T} l m a => ?_⟩
  let l' : mk (m ≫ f.hom) ⟶ f :=
    homMk l (by dsimp; rw [← Over.w k, ← Category.assoc, congrArg (· ≫ g.hom) a, Category.assoc])
  suffices l' = (homMk m : mk (m ≫ f.hom) ⟶ f) by apply congrArg CommaMorphism.left this
  rw [← cancel_mono k]
  ext
  apply a

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