English
For a function U : ι → α into a semilattice Inf α, there is a canonical way to assign to each morphism in the Pairwise ι diagram a morphism between the corresponding diagram objects. Specifically, id on single and id on pair go to identity maps, while the left and right morphisms correspond to the infimum projections.
Русский
Для функции U : ι → α в полную связку полусферы Inf α существует канонический способ сопоставления каждому морфизму в диаграмме Pairwise ι соответствующий морфизм между соответствующими объектами диаграммы. Иными словами, тождественные стрелки от одиночки и пары переходят в тождественные отображения, а стрелки влево и вправо соответствуют проекциям на Inf операции.
LaTeX
$$$\mathrm{diagramMap}_U : \forall o_1,o_2 : \mathrm{Pairwise}\, ι\, (o_1 \to o_2) \to \mathrm{diagramObj}\,U\,o_1 \to \mathrm{diagramObj}\,U\,o_2, \\
\text{with } \\
\mathrm{diagramMap}_U(\mathrm{id_{single\;i}}) = \mathrm{Id}_{U(i)}, \\
\mathrm{diagramMap}_U(\mathrm{id_{pair\;i\;j}}) = \mathrm{Id}_{U(i) \wedge U(j)}, \\
\mathrm{diagramMap}_U(\mathrm{left\;i\;j}) = \mathrm{homOfLE}(\inf\le\text{Left}), \\
\mathrm{diagramMap}_U(\mathrm{right\;i\;j}) = \mathrm{homOfLE}(\inf\le\text{Right}).$$$
Lean4
/-- Auxiliary definition for `diagram`. -/
@[simp]
def diagramMap : ∀ {o₁ o₂ : Pairwise ι} (_ : o₁ ⟶ o₂), diagramObj U o₁ ⟶ diagramObj U o₂
| _, _, id_single _ => 𝟙 _
| _, _, id_pair _ _ => 𝟙 _
| _, _, left _ _ => homOfLE inf_le_left
| _, _, right _ _ => homOfLE inf_le_right
