Documentation

Mathlib.CategoryTheory.Presentable.IsDiscrete

Presentable objects in discrete categories #

The purpose of this file is to show that a category with a single object and a single morphism is locally presentable.

source
@[instance 100]
instance CategoryTheory.IsDiscrete.isCardinalPresentable {C : Type u_1} [Category.{v_1, u_1} C] [IsDiscrete C] (X : C) (κ : Cardinal.{w}) [Fact κ.IsRegular] :
IsCardinalPresentable X κ
source
@[instance 100]
instance CategoryTheory.IsDiscrete.isCardinalAccessible {C : Type u_1} [Category.{v_1, u_1} C] [IsDiscrete C] {D : Type u_2} [Category.{v_2, u_2} D] (F : Functor C D) (κ : Cardinal.{w}) [Fact κ.IsRegular] :
F.IsCardinalAccessible κ
source
@[instance 100]
instance CategoryTheory.IsDiscrete.isAccessible {C : Type u_1} [Category.{v_1, u_1} C] [IsDiscrete C] {D : Type u_2} [Category.{v_2, u_2} D] (F : Functor C D) :
Functor.IsAccessible.{w, v_1, v_2, u_1, u_2} F
source
@[instance 100]
instance CategoryTheory.IsDiscrete.instIsCardinalLocallyPresentableOfSubsingletonOfNonempty {C : Type u_1} [Category.{v_1, u_1} C] [IsDiscrete C] (κ : Cardinal.{w}) [Fact κ.IsRegular] [Subsingleton C] [Nonempty C] :
IsCardinalLocallyPresentable C κ
source
@[instance 100]
instance CategoryTheory.IsDiscrete.instIsLocallyPresentableOfSubsingletonOfNonempty {C : Type u_1} [Category.{v_1, u_1} C] [IsDiscrete C] [Subsingleton C] [Nonempty C] :
IsLocallyPresentable.{w, v_1, u_1} C