Documentation

Mathlib.CategoryTheory.ObjectProperty.ColimitsCardinalClosure

Closure of a property of objects under colimits of bounded cardinality #

In this file, given P : ObjectProperty C and κ : Cardinal.{w}, we introduce the closure P.colimitsCardinalClosure κ of P under colimits of shapes given by categories J such that Arrow J is of cardinality < κ.

If C is locally w-small and P is essentially w-small, we show that this closure P.colimitsCardinalClosure κ is also essentially w-small.

source
def CategoryTheory.ObjectProperty.colimitsCardinalClosure {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) (κ : Cardinal.{w}) :
ObjectProperty C

Given P : ObjectProperty C and κ : Cardinal.{w}, this is the closure of P under colimits of shape given by categories J such that Arrow J is of cardinality < κ.

Equations
Instances For
    source
    theorem CategoryTheory.ObjectProperty.le_colimitsCardinalClosure {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) (κ : Cardinal.{w}) :
    P ≤ P.colimitsCardinalClosure κ
    source
    instance CategoryTheory.ObjectProperty.instIsClosedUnderIsomorphismsColimitsCardinalClosure {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) (κ : Cardinal.{w}) :
    (P.colimitsCardinalClosure κ).IsClosedUnderIsomorphisms
    source
    instance CategoryTheory.ObjectProperty.instEssentiallySmallColimitsCardinalClosureOfLocallySmall {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) (κ : Cardinal.{w}) [ObjectProperty.EssentiallySmall.{w, v, u} P] [LocallySmall.{w, v, u} C] :
    ObjectProperty.EssentiallySmall.{w, v, u} (P.colimitsCardinalClosure κ)
    source
    instance CategoryTheory.ObjectProperty.instIsClosedUnderColimitsOfShapeColimitsCardinalClosureCategoryFamily {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) (κ : Cardinal.{w}) (S : SmallCategoryCardinalLT κ) :
    (P.colimitsCardinalClosure κ).IsClosedUnderColimitsOfShape (SmallCategoryCardinalLT.categoryFamily κ S)
    source
    theorem CategoryTheory.ObjectProperty.isClosedUnderColimitsOfShape_colimitsCardinalClosure {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) (κ : Cardinal.{w}) (J : Type u') [Category.{v', u'} J] (hJ : HasCardinalLT (Arrow J) κ) :
    (P.colimitsCardinalClosure κ).IsClosedUnderColimitsOfShape J
    source
    theorem CategoryTheory.ObjectProperty.colimitsCardinalClosure_le {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) (κ : Cardinal.{w}) {Q : ObjectProperty C} [Q.IsClosedUnderIsomorphisms] (hQ : ∀ (J : Type w) [inst : SmallCategory J], HasCardinalLT (Arrow J) κ → Q.IsClosedUnderColimitsOfShape J) (h : P ≤ Q) :
    P.colimitsCardinalClosure κ ≤ Q
    source
    instance CategoryTheory.ObjectProperty.isStableUnderRetracts_colimitsCardinalClosure {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) (κ : Cardinal.{w}) [Fact κ.IsRegular] :
    (P.colimitsCardinalClosure κ).IsStableUnderRetracts