Theorems · Theorem · category theory

CategoryTheory.any_functor_const_on_obj

∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] [CategoryTheory.IsPreconnected J] {α : Type u₂}
  (F : CategoryTheory.Functor J (CategoryTheory.Discrete α)) (j j' : J), F.obj j = F.obj j'

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.

Defined in

Mathlib.CategoryTheory.IsConnected

Cited by

1 results in Mathlib

Foundations

Depth 29 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.IsPreconnected