English
If a category has images, pullbacks, and equalizers, then images are strong epi images.
Русский
Если в категории существуют образы, поперечные пределы и равносходы, то образы становятся сильными epi-образами.
LaTeX
$$$\text{HasPullbacks}(C) \wedge \text{HasEqualizers}(C) \wedge \text{HasImages}(C) \Rightarrow \text{HasStrongEpiImages}(C)$$$
Lean4
/-- If a category has images, equalizers and pullbacks, then images are automatically strong epi
images. -/
instance (priority := 100) hasStrongEpiImages_of_hasPullbacks_of_hasEqualizers [HasPullbacks C] [HasEqualizers C] :
HasStrongEpiImages C where
strong_factorThruImage
f :=
StrongEpi.mk' fun {A} {B} h h_mono x y sq =>
CommSq.HasLift.mk'
{ l :=
image.lift
{ I := pullback h y
m := pullback.snd h y ≫ image.ι f
m_mono := mono_comp _ _
e := pullback.lift _ _ sq.w } ≫
pullback.fst h y
fac_left := by simp only [image.fac_lift_assoc, pullback.lift_fst]
fac_right := by
apply image.ext
simp only [sq.w, Category.assoc, image.fac_lift_assoc, pullback.lift_fst_assoc] }
