English
Compatibility of quotUliftToQuot with injections: for any j ∈ J and x ∈ (F ⋙ uliftFunctor).obj j, applying quotUliftToQuot to Quot.ι F j x yields Quot.ι F j x.down.
Русский
Совместимость quotUliftToQuot с инъекциями: для любого j ∈ J и x ∈ (F ⋙ uliftFunctor).obj j применение quotUliftToQuot к Quot.ι F j x даёт Quot.ι F j x.down.
LaTeX
$$$ \operatorname{quotUliftToQuot} F (\mathrm{Quot}.\mathrm{ι} F j x) = \mathrm{Quot}.\mathrm{ι} F j x.\downarrow $$$
Lean4
theorem quotUliftToQuot_ι [DecidableEq J] (j : J) (x : (F ⋙ uliftFunctor.{u'}).obj j) :
quotUliftToQuot F (Quot.ι _ j x) = Quot.ι F j x.down :=
by
dsimp [quotUliftToQuot, Quot.ι]
conv_lhs =>
erw [AddMonoidHom.comp_apply (QuotientAddGroup.mk' (Relations (F ⋙ uliftFunctor))) (DFinsupp.singleAddHom _ j),
QuotientAddGroup.lift_mk']
simp only [Functor.comp_obj, uliftFunctor_obj, DFinsupp.singleAddHom_apply, DFinsupp.sumAddHom_single,
AddMonoidHom.coe_comp, AddMonoidHom.coe_coe, Function.comp_apply]
rfl
