descAddMonoidHom_quotMk — Mathlib

English

Let F be a diagram F: J ⥤ SemiRingCat with a cocone t. For every object j in J and every x in F.obj j, the value of the descent AddMonoidHom applied to the class [j, x] is exactly the component t.ι.app j applied to x; i.e. the descent map sends the representative (j, x) to the image of x in the colimit.

Русский

Пусть F: J ⥤ SemiRingCat – диаграмма, имеющая кокон t. Для любого объекта j ∈ J и любого x ∈ F.obj j значение отображения спуска AddMonoidHom, применённого к классy [j, x], равно компоненте кокона: t.ι.app j x.

LaTeX

$$$ \\mathrm{descAddMonoidHom}(t)(\\mathrm{Quot.mk}_{\\_}(\\langle j, x \\rangle)) = t.\\iota_{j}(x)$$$

Lean4

theorem descAddMonoidHom_quotMk {j : J} (x : F.obj j) : descAddMonoidHom t (Quot.mk _ ⟨j, x⟩) = t.ι.app j x :=
  congr_fun
    ((forget _).congr_map
      ((AddCommMonCat.FilteredColimits.colimitCoconeIsColimit.{v, u} (F ⋙ forget₂ SemiRingCat AddCommMonCat)).fac
        ((forget₂ SemiRingCat AddCommMonCat).mapCocone t) j))
    x

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