English
The sequentialFunctor is a canonical functor from N^op to J, with object part given by sequentialFunctor_obj J and map part given by sequentialFunctor_map.
Русский
Последовательный функтор — каноничный функтор из \\mathbb{N}^{op} в J, на котором объектная часть задана sequentialFunctorObj, а отображение — sequentialFunctorMap.
LaTeX
$$$ \\text{sequentialFunctor } J : \\mathbb{N}^{op} \\to J,\\; \\text{obj}(n) = \\text{sequentialFunctor\\_obj } J n,\\; \\text{map}(h) = \\text{homOfLE}( \\text{sequentialFunctor\\_map }(J,h)) $$$
Lean4
/-- The initial functor `ℕᵒᵖ ⥤ J`, which allows us to turn cofiltered limits over countable preorders
into sequential limits.
TODO: redefine this as `(IsFiltered.sequentialFunctor Jᵒᵖ).leftOp`. This would need API for initial/
final functors of the form `leftOp`/`rightOp`.
-/
noncomputable def sequentialFunctor : ℕᵒᵖ ⥤ J
where
obj n := sequentialFunctor_obj J (unop n)
map h := homOfLE (sequentialFunctor_map J (leOfHom h.unop))
