English
Let J be a connected index category and C a category. For any X, Y in C, any natural transformation α: const_J X ⟶ const_J Y is pointwise constant: α_j = α_{j′} for all j, j′ in J.
Русский
Пусть J связан по индексу, и C — категория. Для любых X, Y ∈ C любая натуралная трансформация α: const_J X ⟶ const_J Y константна по всем индексам: α_j = α_{j′} для любых j, j′ ∈ J.
LaTeX
$$$ [IsPreconnected(J)] \\Rightarrow \\forall X,Y \\in C, \\forall \\alpha : (Const_J X) \\to (Const_J Y), \\forall j,j' : J, \\alpha_{j} = \\alpha_{j'}$$$
Lean4
/-- For objects `X Y : C`, any natural transformation `α : const X ⟶ const Y` from a connected
category must be constant.
This is the key property of connected categories which we use to establish properties about limits.
-/
theorem nat_trans_from_is_connected [IsPreconnected J] {X Y : C}
(α : (Functor.const J).obj X ⟶ (Functor.const J).obj Y) : ∀ j j' : J, α.app j = (α.app j' : X ⟶ Y) :=
@constant_of_preserves_morphisms _ _ _ (X ⟶ Y) (fun j => α.app j) fun _ _ f => by simpa using (α.naturality f).symm
