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).

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

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

@[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

@[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 Ω.

Equations

• CategoryTheory.SmallCategoryOfSet.categoryFamily Ω S = ↑S.obj

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.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

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

@[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_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

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.

Equations

• h.functor = { obj := ⇑h.objEquiv, map := fun {X Y : ↑h.smallCategoryOfSet.obj} => ⇑h.homEquiv, map_id := ⋯, map_comp := ⋯ }

@[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

@[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

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.

Equations

• h.fullyFaithfulFunctor = { preimage := fun {X Y : ↑h.smallCategoryOfSet.obj} => ⇑h.homEquiv.symm, map_preimage := ⋯, preimage_map := ⋯ }

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.

Equations

• h.equivalence = h.functor.asEquivalence

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)