English
For a diagram F: J ⥤ MonoOver Y and a cocone c, a certain Sigma-desc construction yields a commuting square with the strong epi–mono factorisation.
Русский
Для диаграммы $F: J \to MonoOver Y$ и какому-либо кокониму $c$ получаем композицию, образующую коммутативный квадрат между факторизациями сильного эпиморфизма и монообраза.
LaTeX
$$CommSq (Sigma.desc ...) (strongEpiMonoFactorisationSigmaDesc F).e c.pt.arrow (strongEpiMonoFactorisationSigmaDesc F).m$$
Lean4
theorem commSqOfHasStrongEpiMonoFactorisation (F : J ⥤ MonoOver Y) (c : Cocone F) :
CommSq (Sigma.desc fun i ↦ (c.ι.app i).left) (strongEpiMonoFactorisationSigmaDesc F).e c.pt.arrow
(strongEpiMonoFactorisationSigmaDesc F).m
where
w := by
apply Sigma.hom_ext
intro j
simp only [colimit.ι_desc_assoc, Discrete.functor_obj_eq_as, Cofan.mk_pt, Cofan.mk_ι_app, MonoFactorisation.fac,
colimit.ι_desc]
convert (c.ι.app j).w
simp only [const_obj_obj, CostructuredArrow.right_eq_id, const_obj_map, comp_id]
exact rfl
