diagramOverOpenπ — Mathlib

English

Let D be a gluing data and U an open subset in D.U i. There is a canonical projection from the limit of the gluing diagram to the component corresponding to j in the WalkingMultispan, i.e. a map to the j-th object of the diagram over open U.

Русский

Пусть D задаёт сшивку, и U открытое множество внутри D.U_i. Существует каноническая проекция из предела диаграммы сшивки на компоненту, соответствующую j в WalkingMultispan, т.е. отображение в j-ый объект диаграммы над открытым множеством U.

LaTeX

$$$\text{diagramOverOpenπ}_{i,U,j} : \varprojlim (D.\mathrm{diagramOverOpen}\,U) \to (D.\mathrm diagramOverOpen\,U).obj(\mathrm{op}\,j)$$$

Lean4

/-- (Implementation)
The projection from the limit of `diagram_over_open` to a component of `D.U j`. -/
abbrev diagramOverOpenπ {i : D.J} (U : Opens (D.U i).carrier) (j : D.J) :=
  limit.π (D.diagramOverOpen U) (op (WalkingMultispan.right j))

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