English
Given a function U : ι → α into a complete lattice, there is a functor diagram(U) : Pairwise ι ⥤ α sending single i to U(i) and pair i j to U(i) ⊓ U(j), with the action on morphisms given by diagramMap.
Русский
Пусть имеется функция U : ι → α в полную решётку. Тогда существует функтор diagram(U) : Pairwise ι ⥤ α, который отображает одиночные элементы i в U(i), пары i j в U(i) ⊓ U(j), а действием на морфизмы задаётся diagramMap.
LaTeX
$$$\mathrm{diagram}(U) : \mathrm{Pairwise}\, ι \to α, \quad \mathrm{diagram}(U)(\mathrm{single\;i}) = U(i), \quad \mathrm{diagram}(U)(\mathrm{pair\;i\;j}) = U(i) \wedge U(j), \quad \mathrm{diagram}(U)(\text{Hom}) = \mathrm{diagramMap}_U.$$$
Lean4
/-- Given a function `U : ι → α` for `[SemilatticeInf α]`, we obtain a functor `Pairwise ι ⥤ α`,
sending `single i` to `U i` and `pair i j` to `U i ⊓ U j`,
and the morphisms to the obvious inequalities.
-/
@[simps]
def diagram : Pairwise ι ⥤ α where
obj := diagramObj U
map := diagramMap U
