Codiscrete categories

We define Codiscrete A as an alias for the type A, and use this type alias to provide a Category instance whose Hom types are Unit.

Codiscrete.functor promotes a function f : C → A (for any category C) to a functor f : C ⥤ Codiscrete A.

Similarly, Codiscrete.natTrans and Codiscrete.natIso promote I-indexed families of morphisms, or I-indexed families of isomorphisms to natural transformations or natural isomorphisms.

We define functorToCat : Type u ⥤ Cat.{0,u} which sends a type to the codiscrete category and show it is right adjoint to Cat.objects.

structure CategoryTheory.Codiscrete (α : Type u) : Type u

A wrapper for promoting any type to a category, with a unique morphism between any two objects of the category.

• as : α

  A wrapper for promoting any type to a category, with a unique morphism between any two objects of the category.

theorem CategoryTheory.Codiscrete.ext_iff {α : Type u} {x y : Codiscrete α} : x = y ↔ x.as = y.as

theorem CategoryTheory.Codiscrete.ext {α : Type u} {x y : Codiscrete α} (as : x.as = y.as) : x = y

@[simp]

theorem CategoryTheory.Codiscrete.mk_as {α : Type u} (X : Codiscrete α) : { as := X.as } = X

def CategoryTheory.codiscreteEquiv {α : Type u} : Codiscrete α ≃ α

Codiscrete α is equivalent to the original type α.

Equations

• CategoryTheory.codiscreteEquiv = { toFun := CategoryTheory.Codiscrete.as, invFun := CategoryTheory.Codiscrete.mk, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem CategoryTheory.codiscreteEquiv_symm_apply_as {α : Type u} (as : α) : (codiscreteEquiv.symm as).as = as

@[simp]

theorem CategoryTheory.codiscreteEquiv_apply {α : Type u} (self : Codiscrete α) : codiscreteEquiv self = self.as

@[implicit_reducible]

instance CategoryTheory.instDecidableEqCodiscrete {α : Type u} [DecidableEq α] : DecidableEq (Codiscrete α)

Equations

• CategoryTheory.instDecidableEqCodiscrete = CategoryTheory.codiscreteEquiv.decidableEq

@[implicit_reducible]

instance CategoryTheory.Codiscrete.instCategory (A : Type u_1) : Category.{0, u_1} (Codiscrete A)

Equations

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

def CategoryTheory.Codiscrete.iso {A : Type u} (x y : Codiscrete A) : x ≅ y

Any two objects in a codiscrete category are isomorphic.

Equations

• x.iso y = { hom := (), inv := (), hom_inv_id := ⋯, inv_hom_id := ⋯ }

theorem CategoryTheory.Codiscrete.eq_id {A : Type u} {x : Codiscrete A} (f : x ⟶ x) : f = CategoryStruct.id x

theorem CategoryTheory.Codiscrete.eq_iso_hom {A : Type u} {x y : Codiscrete A} (f : x ⟶ y) : f = (x.iso y).hom

theorem CategoryTheory.Codiscrete.eq_iso_inv {A : Type u} {x y : Codiscrete A} (f : x ⟶ y) : f = (y.iso x).inv

@[implicit_reducible]

instance CategoryTheory.Codiscrete.uniqueHom {A : Type u} (x y : Codiscrete A) : Unique (x ⟶ y)

Equations

• x.uniqueHom y = { default := (x.iso y).hom, uniq := ⋯ }

@[simp]

theorem CategoryTheory.Codiscrete.uniqueHom_default {A : Type u} (x y : Codiscrete A) : default = (x.iso y).hom

@[implicit_reducible]

instance CategoryTheory.Codiscrete.uniqueIso {A : Type u} (x y : Codiscrete A) : Unique (x ≅ y)

Equations

• x.uniqueIso y = { default := x.iso y, uniq := ⋯ }

@[simp]

theorem CategoryTheory.Codiscrete.uniqueIso_default {A : Type u} (x y : Codiscrete A) : default = x.iso y

def CategoryTheory.Codiscrete.functor {C : Type u} [Category.{v, u} C] {A : Type w} (F : C → A) : Functor C (Codiscrete A)

Any function C → A lifts to a functor C ⥤ Codiscrete A.

Equations

• CategoryTheory.Codiscrete.functor F = { obj := CategoryTheory.Codiscrete.mk ∘ F, map := fun {X Y : C} (x : X ⟶ Y) => PUnit.unit, map_id := ⋯, map_comp := ⋯ }

def CategoryTheory.Codiscrete.invFunctor {C : Type u} [Category.{v, u} C] {A : Type w} (F : Functor C (Codiscrete A)) : C → A

The underlying function C → A of a functor C ⥤ Codiscrete A.

Equations

• CategoryTheory.Codiscrete.invFunctor F = CategoryTheory.Codiscrete.as ∘ F.obj

def CategoryTheory.Codiscrete.natTrans {C : Type u} [Category.{v, u} C] {A : Type w} {F G : Functor C (Codiscrete A)} : F ⟶ G

Given two functors to a codiscrete category, there is a trivial natural transformation.

Equations

• CategoryTheory.Codiscrete.natTrans = { app := fun (x : C) => PUnit.unit, naturality := ⋯ }

def CategoryTheory.Codiscrete.natIso {C : Type u} [Category.{v, u} C] {A : Type w} {F G : Functor C (Codiscrete A)} : F ≅ G

Given two functors into a codiscrete category, the trivial natural transformation is a natural isomorphism.

Equations

• CategoryTheory.Codiscrete.natIso = { hom := CategoryTheory.Codiscrete.natTrans, inv := CategoryTheory.Codiscrete.natTrans, hom_inv_id := ⋯, inv_hom_id := ⋯ }

def CategoryTheory.Codiscrete.natIsoFunctor {C : Type u} [Category.{v, u} C] {A : Type w} {F : Functor C (Codiscrete A)} : F ≅ functor (as ∘ F.obj)

Every functor F to a codiscrete category is naturally isomorphic (actually, equal) to Codiscrete.as ∘ F.obj.

Equations

• CategoryTheory.Codiscrete.natIsoFunctor = CategoryTheory.Iso.refl F

@[simp]

theorem CategoryTheory.Codiscrete.natIsoFunctor_inv_app {C : Type u} [Category.{v, u} C] {A : Type w} {F : Functor C (Codiscrete A)} (X : C) : natIsoFunctor.inv.app X = CategoryStruct.id (F.obj X)

@[simp]

theorem CategoryTheory.Codiscrete.natIsoFunctor_hom_app {C : Type u} [Category.{v, u} C] {A : Type w} {F : Functor C (Codiscrete A)} (X : C) : natIsoFunctor.hom.app X = CategoryStruct.id (F.obj X)

def CategoryTheory.Codiscrete.functorOfFun {A : Type u_1} {B : Type u_2} (f : A → B) : Functor (Codiscrete A) (Codiscrete B)

A function induces a functor between codiscrete categories.

Equations

• CategoryTheory.Codiscrete.functorOfFun f = CategoryTheory.Codiscrete.functor (f ∘ CategoryTheory.Codiscrete.as)

def CategoryTheory.Codiscrete.oppositeEquivalence (A : Type u_1) : (Codiscrete A)ᵒᵖ ≌ Codiscrete A

A codiscrete category is equivalent to its opposite category.

Equations

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

def CategoryTheory.Codiscrete.functorToCat : Functor (Type u) Cat

Codiscrete.functorToCat turns a type into a codiscrete category.

Equations

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

def CategoryTheory.Codiscrete.equivFunctorToCodiscrete {C : Type u} [Category.{v, u} C] {A : Type w} : (C → A) ≃ Functor C (Codiscrete A)

For a category C and type A, there is an equivalence between functions objects.obj C ⟶ A and functors C ⥤ Codiscrete A.

Equations

• CategoryTheory.Codiscrete.equivFunctorToCodiscrete = { toFun := CategoryTheory.Codiscrete.functor, invFun := CategoryTheory.Codiscrete.invFunctor, left_inv := ⋯, right_inv := ⋯ }

def CategoryTheory.Codiscrete.adj : Cat.objects ⊣ functorToCat

The functor that turns a type into a codiscrete category is right adjoint to the objects functor.

Equations

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

def CategoryTheory.Codiscrete.unitApp (C : Type u) [Category.{v, u} C] : Functor C (Codiscrete C)

Components of the unit of the adjunction Cat.objects ⊣ Codiscrete.functorToCat.

Equations

• CategoryTheory.Codiscrete.unitApp C = CategoryTheory.Codiscrete.functor id

def CategoryTheory.Codiscrete.counitApp (A : Type u) : Codiscrete A → A

Components of the counit of the adjunction Cat.objects ⊣ Codiscrete.functorToCat

Equations

• CategoryTheory.Codiscrete.counitApp A = CategoryTheory.Codiscrete.as

theorem CategoryTheory.Codiscrete.adj_unit_app (X : Cat) : adj.unit.app X = (unitApp ↑X).toCatHom

theorem CategoryTheory.Codiscrete.adj_counit_app (A : Type u) : adj.counit.app A = TypeCat.ofHom (counitApp A)

theorem CategoryTheory.Codiscrete.left_triangle_components (C : Type u) [Category.{v, u} C] : counitApp C ∘ (unitApp C).obj = id

Left triangle equality of the adjunction Cat.objects ⊣ Codiscrete.functorToCat, as a universe polymorphic statement.

theorem CategoryTheory.Codiscrete.right_triangle_components (X : Type u) : (unitApp (Codiscrete X)).comp (functorOfFun (counitApp X)) = Functor.id (Codiscrete X)

Right triangle equality of the adjunction Cat.objects ⊣ Codiscrete.functorToCat, stated using a composition of functors.