English
From a cone in Profinite, construct a functor from the opposite indexing category into a costructured arrow, via the extension.
Русский
Из конуса в Profinite строится объединённый функтор из противоположного индекса к CostructuredArrow через расширение.
LaTeX
$$$\\operatorname{functorOp}: I^{\\mathrm{op}}\\to \\mathrm{CostructuredArrow}\\;\\mathrm{toProfinite}^{\\mathrm{op}}$ with appropriate structure$$
Lean4
/-- Given a cone in `Profinite`, consisting of finite sets and indexed by a cofiltered category,
we obtain a functor from the opposite of the indexing category to
`CostructuredArrow toProfinite.op ⟨c.pt⟩`.
-/
@[simps! obj map]
def functorOp : Iᵒᵖ ⥤ CostructuredArrow toProfinite.op ⟨c.pt⟩ :=
(functor c).op ⋙
StructuredArrow.toCostructuredArrow _
_
-- We check that the opposite of the original diagram factors through `Profinite.Extend.functorOp`.
