English
The multispan index in the category corresponding to a complete lattice is defined by: left maps ⟨i,j⟩ ↦ v(i,j), right maps given by u, with fst and snd components coming from homOfLE, encoding the order relations.
Русский
Мультископическая индексная схема в категории, связанной сCompleteLattice, задаётся следующим образом: левая часть — v(i,j), правая — u, fst и snd — соответствуют гомоморфизмам по отношению к ≤.
LaTeX
$$$\\text{multispanIndex} := \\text{{ left := } (\\langle i,j \\rangle \\mapsto v\\,i\\,j),\\; right := u,\\; fst := \\mathrm{homOfLE}(\\text{by grind}),\\; snd := \\mathrm{homOfLE}(\\text{by grind})}}$$$
Lean4
/-- The multispan index in the category associated to the complete lattice `T`
given by the objects `u i` and the minima `v i j = u i ⊓ u j`,
when `d : MulticoequalizerDiagram x u v`. -/
@[simps]
def multispanIndex : MultispanIndex (.prod ι) T
where
left := fun ⟨i, j⟩ ↦ v i j
right := u
fst _ := homOfLE (by grind)
snd _ := homOfLE (by grind)
