Closure of a property of objects under limits of certain shapes

In this file, given a property P of objects in a category C and family of categories J : α → Type _, we introduce the closure P.limitsClosure J of P under limits of shapes J a for all a : α, and under certain smallness assumptions, we show that its essentially small.

inductive CategoryTheory.ObjectProperty.limitsClosure {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) {α : Type t} (J : α → Type u') [(a : α) → Category.{v', u'} (J a)] : ObjectProperty C

The closure of a property of objects of a category under limits of shape J a for a family of categories J.

• of_mem {C : Type u} [Category.{v, u} C] {P : ObjectProperty C} {α : Type t} {J : α → Type u'} [(a : α) → Category.{v', u'} (J a)] (X : C) (hX : P X) : P.limitsClosure J X
• of_isoClosure {C : Type u} [Category.{v, u} C] {P : ObjectProperty C} {α : Type t} {J : α → Type u'} [(a : α) → Category.{v', u'} (J a)] {X Y : C} (e : X ≅ Y) (hX : P.limitsClosure J X) : P.limitsClosure J Y
• of_limitPresentation {C : Type u} [Category.{v, u} C] {P : ObjectProperty C} {α : Type t} {J : α → Type u'} [(a : α) → Category.{v', u'} (J a)] {X : C} {a : α} (pres : Limits.LimitPresentation (J a) X) (h : ∀ (j : J a), P.limitsClosure J (pres.diag.obj j)) : P.limitsClosure J X

@[simp]

theorem CategoryTheory.ObjectProperty.le_limitsClosure {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) {α : Type t} (J : α → Type u') [(a : α) → Category.{v', u'} (J a)] : P ≤ P.limitsClosure J

instance CategoryTheory.ObjectProperty.instIsClosedUnderIsomorphismsLimitsClosure {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) {α : Type t} (J : α → Type u') [(a : α) → Category.{v', u'} (J a)] : (P.limitsClosure J).IsClosedUnderIsomorphisms

instance CategoryTheory.ObjectProperty.instIsClosedUnderLimitsOfShapeLimitsClosure {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) {α : Type t} (J : α → Type u') [(a : α) → Category.{v', u'} (J a)] (a : α) : (P.limitsClosure J).IsClosedUnderLimitsOfShape (J a)

theorem CategoryTheory.ObjectProperty.limitsClosure_le {C : Type u} [Category.{v, u} C] {P : ObjectProperty C} {α : Type t} {J : α → Type u'} [(a : α) → Category.{v', u'} (J a)] {Q : ObjectProperty C} [Q.IsClosedUnderIsomorphisms] [∀ (a : α), Q.IsClosedUnderLimitsOfShape (J a)] (h : P ≤ Q) : P.limitsClosure J ≤ Q

theorem CategoryTheory.ObjectProperty.limitsClosure_monotone {C : Type u} [Category.{v, u} C] {P : ObjectProperty C} {α : Type t} (J : α → Type u') [(a : α) → Category.{v', u'} (J a)] {Q : ObjectProperty C} (h : P ≤ Q) : P.limitsClosure J ≤ Q.limitsClosure J

theorem CategoryTheory.ObjectProperty.limitsClosure_isoClosure {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) {α : Type t} (J : α → Type u') [(a : α) → Category.{v', u'} (J a)] : P.isoClosure.limitsClosure J = P.limitsClosure J

def CategoryTheory.ObjectProperty.strictLimitsClosureStep {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) {α : Type t} (J : α → Type u') [(a : α) → Category.{v', u'} (J a)] : ObjectProperty C

Given P : ObjectProperty C and a family of categories J : α → Type _, this property objects contains P and all objects that are equal to lim F for some functor F : J a ⥤ C such that F.obj j satisfies P for any j.

Equations

• P.strictLimitsClosureStep J = P ⊔ ⨆ (a : α), P.strictLimitsOfShape (J a)

@[simp]

theorem CategoryTheory.ObjectProperty.le_strictLimitsClosureStep {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) {α : Type t} (J : α → Type u') [(a : α) → Category.{v', u'} (J a)] : P ≤ P.strictLimitsClosureStep J

theorem CategoryTheory.ObjectProperty.strictLimitsClosureStep_monotone {C : Type u} [Category.{v, u} C] {P : ObjectProperty C} {α : Type t} (J : α → Type u') [(a : α) → Category.{v', u'} (J a)] {Q : ObjectProperty C} (h : P ≤ Q) : P.strictLimitsClosureStep J ≤ Q.strictLimitsClosureStep J

@[reducible, inline]

abbrev CategoryTheory.ObjectProperty.strictLimitsClosureIter {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) {α : Type t} (J : α → Type u') [(a : α) → Category.{v', u'} (J a)] {β : Type w'} [LinearOrder β] [SuccOrder β] [WellFoundedLT β] (b : β) : ObjectProperty C

Given P : ObjectProperty C, a family of categories J a, this is the transfinite iteration of Q ↦ Q.strictLimitsClosureStep J.

Equations

• P.strictLimitsClosureIter J b = transfiniteIterate (fun (Q : CategoryTheory.ObjectProperty C) => Q.strictLimitsClosureStep J) b P

theorem CategoryTheory.ObjectProperty.le_strictLimitsClosureIter {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) {α : Type t} (J : α → Type u') [(a : α) → Category.{v', u'} (J a)] {β : Type w'} [LinearOrder β] [OrderBot β] [SuccOrder β] [WellFoundedLT β] (b : β) : P ≤ P.strictLimitsClosureIter J b

theorem CategoryTheory.ObjectProperty.strictLimitsClosureIter_le_limitsClosure {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) {α : Type t} (J : α → Type u') [(a : α) → Category.{v', u'} (J a)] {β : Type w'} [LinearOrder β] [OrderBot β] [SuccOrder β] [WellFoundedLT β] (b : β) : P.strictLimitsClosureIter J b ≤ P.limitsClosure J

instance CategoryTheory.ObjectProperty.instSmallStrictLimitsClosureIterOfLocallySmallOfSmallElemIio {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) {α : Type t} (J : α → Type u') [(a : α) → Category.{v', u'} (J a)] {β : Type w'} [LinearOrder β] [OrderBot β] [SuccOrder β] [WellFoundedLT β] [ObjectProperty.Small.{w, v, u} P] [LocallySmall.{w, v, u} C] [Small.{w, t} α] [∀ (a : α), Small.{w, u'} (J a)] [∀ (a : α), LocallySmall.{w, v', u'} (J a)] (b : β) [hb₀ : Small.{w, w'} ↑(Set.Iio b)] : ObjectProperty.Small.{w, v, u} (P.strictLimitsClosureIter J b)

theorem CategoryTheory.ObjectProperty.strictLimitsClosureStep_strictLimitsClosureIter_eq_self {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) {α : Type t} (J : α → Type u') [(a : α) → Category.{v', u'} (J a)] (κ : Cardinal.{w}) [Fact κ.IsRegular] (h : ∀ (a : α), HasCardinalLT (J a) κ) : (P.strictLimitsClosureIter J κ.ord).strictLimitsClosureStep J = P.strictLimitsClosureIter J κ.ord

theorem CategoryTheory.ObjectProperty.isoClosure_strictLimitsClosureIter_eq_limitsClosure {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) {α : Type t} (J : α → Type u') [(a : α) → Category.{v', u'} (J a)] (κ : Cardinal.{w}) [Fact κ.IsRegular] (h : ∀ (a : α), HasCardinalLT (J a) κ) : (P.strictLimitsClosureIter J κ.ord).isoClosure = P.limitsClosure J

theorem CategoryTheory.ObjectProperty.isEssentiallySmall_limitsClosure {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) {α : Type t} (J : α → Type u') [(a : α) → Category.{v', u'} (J a)] (κ : Cardinal.{w}) [Fact κ.IsRegular] (h : ∀ (a : α), HasCardinalLT (J a) κ) [ObjectProperty.EssentiallySmall.{w, v, u} P] [LocallySmall.{w, v, u} C] [Small.{w, t} α] [∀ (a : α), Small.{w, u'} (J a)] [∀ (a : α), LocallySmall.{w, v', u'} (J a)] : ObjectProperty.EssentiallySmall.{w, v, u} (P.limitsClosure J)

instance CategoryTheory.ObjectProperty.instEssentiallySmallLimitsClosureOfSmallOfLocallySmall {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) {α : Type t} (J : α → Type u') [(a : α) → Category.{v', u'} (J a)] [ObjectProperty.EssentiallySmall.{w, v, u} P] [LocallySmall.{w, v, u} C] [Small.{w, t} α] [∀ (a : α), Small.{w, u'} (J a)] [∀ (a : α), LocallySmall.{w, v', u'} (J a)] : ObjectProperty.EssentiallySmall.{w, v, u} (P.limitsClosure J)