lim_μ_π — Mathlib

English

For a pair of diagrams F and G, and for each index j, the monoidal multiplication map on the limit together with the projection equals the tensor of the two projections: μ lim F G ≫ limit.π_j = limit.π_F_j ⊗ limit.π_G_j.

Русский

Для пары диаграмм F и G и для каждого индекса j композиция умножения в моноидальной структуре на пределе с проекцией равна тензору проекций: μ lim F G ≫ limit.π_j = limit.π_F_j ⊗ limit.π_G_j.

LaTeX

$$$\\mu\\,\\lim F G \\;\\circ\\; \\mathrm{limit}.\\pi_{j} = \\mathrm{limit}.\\pi_{F j} \\; \\otimes_{\\mathsf{C}}\\; \\mathrm{limit}.\\pi_{G j}$$$

Lean4

@[reassoc (attr := simp)]
theorem lim_μ_π (F G : J ⥤ C) (j : J) : μ lim F G ≫ limit.π _ j = limit.π F j ⊗ₘ limit.π G j :=
  limit.lift_π _ _

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