English
The morphism part of the index functor is defined by restricting precomposition along the inclusion h, and reindexing the elements accordingly.
Русский
Часть отображения функтору индекса задана как ограничение предкомпоновки вдоль включения h и перенумерацией элементов.
LaTeX
$$$\\mathrm{map}\;h : C(obj\,C\,K, obj\,C\,J) = \\langle \\mathrm{Set.MapsTo.restrict}(\\mathrm{precomp}(\\mathrm{Set.inclusion}\\;h))\\, \\_', \\mathrm{Continuous.restrict}\\_\\rangle$$$
Lean4
/-- The morphism part of the functor `indexFunctor : (Finset ι)ᵒᵖ ⥤ Profinite`. -/
def map (h : ∀ i, J i → K i) : C(obj C K, obj C J) :=
⟨Set.MapsTo.restrict (precomp (Set.inclusion h)) _ _
(fun _ hx ↦ by
obtain ⟨y, hy⟩ := hx
rw [← hy.2]
exact ⟨y, hy.1, rfl⟩),
Continuous.restrict _ (Pi.continuous_precomp' _)⟩
