English
There is a natural bijection between functions from the connected components of J to a set X and functors J → Discrete X. The bijection is given by taking a function on components to a functor that is constant on components, with explicit inverses described by representatives of the components.
Русский
Существуют естественная bi-екция между отображениями от связных компонент J в X и функторaми J → Discrete X. Биекция задаётся отображением функции на компоненты в соответствующий константный функтор по компонентам и обратной картиной через представителя каждой компоненты.
LaTeX
$$$ (\\mathrm{ConnectedComponents}\\ J \\to X) \\ \simeq \ (J \\;\\to\\; \\mathrm{Discrete}\; X) $$$
Lean4
/-- Functions from connected components and functors to discrete category are in bijection -/
def typeToCatHomEquiv (J) [Category J] (X : Type*) : (ConnectedComponents J → X) ≃ (J ⥤ Discrete X)
where
toFun := ConnectedComponents.functorToDiscrete _
invFun := ConnectedComponents.liftFunctor _
left_inv
f :=
funext fun x ↦ by
obtain ⟨x, h⟩ := Quotient.exists_rep x
rw [← h]
rfl
right_inv
fctr :=
Functor.hext (fun _ ↦ rfl)
(fun c d f ↦
have : Subsingleton (fctr.obj c ⟶ fctr.obj d) := Discrete.instSubsingletonDiscreteHom _ _
(Subsingleton.elim (fctr.map f) _).symm.heq)
