of_any_functor_const_on_obj — Mathlib

English

If every functor J ⥤ Discrete α is object-constant, then J is connected (assuming Nonempty J).

Русский

Если каждый функтор J ⥤ Discrete(α) константен на объектах, то J связен.

LaTeX

$$$[\\mathrm{Nonempty}(J)] \\Rightarrow (\\forall \\alpha, \\forall F: J \\to \\mathrm{Discrete}(\\alpha), \\forall j,j': J, F(j)=F(j')) \\Rightarrow \\operatorname{IsConnected}(J)$$$

Lean4

/-- If any functor to a discrete category is constant on objects, J is connected.
The converse of `any_functor_const_on_obj`.
-/
theorem of_any_functor_const_on_obj [Nonempty J]
    (h : ∀ {α : Type u₁} (F : J ⥤ Discrete α), ∀ j j' : J, F.obj j = F.obj j') : IsConnected J :=
  { IsPreconnected.of_any_functor_const_on_obj h with }

Похожие утверждения