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.

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)

@[simp]

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

@[simp]

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

instance CategoryTheory.ObjectProperty.instSmallOppositeOp_1 {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_1 {C : Type u} [Category.{v, u} C] (P : ObjectProperty Cᵒᵖ) [ObjectProperty.Small.{w, v, u} P] : ObjectProperty.Small.{w, v, u} P.unop

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)

@[simp]

theorem CategoryTheory.ObjectProperty.essentiallySmall_op_iff {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) : ObjectProperty.EssentiallySmall.{w, v, u} P.op ↔ ObjectProperty.EssentiallySmall.{w, v, u} P

@[simp]

theorem CategoryTheory.ObjectProperty.essentiallySmall_unop_iff {C : Type u} [Category.{v, u} C] (P : ObjectProperty Cᵒᵖ) : ObjectProperty.EssentiallySmall.{w, v, u} P.unop ↔ ObjectProperty.EssentiallySmall.{w, v, u} P

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

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

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

instance CategoryTheory.ObjectProperty.instEssentiallySmallTopOfEssentiallySmall {C : Type u} [Category.{v, u} C] [EssentiallySmall.{w, v, u} C] : ObjectProperty.EssentiallySmall.{w, v, u} ⊤

instance CategoryTheory.ObjectProperty.instSmallStrictMap {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] (P : ObjectProperty C) [ObjectProperty.Small.{w, v, u} P] (F : Functor C D) : ObjectProperty.Small.{w, v', u'} (P.strictMap F)

instance CategoryTheory.ObjectProperty.instEssentiallySmallMap {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] (P : ObjectProperty C) [ObjectProperty.EssentiallySmall.{w, v, u} P] (F : Functor C D) : ObjectProperty.EssentiallySmall.{w, v', u'} (P.map F)

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

theorem CategoryTheory.ObjectProperty.exists_equivalence_iff {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) [LocallySmall.{w', v, u} C] : (∃ (J : Type w) (x : Category.{w', w} J), Nonempty (P.FullSubcategory ≌ J)) ↔ ObjectProperty.EssentiallySmall.{w, v, u} P

theorem CategoryTheory.exists_equivalence_iff_of_locallySmall (C : Type u) [Category.{v, u} C] [LocallySmall.{w', v, u} C] : (∃ (J : Type w) (x : Category.{w', w} J), Nonempty (C ≌ J)) ↔ ObjectProperty.EssentiallySmall.{w, v, u} ⊤