any_functor_const_on_obj — Mathlib

English

If J is preconnected, any functor from J to a discrete category is constant on objects.

Русский

Пусть J прочно сопряжена; каждый функтор J → Discrete(α) константен на объектах.

LaTeX

$$$\\operatorname{IsPreconnected}(J) \\Rightarrow \\forall \\alpha\\,,\\forall F: J \\to \\mathrm{Discrete}(\\alpha),\\forall j,j': J,\\ F(j)=F(j').$$$

Lean4

/-- If `J` is connected, any functor to a discrete category is constant on objects.
The converse is given in `IsConnected.of_any_functor_const_on_obj`.
-/
theorem any_functor_const_on_obj [IsPreconnected J] {α : Type u₂} (F : J ⥤ Discrete α) (j j' : J) :
    F.obj j = F.obj j' := by ext; exact ((isoConstant F j').hom.app j).down.1

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