English
A compatibility between two descent constructions and an AddEquiv: the composition of quotQuotUliftAddEquiv and the lifted descent equals the composition of the lifted descent with toAddMonoidHom from F to c.
Русский
Совместимость двух построений спуска и AddEquiv: композиция quotQuotUliftAddEquiv и поднятого спуска равна композиции поднятого спуска с toAddMonoidHom из F в c.
LaTeX
$$$ (\,\operatorname{Quot.desc} (F \cdot \mathrm{uliftFunctor}) (\mathrm{uliftFunctor}.mapCocone c)\,).comp (\mathrm{quotQuotUliftAddEquiv} F).toAddMonoidHom = \n \mathrm{AddEquiv.ulift.symm.toAddMonoidHom}.comp (\mathrm{Quot.desc} F c) $$$
Lean4
theorem desc_toCocone_desc [DecidableEq J] {A : Type w} [AddCommGroup A] (f : Quot F →+ A) (hc : IsColimit c) :
(hc.desc (toCocone F f)).hom.comp (Quot.desc F c) = f :=
by
refine Quot.addMonoidHom_ext F (fun j x ↦ ?_)
rw [AddMonoidHom.comp_apply, ι_desc]
change (c.ι.app j ≫ hc.desc (toCocone F f)) _ = _
rw [hc.fac]
simp
