Mono of diagonal is mono

Stream: Is there code for X?

[Christian Merten]

Is there somewhere:

import Mathlib

open CategoryTheory Limits

lemma mono_of_pullback_mono {C : Type u} [Category.{v} C] {X Y : C}
    (f : X ⟶ Y) [HasPullback f f] [Mono (pullback.fst : pullback f f ⟶ X)] :
    Mono f where
  right_cancellation {Z} g h heq := by
    have h2 : pullback.lift g h heq = pullback.lift g g rfl := by
      apply (cancel_mono pullback.fst).mp
      simp only [limit.lift_π, PullbackCone.mk_π_app]
    convert_to pullback.lift g g rfl ≫ pullback.snd = h
    exact (pullback.lift_snd g g (rfl : g ≫ f = g ≫ f)).symm
    rw [← h2, limit.lift_π, PullbackCone.mk_π_app]

[Andrew Yang]

No but

import Mathlib.CategoryTheory.Limits.Shapes.Diagonal

open CategoryTheory Limits

lemma mono_of_pullback_mono {C : Type u} [Category.{v} C] {X Y : C}
    (f : X ⟶ Y) [HasPullback f f] [Mono (pullback.fst : pullback f f ⟶ X)] :
    Mono f :=
  have := isIso_of_mono_of_isSplitEpi (pullback.fst : pullback f f ⟶ X)
  (pullback.diagonal_isKernelPair f).mono_of_isIso_fst

[Andrew Yang]

I'd say you can make the proof inline unless you need to use it several times.

[Andrew Yang]

And also for the title, I think diagonal map usually refers to X ⟶ pullback f fand I think we are indeed missing

import Mathlib.CategoryTheory.Limits.Shapes.Diagonal

open CategoryTheory Limits pullback

lemma mono_of_diagonal_epi {C : Type u} [Category.{v} C] {X Y : C}
    (f : X ⟶ Y) [HasPullback f f] [Epi (pullback.diagonal f)] :
    Mono f :=
  have := isIso_of_epi_of_isSplitMono (pullback.diagonal f)
  have : IsIso (pullback.fst : diagonalObj f ⟶ _) := by
    rw [← (IsIso.inv_eq_of_hom_inv_id (diagonal_fst f))]
    infer_instance
  (pullback.diagonal_isKernelPair f).mono_of_isIso_fst

[Christian Merten]

Thank you!