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.

Instances For
    theorem CategoryTheory.Codiscrete.ext {α : Type u} {x : CategoryTheory.Codiscrete α} {y : CategoryTheory.Codiscrete α} (as : x.as = y.as) :
    x = y
    @[simp]
    theorem CategoryTheory.Codiscrete.mk_as {α : Type u} (X : CategoryTheory.Codiscrete α) :
    { as := X.as } = X

    Codiscrete α is equivalent to the original type α.

    Equations
    • CategoryTheory.codiscreteEquiv = { toFun := CategoryTheory.Codiscrete.as, invFun := CategoryTheory.Codiscrete.mk, left_inv := , right_inv := }
    Instances For
      @[simp]
      theorem CategoryTheory.codiscreteEquiv_apply {α : Type u} (self : CategoryTheory.Codiscrete α) :
      CategoryTheory.codiscreteEquiv self = self.as
      @[simp]
      theorem CategoryTheory.codiscreteEquiv_symm_apply_as {α : Type u} (as : α) :
      (CategoryTheory.codiscreteEquiv.symm as).as = as
      Equations
      • CategoryTheory.instDecidableEqCodiscrete = CategoryTheory.codiscreteEquiv.decidableEq

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

      Equations
      Instances For

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

        Equations
        Instances For

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

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

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

            Equations
            • CategoryTheory.Codiscrete.natIso = { hom := CategoryTheory.Codiscrete.natTrans, inv := CategoryTheory.Codiscrete.natTrans, hom_inv_id := , inv_hom_id := }
            Instances For

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

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

                A function induces a functor between codiscrete categories.

                Equations
                Instances For

                  A codiscrete category is equivalent to its opposite category.

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

                    Codiscrete.functorToCat turns a type into a codiscrete category

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

                      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 := }
                      Instances For

                        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.
                        Instances For

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

                          Equations
                          Instances For

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