Theorems · Definition · category theory

CategoryTheory.SolutionSetCondition

{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {D : Type u₁} → [inst_1 : CategoryTheory.Category.{v₁, u₁} D] → CategoryTheory.Functor D C → Prop

The functor G : D ⥤ C satisfies the solution set condition if for every A : C, there is a family of morphisms {f_i : A ⟶ G (B_i) // i ∈ ι} such that given any morphism h : A ⟶ G X, there is some i ∈ ι such that h factors through f_i. The key part of this definition is that the indexing set ι lives in Type v, where v is the universe of morphisms of the category: this is the "smallness" condition which allows the general adjoint functor theorem to go through.

Defined in

Mathlib.CategoryTheory.Adjunction.AdjointFunctorTheorems

Cited by

2 results in Mathlib

Foundations

Depth 4 from the axioms · uses no axioms

Assumes

CategoryTheory.CategoryCategoryTheory.Category