lim_ε_π — Mathlib

English

In a monoidal setting with limits, for every object J in the index category, the structural map ε applied to the limit composed with the projection to J is the identity on the corresponding component.

Русский

В условиях моноидального категория и пределов для каждого индекса j из категории индексов последовательности, аппроксимационная карта ε на пределе, компонуемая с проекцией к j, равна тождественному отображению на соответствующем компоненте.

LaTeX

$$$\\varepsilon_{\\lim (J \\to C)} \\; \\circ \\mathrm{limit}.\\pi_{j} = \\mathrm{id}_{F_j}$$$

Lean4

@[reassoc (attr := simp)]
theorem lim_ε_π (j : J) : ε (lim (J := J) (C := C)) ≫ limit.π _ j = 𝟙 _ :=
  limit.lift_π _ _

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