descMonoidHom_quotMk — Mathlib

English

The map descMonoidHom commutes with quotient.mk, aligning the colimit description with representatives.

Русский

Карта descMonoidHom коммутирует с quotient.mk, согласуя описание колимита с представительствами.

LaTeX

$$descMonoidHom t (Quot.mk _ ⟨j,x⟩) = t.ι.app j x$$

Lean4

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

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