Theorems · Theorem · category theory

CategoryTheory.Functor.initial_const_of_isInitial

∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [CategoryTheory.IsCofiltered C] {X : D} (hX : CategoryTheory.Limits.IsInitial X),
  ((CategoryTheory.Functor.const C).obj X).Initial

The inclusion of an initial object is initial.

Defined in

Mathlib.CategoryTheory.Filtered.Final

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.IsCofiltered