normalOfIsPullbackSndOfNormal — Mathlib

Lean4
/-- The second leg of a pullback cone is a normal monomorphism if the right component is too.

See also `pullback.sndOfMono` for the basic monomorphism version, and
`normalOfIsPullbackFstOfNormal` for the flipped version.
-/
def normalOfIsPullbackSndOfNormal {P Q R S : C} {f : P ⟶ Q} {g : P ⟶ R} {h : Q ⟶ S} {k : R ⟶ S} [hn : NormalMono h]
    (comm : f ≫ h = g ≫ k) (t : IsLimit (PullbackCone.mk _ _ comm)) : NormalMono g
    where
  Z := hn.Z
  g := k ≫ hn.g
  w :=
    by
    have reassoc' {W : C} (h' : S ⟶ W) : f ≫ h ≫ h' = g ≫ k ≫ h' := by simp only [← Category.assoc, eq_whisker comm]
    rw [← reassoc', hn.w, HasZeroMorphisms.comp_zero]
  isLimit := by
    letI gr := regularOfIsPullbackSndOfRegular comm t
    have q := (HasZeroMorphisms.comp_zero k hn.Z).symm
    convert gr.isLimit
Похожие утверждения