Smallness of a property of objects

In this file, given P : ObjectProperty C, we define ObjectProperty.Small.{w} P as an abbreviation for Small.{w} (Subtype P).

@[reducible, inline]

abbrev CategoryTheory.ObjectProperty.Small {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) : Prop

A property of objects is small relative to a universe w if the corresponding subtype is.

Equations

• CategoryTheory.ObjectProperty.Small.{?u.22, ?u.21, ?u.20} P = Small.{?u.22, ?u.20} (Subtype P)

instance CategoryTheory.ObjectProperty.instSmallFullSubcategoryOfSmall {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) [ObjectProperty.Small.{w, v, u} P] : Small.{w, u} P.FullSubcategory

theorem CategoryTheory.ObjectProperty.Small.of_le {C : Type u} [Category.{v, u} C] {P Q : ObjectProperty C} [ObjectProperty.Small.{w, v, u} Q] (h : P ≤ Q) : ObjectProperty.Small.{w, v, u} P

instance CategoryTheory.ObjectProperty.instSmallOppositeOp {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) [ObjectProperty.Small.{w, v, u} P] : ObjectProperty.Small.{w, v, u} P.op

instance CategoryTheory.ObjectProperty.instSmallUnopOfOpposite {C : Type u} [Category.{v, u} C] (P : ObjectProperty Cᵒᵖ) [ObjectProperty.Small.{w, v, u} P] : ObjectProperty.Small.{w, v, u} P.unop

instance CategoryTheory.ObjectProperty.instSmallOfObjOfSmall {C : Type u} [Category.{v, u} C] {ι : Type u_1} (X : ι → C) [Small.{w, u_1} ι] : ObjectProperty.Small.{w, v, u} (ofObj X)

instance CategoryTheory.ObjectProperty.instSmallPair {C : Type u} [Category.{v, u} C] (X Y : C) : ObjectProperty.Small.{w, v, u} (pair X Y)

instance CategoryTheory.ObjectProperty.instSmallMin {C : Type u} [Category.{v, u} C] {P Q : ObjectProperty C} [ObjectProperty.Small.{w, v, u} Q] : ObjectProperty.Small.{w, v, u} (P ⊓ Q)

instance CategoryTheory.ObjectProperty.instSmallMin_1 {C : Type u} [Category.{v, u} C] {P Q : ObjectProperty C} [ObjectProperty.Small.{w, v, u} P] : ObjectProperty.Small.{w, v, u} (P ⊓ Q)

instance CategoryTheory.ObjectProperty.instSmallMax {C : Type u} [Category.{v, u} C] {P Q : ObjectProperty C} [ObjectProperty.Small.{w, v, u} P] [ObjectProperty.Small.{w, v, u} Q] : ObjectProperty.Small.{w, v, u} (P ⊔ Q)

instance CategoryTheory.ObjectProperty.instSmallISupOfSmall {C : Type u} [Category.{v, u} C] {α : Type u_1} (P : α → ObjectProperty C) [∀ (a : α), ObjectProperty.Small.{w, v, u} (P a)] [Small.{w, u_1} α] : ObjectProperty.Small.{w, v, u} (⨆ (a : α), P a)

class CategoryTheory.ObjectProperty.EssentiallySmall {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) : Prop

A property of objects is essentially small relative to a universe w if it is contained in the closure by isomorphisms of a small property.

• exists_small_le' : ∃ (Q : ObjectProperty C) (_ : ObjectProperty.Small.{w, v, u} Q), P ≤ Q.isoClosure

theorem CategoryTheory.ObjectProperty.EssentiallySmall.exists_small_le {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) [ObjectProperty.EssentiallySmall.{w, v, u} P] : ∃ (Q : ObjectProperty C) (_ : ObjectProperty.Small.{w, v, u} Q), Q ≤ P ∧ P ≤ Q.isoClosure

instance CategoryTheory.ObjectProperty.instEssentiallySmallOfSmall {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) [ObjectProperty.Small.{w, v, u} P] : ObjectProperty.EssentiallySmall.{w, v, u} P

instance CategoryTheory.ObjectProperty.instEssentiallySmallIsoClosure {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) [ObjectProperty.EssentiallySmall.{w, v, u} P] : ObjectProperty.EssentiallySmall.{w, v, u} P.isoClosure

theorem CategoryTheory.ObjectProperty.EssentiallySmall.exists_small {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) [P.IsClosedUnderIsomorphisms] [ObjectProperty.EssentiallySmall.{w, v, u} P] : ∃ (P₀ : ObjectProperty C) (_ : ObjectProperty.Small.{w, v, u} P₀), P = P₀.isoClosure

theorem CategoryTheory.ObjectProperty.EssentiallySmall.of_le {C : Type u} [Category.{v, u} C] {P Q : ObjectProperty C} [ObjectProperty.EssentiallySmall.{w, v, u} Q] (h : P ≤ Q) : ObjectProperty.EssentiallySmall.{w, v, u} P

instance CategoryTheory.ObjectProperty.instEssentiallySmallMax {C : Type u} [Category.{v, u} C] {P Q : ObjectProperty C} [ObjectProperty.EssentiallySmall.{w, v, u} P] [ObjectProperty.EssentiallySmall.{w, v, u} Q] : ObjectProperty.EssentiallySmall.{w, v, u} (P ⊔ Q)

instance CategoryTheory.ObjectProperty.instEssentiallySmallISupOfSmall {C : Type u} [Category.{v, u} C] {α : Type u_1} (P : α → ObjectProperty C) [∀ (a : α), ObjectProperty.EssentiallySmall.{w, v, u} (P a)] [Small.{w, u_1} α] : ObjectProperty.EssentiallySmall.{w, v, u} (⨆ (a : α), P a)