of_any_functor_const_on_obj — Mathlib

English

If every functor to a discrete category is object-constant, then J is preconnected (assuming J is nonempty).

Русский

Если для любого функторы в дискретную категорию множество объектов константно, то J имеет свойство предсвязности (при непустоте J).

LaTeX

$$$[\\mathrm{Nonempty}(J)] \\Rightarrow \\big(\\forall \\alpha \\forall F: J \\to \\mathrm{Discrete}(\\alpha), \\forall j,j': J, F(j)=F(j')\\big) \\Rightarrow \\operatorname{IsPreconnected}(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 (h : ∀ {α : Type u₁} (F : J ⥤ Discrete α), ∀ j j' : J, F.obj j = F.obj j') :
    IsPreconnected J where iso_constant := fun F j' => ⟨NatIso.ofComponents fun j => eqToIso (h F j j')⟩

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