English
The descent along F to the colimit cocone equals the Shrink addEquiv inverse: Quot.desc F (colimitCocone F) = Shrink.addEquiv (α := Quot F)).symm.toAddMonoidHom.
Русский
Спуск по F к колимитному кооконe равен обратной карте сокращения: Quot.desc F (colimitCocone F) = Shrink.addEquiv (α := Quot F).symm.toAddMonoidHom.
LaTeX
$$$ \mathrm{Quot}.\mathrm{desc} F (\mathrm{colimitCocone} F) = \mathrm{Shrink}.\mathrm{addEquiv}(\alpha := \mathrm{Quot} F).\mathrm{symm}.toAddMonoidHom $$$
Lean4
@[simp]
theorem desc_colimitCocone [DecidableEq J] (F : J ⥤ AddCommGrpCat.{w}) [Small.{w} (Quot F)] :
Quot.desc F (colimitCocone F) = (Shrink.addEquiv (α := Quot F)).symm.toAddMonoidHom :=
by
refine Quot.addMonoidHom_ext F (fun j x ↦ ?_)
simpa only [colimitCocone_pt, AddEquiv.toAddMonoidHom_eq_coe, AddMonoidHom.coe_coe] using
Quot.ι_desc F (colimitCocone F) j x
