Documentation

Mathlib.CategoryTheory.CodiscreteCategory

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 type are Unit types.

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

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

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

  • as : α

    A wrapper for promoting any type to a category, with a unique morphisms 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

Codiscrete α is equivalent to the original type α.

Equations
@[simp]
Equations
  • One or more equations did not get rendered due to their size.
def CategoryTheory.Codiscrete.functor {C : Type u} [Category.{v, u} C] {A : Type w} (F : CA) :

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

Equations

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

Equations

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

Equations

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

Equations

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

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

A function induces a functor between codiscrete categories.

Equations

A codiscrete category is equivalent to its opposite category.

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

Codiscrete.functorToCat turns a type into a codiscrete category.

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

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

Equations

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.

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

Equations

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

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