desc_quotQuotUliftAddEquiv — Mathlib

English

For any f: Quot F →+ A and hc IsColimit of c, the value of hc.desc(toCocone F f) at Quot.desc F c x equals f x for any x ∈ Quot F.

Русский

Для любого f: Quot F →+ A и hc, являющегося IsColimit для c, значение hc.desc(toCocone F f) на Quot.desc F c x равно f x для любого x ∈ Quot F.

LaTeX

$$$ (hc.desc (toCocone F f)).hom (Quot.desc F c x) = f x $$$

Lean4

theorem desc_quotQuotUliftAddEquiv [DecidableEq J] (c : Cocone F) :
    (Quot.desc (F ⋙ uliftFunctor.{u'}) (uliftFunctor.{u'}.mapCocone c)).comp (quotQuotUliftAddEquiv F).toAddMonoidHom =
      AddEquiv.ulift.symm.toAddMonoidHom.comp (Quot.desc F c) :=
  by
  refine Quot.addMonoidHom_ext _ (fun j a ↦ ?_)
  dsimp
  simp only [quotToQuotUlift_ι, Functor.comp_obj, uliftFunctor_obj, ι_desc, Functor.const_obj_obj, ι_desc]
  erw [Quot.ι_desc]
  rfl

Похожие утверждения