Lean4
/-- The second leg of a pullback cone is a regular monomorphism if the right component is too.
See also `Pullback.sndOfMono` for the basic monomorphism version, and
`regularOfIsPullbackFstOfRegular` for the flipped version.
-/
def regularOfIsPullbackSndOfRegular {P Q R S : C} {f : P ⟶ Q} {g : P ⟶ R} {h : Q ⟶ S} {k : R ⟶ S} [hr : RegularMono h]
(comm : f ≫ h = g ≫ k) (t : IsLimit (PullbackCone.mk _ _ comm)) : RegularMono g
where
Z := hr.Z
left := k ≫ hr.left
right := k ≫ hr.right
w := by
repeat (rw [← Category.assoc, ← eq_whisker comm])
simp only [Category.assoc, hr.w]
isLimit := by
apply Fork.IsLimit.mk' _ _
intro s
have l₁ : (Fork.ι s ≫ k) ≫ RegularMono.left = (Fork.ι s ≫ k) ≫ hr.right := by
rw [Category.assoc, s.condition, Category.assoc]
obtain ⟨l, hl⟩ := Fork.IsLimit.lift' hr.isLimit _ l₁
obtain ⟨p, _, hp₂⟩ := PullbackCone.IsLimit.lift' t _ _ hl
refine ⟨p, hp₂, ?_⟩
intro m w
have z : m ≫ g = p ≫ g := w.trans hp₂.symm
apply t.hom_ext
apply (PullbackCone.mk f g comm).equalizer_ext
· erw [← cancel_mono h, Category.assoc, Category.assoc, comm]
simp only [← Category.assoc, eq_whisker z]
· exact z
