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.3, ?u.2, ?u.1} P = Small.{?u.3, ?u.1} (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

theorem CategoryTheory.ObjectProperty.Small.exists_eq_ofObj {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) [ObjectProperty.Small.{w, v, u} P] : ∃ (ι : Type w) (X : ι → C), P = ofObj X

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.exists_eq_isoClosure_ofObj {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) [P.IsClosedUnderIsomorphisms] [ObjectProperty.EssentiallySmall.{w, v, u} P] : ∃ (ι : Type w) (X : ι → C), P = (ofObj X).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.instEssentiallySmallEssImageOfEssentiallySmall {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] [EssentiallySmall.{w, v, u} C] (F : Functor C D) : ObjectProperty.EssentiallySmall.{w, v', u'} F.essImage

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.EssentiallySmall.of_functor {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] (P : ObjectProperty C) (F : Functor C D) (H₁ : ObjectProperty.EssentiallySmall.{w, v', u'} (P.map F)) (H₂ : ∀ (Y : D), ObjectProperty.EssentiallySmall.{w, v, u} (P ⊓ fun (x : C) => Nonempty (F.obj x ≅ Y))) : ObjectProperty.EssentiallySmall.{w, v, u} P

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_1} [Category.{v_1, u_1} C] [LocallySmall.{w', v_1, u_1} C] : (∃ (J : Type w) (x : Category.{w', w} J), Nonempty (C ≌ J)) ↔ ObjectProperty.EssentiallySmall.{w, v_1, u_1} ⊤

theorem CategoryTheory.essentiallySmall_iff_objectPropertyEssentiallySmall_top (C : Type u) [Category.{v, u} C] [LocallySmall.{w, v, u} C] : EssentiallySmall.{w, v, u} C ↔ ObjectProperty.EssentiallySmall.{w, v, u} ⊤

theorem CategoryTheory.essentiallySmall_iff_objectPropertyEssentiallySmall {C : Type u_1} [Category.{v_1, u_1} C] : EssentiallySmall.{w, v_1, u_1} C ↔ LocallySmall.{w, v_1, u_1} C ∧ ObjectProperty.EssentiallySmall.{w, v_1, u_1} ⊤

theorem CategoryTheory.EssentiallySmall.of_functor {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] (F : Functor C D) [LocallySmall.{w, v_1, u_1} C] (H₁ : ObjectProperty.EssentiallySmall.{w, v_2, u_2} F.essImage) (H₂ : ∀ (Y : D), ObjectProperty.EssentiallySmall.{w, v_1, u_1} fun (x : C) => Nonempty (F.obj x ≅ Y)) : EssentiallySmall.{w, v_1, u_1} C