English
Two natural constructions yield equal additive monoid homomorphisms: the descent along the lifted diagram followed by quotQuotUliftAddEquiv, and the inverse AddEquiv.ulift composed with the descent along F. They are equal as monoid homomorphisms.
Русский
Две естественные конструкции дают равные моноид-гомоморфизмы: спуск по поднятому диаграмме с последующим quotQuotUliftAddEquiv и обратное отображение AddEquiv.ulift после спуска по F. Они равны.
LaTeX
$$$ (\mathrm{Quot.desc} (F \circ \mathrm{uliftFunctor}) (\mathrm{uliftFunctor}.mapCocone c)).{\rm toAddMonoidHom} \circ (\mathrm{quotQuotUliftAddEquiv} F) = (\mathrm{AddEquiv.ulift.symm.toAddMonoidHom}) \circ (\mathrm{Quot.desc} F c) $$$
Lean4
theorem quotToQuotUlift_ι [DecidableEq J] (j : J) (x : F.obj j) :
quotToQuotUlift F (Quot.ι F j x) = Quot.ι _ j (ULift.up x) :=
by
dsimp [quotToQuotUlift, Quot.ι]
conv_lhs =>
erw [AddMonoidHom.comp_apply (QuotientAddGroup.mk' (Relations F)) (DFinsupp.singleAddHom _ j),
QuotientAddGroup.lift_mk']
simp only [DFinsupp.singleAddHom_apply, DFinsupp.sumAddHom_single, AddMonoidHom.coe_comp, AddMonoidHom.coe_coe,
Function.comp_apply]
rfl
