English
A sequential cone in LightProfinite of finite sets yields a functor from Nat^op to StructuredArrow.
Русский
Последовательное конусов LightProfinite над конечными множествами порождает функтор из Nat^op в StructuredArrow.
LaTeX
$$$\mathrm{LightProfinite.Extend.functor} : \mathbb{N}^{op} \to \mathrm{StructuredArrow}(c.pt,\mathrm{toLightProfinite})$$$
Lean4
/-- Given a sequential cone in `LightProfinite` consisting of finite sets,
we obtain a functor from the indexing category to `StructuredArrow c.pt toLightProfinite`.
-/
@[simps]
def functor : ℕᵒᵖ ⥤ StructuredArrow c.pt toLightProfinite
where
obj i := StructuredArrow.mk (c.π.app i)
map
f :=
StructuredArrow.homMk (F.map f)
(c.w f)
-- We check that the original diagram factors through `LightProfinite.Extend.functor`.
