Theorems · Theorem · category theory

CategoryTheory.hasInitial_of_isCoseparating

∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.LocallySmall.{w, v₁, u₁} C]
  [CategoryTheory.WellPowered.{w, v₁, u₁} C] [CategoryTheory.Limits.HasLimitsOfSize.{w, w, v₁, u₁} C]
  {P : CategoryTheory.ObjectProperty C} [CategoryTheory.ObjectProperty.Small.{w, v₁, u₁} P],
  P.IsCoseparating → CategoryTheory.Limits.HasInitial C

An ingredient of the proof of the Special Adjoint Functor Theorem: a complete well-powered category with a small coseparating set has an initial object. In fact, it follows from the Special Adjoint Functor Theorem that C is already cocomplete, see hasColimits_of_hasLimits_of_isCoseparating.

Defined in

Mathlib.CategoryTheory.Generator.Basic

Cited by

2 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.LocallySmallCategoryTheory.WellPoweredCategoryTheory.Limits.HasLimitsOfSizeCategoryTheory.ObjectProperty.Small