Representatives of small categories

Given a type Ω : Type w, we construct a structure SmallCategoryOfSet Ω : Type w which consists of the data and axioms that allows to define a category structure such that the type of objects and morphisms identify to subtypes of Ω.

This allows to define a small family of small categories SmallCategoryOfSet.categoryFamily : SmallCategoryOfSet Ω → Type w which, up to equivalence, represents all categories such that types of objects and morphisms have cardinalities less than or equal to that of Ω (see SmallCategoryOfSet.exists_equivalence).

Given a cardinal κ : Cardinal.{w}, we also provide a small family of categories SmallCategoryCardinalLT.categoryFamily κ which represents (up to isomorphism) any category C such that HasCardinalLT C κ holds.

structure CategoryTheory.SmallCategoryOfSet (Ω : Type w) : Type w

Structure which allows to construct a category whose types of objects and morphisms are subtypes of a fixed type Ω.

• obj : Set Ω

  objects

• hom (X Y : ↑self.obj) : Set Ω

  morphisms

• id (X : ↑self.obj) : ↑(self.hom X X)

  identity morphisms

• comp {X Y Z : ↑self.obj} (f : ↑(self.hom X Y)) (g : ↑(self.hom Y Z)) : ↑(self.hom X Z)

  the composition of morphisms

• id_comp {X Y : ↑self.obj} (f : ↑(self.hom X Y)) : self.comp (self.id X) f = f
• comp_id {X Y : ↑self.obj} (f : ↑(self.hom X Y)) : self.comp f (self.id Y) = f
• assoc {X Y Z T : ↑self.obj} (f : ↑(self.hom X Y)) (g : ↑(self.hom Y Z)) (h : ↑(self.hom Z T)) : self.comp (self.comp f g) h = self.comp f (self.comp g h)

instance CategoryTheory.SmallCategoryOfSet.instSmallCategoryElemObj (Ω : Type w) (S : SmallCategoryOfSet Ω) : SmallCategory ↑S.obj

@[simp]

theorem CategoryTheory.SmallCategoryOfSet.comp_def (Ω : Type w) (S : SmallCategoryOfSet Ω) {X✝ Y✝ Z✝ : ↑S.obj} (f : ↑(S.hom X✝ Y✝)) (g : ↑(S.hom Y✝ Z✝)) : CategoryStruct.comp f g = S.comp f g

@[simp]

theorem CategoryTheory.SmallCategoryOfSet.id_def (Ω : Type w) (S : SmallCategoryOfSet Ω) (X : ↑S.obj) : CategoryStruct.id X = S.id X

@[reducible, inline]

abbrev CategoryTheory.SmallCategoryOfSet.categoryFamily (Ω : Type w) : SmallCategoryOfSet Ω → Type w

The family of all categories such that the types of objects and morphisms are subtypes of a given type Ω.

structure CategoryTheory.CoreSmallCategoryOfSet (Ω : Type w) (C : Type u) [Category.{v, u} C] : Type (max (max u v) w)

Helper structure for the construction of a term in SmallCategoryOfSet. This involves the choice of bijections between types of objects and morphisms in a category C and subtypes of a type Ω.

• obj : Set Ω

  objects

• hom (X Y : ↑self.obj) : Set Ω

  morphisms

• objEquiv : ↑self.obj ≃ C

  a bijection between the types of objects

• homEquiv {X Y : ↑self.obj} : ↑(self.hom X Y) ≃ (self.objEquiv X ⟶ self.objEquiv Y)

  a bijection between the types of morphisms

def CategoryTheory.CoreSmallCategoryOfSet.smallCategoryOfSet {Ω : Type w} {C : Type u} [Category.{v, u} C] (h : CoreSmallCategoryOfSet Ω C) : SmallCategoryOfSet Ω

The SmallCategoryOfSet structure induced by a CoreSmallCategoryOfSet structure.

@[simp]

theorem CategoryTheory.CoreSmallCategoryOfSet.smallCategoryOfSet_id {Ω : Type w} {C : Type u} [Category.{v, u} C] (h : CoreSmallCategoryOfSet Ω C) (X : ↑h.obj) : h.smallCategoryOfSet.id X = h.homEquiv.symm (CategoryStruct.id (h.objEquiv X))

@[simp]

theorem CategoryTheory.CoreSmallCategoryOfSet.smallCategoryOfSet_hom {Ω : Type w} {C : Type u} [Category.{v, u} C] (h : CoreSmallCategoryOfSet Ω C) (X Y : ↑h.obj) : h.smallCategoryOfSet.hom X Y = h.hom X Y

@[simp]

theorem CategoryTheory.CoreSmallCategoryOfSet.smallCategoryOfSet_comp {Ω : Type w} {C : Type u} [Category.{v, u} C] (h : CoreSmallCategoryOfSet Ω C) {X✝ Y✝ Z✝ : ↑h.obj} (f : ↑(h.hom X✝ Y✝)) (g : ↑(h.hom Y✝ Z✝)) : h.smallCategoryOfSet.comp f g = h.homEquiv.symm (CategoryStruct.comp (h.homEquiv f) (h.homEquiv g))

@[simp]

theorem CategoryTheory.CoreSmallCategoryOfSet.smallCategoryOfSet_obj {Ω : Type w} {C : Type u} [Category.{v, u} C] (h : CoreSmallCategoryOfSet Ω C) : h.smallCategoryOfSet.obj = h.obj

def CategoryTheory.CoreSmallCategoryOfSet.functor {Ω : Type w} {C : Type u} [Category.{v, u} C] (h : CoreSmallCategoryOfSet Ω C) : Functor (↑h.smallCategoryOfSet.obj) C

Given h : CoreSmallCategoryOfSet Ω C, this is the obvious functor h.smallCategoryOfSet.obj ⥤ C.

@[simp]

theorem CategoryTheory.CoreSmallCategoryOfSet.functor_obj {Ω : Type w} {C : Type u} [Category.{v, u} C] (h : CoreSmallCategoryOfSet Ω C) (a : ↑h.obj) : h.functor.obj a = h.objEquiv a

@[simp]

theorem CategoryTheory.CoreSmallCategoryOfSet.functor_map {Ω : Type w} {C : Type u} [Category.{v, u} C] (h : CoreSmallCategoryOfSet Ω C) {X✝ Y✝ : ↑h.smallCategoryOfSet.obj} (a : ↑(h.hom X✝ Y✝)) : h.functor.map a = h.homEquiv a

def CategoryTheory.CoreSmallCategoryOfSet.fullyFaithfulFunctor {Ω : Type w} {C : Type u} [Category.{v, u} C] (h : CoreSmallCategoryOfSet Ω C) : h.functor.FullyFaithful

Given h : CoreSmallCategoryOfSet Ω C, the obvious functor h.smallCategoryOfSet.obj ⥤ C is fully faithful.

instance CategoryTheory.CoreSmallCategoryOfSet.instIsEquivalenceElemObjSmallCategoryOfSetFunctor {Ω : Type w} {C : Type u} [Category.{v, u} C] (h : CoreSmallCategoryOfSet Ω C) : h.functor.IsEquivalence

noncomputable def CategoryTheory.CoreSmallCategoryOfSet.equivalence {Ω : Type w} {C : Type u} [Category.{v, u} C] (h : CoreSmallCategoryOfSet Ω C) : ↑h.smallCategoryOfSet.obj ≌ C

Given h : CoreSmallCategoryOfSet Ω C, the obvious functor h.smallCategoryOfSet.obj ⥤ C is an equivalence.

noncomputable def CategoryTheory.CoreSmallCategoryOfSet.arrowEquiv {Ω : Type w} {C : Type u} [Category.{v, u} C] (h : CoreSmallCategoryOfSet Ω C) : Arrow ↑h.smallCategoryOfSet.obj ≃ Arrow C

Given h : CoreSmallCategoryOfSet Ω C, the equivalence of categories h.smallCategoryOfSet.obj ≌ C is actually an isomorphism: it induces a bijection on the type of arrows.

theorem CategoryTheory.SmallCategoryOfSet.exists_equivalence (Ω : Type w) (C : Type u) [Category.{v, u} C] (h₁ : Cardinal.lift.{w, u} (Cardinal.mk C) ≤ Cardinal.lift.{u, w} (Cardinal.mk Ω)) (h₂ : ∀ (X Y : C), Cardinal.lift.{w, v} (Cardinal.mk (X ⟶ Y)) ≤ Cardinal.lift.{v, w} (Cardinal.mk Ω)) : ∃ (h : SmallCategoryOfSet Ω), Nonempty (categoryFamily Ω h ≌ C)

def CategoryTheory.SmallCategoryCardinalLT (κ : Cardinal.{w}) : Type w

Index set of a representative set of all categories C which satisfy HasCardinalLT C κ, see SmallCategoryCardinalLT.categoryFamily.

@[reducible, inline]

abbrev CategoryTheory.SmallCategoryCardinalLT.categoryFamily (κ : Cardinal.{w}) (S : SmallCategoryCardinalLT κ) : Type w

Given a cardinal κ, this is a representative family of all categories C such that HasCardinalLT C κ.

theorem CategoryTheory.SmallCategoryCardinalLT.hasCardinalLT (κ : Cardinal.{w}) (S : SmallCategoryCardinalLT κ) : HasCardinalLT (Arrow (categoryFamily κ S)) κ

theorem CategoryTheory.SmallCategoryCardinalLT.exists_equivalence (κ : Cardinal.{w}) (C : Type u) [Category.{v, u} C] (hC : HasCardinalLT (Arrow C) κ) : ∃ (S : SmallCategoryCardinalLT κ), Nonempty (categoryFamily κ S ≌ C)