Documentation

Mathlib.CategoryTheory.Types

The category Type. #

In this section we set up the theory so that Lean's types and functions between them can be viewed as a LargeCategory in our framework.

Lean can not transparently view a function as a morphism in this category, and needs a hint in order to be able to type check. We provide the abbreviation asHom f to guide type checking, as well as a corresponding notation ↾ f. (Entered as \upr .)

We provide various simplification lemmas for functors and natural transformations valued in Type.

We define uliftFunctor, from Type u to Type (max u v), and show that it is fully faithful (but not, of course, essentially surjective).

We prove some basic facts about the category Type:

theorem CategoryTheory.types_hom {α : Type u} {β : Type u} :
(α β) = (αβ)
theorem CategoryTheory.types_ext {α : Type u} {β : Type u} (f : α β) (g : α β) (h : ∀ (a : α), f a = g a) :
f = g
theorem CategoryTheory.types_comp {X : Type u} {Y : Type u} {Z : Type u} (f : X Y) (g : Y Z) :
@[simp]
theorem CategoryTheory.types_comp_apply {X : Type u} {Y : Type u} {Z : Type u} (f : X Y) (g : Y Z) (x : X) :
@[simp]
theorem CategoryTheory.hom_inv_id_apply {X : Type u} {Y : Type u} (f : X Y) (x : X) :
f.inv (f.hom x) = x
@[simp]
theorem CategoryTheory.inv_hom_id_apply {X : Type u} {Y : Type u} (f : X Y) (y : Y) :
f.hom (f.inv y) = y
@[inline, reducible]
abbrev CategoryTheory.asHom {α : Type u} {β : Type u} (f : αβ) :
α β

asHom f helps Lean type check a function as a morphism in the category Type.

Equations
Instances For

    asHom f helps Lean type check a function as a morphism in the category Type.

    Equations
    Instances For

      The sections of a functor J ⥤ Type are the choices of a point u j : F.obj j for each j, such that F.map f (u j) = u j' for every morphism f : j ⟶ j'.

      We later use these to define limits in Type and in many concrete categories.

      Equations
      Instances For
        @[simp]
        theorem CategoryTheory.Functor.sections_property {J : Type u} [CategoryTheory.Category.{v, u} J] {F : CategoryTheory.Functor J (Type w)} (s : (CategoryTheory.Functor.sections F)) {j : J} {j' : J} (f : j j') :
        F.map f (s j) = s j'

        The functor which sends a functor to types to its sections.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          @[simp]
          theorem CategoryTheory.FunctorToTypes.map_comp_apply {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C (Type w)) {X : C} {Y : C} {Z : C} (f : X Y) (g : Y Z) (a : F.obj X) :
          F.map (CategoryTheory.CategoryStruct.comp f g) a = F.map g (F.map f a)
          theorem CategoryTheory.FunctorToTypes.naturality {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C (Type w)) (G : CategoryTheory.Functor C (Type w)) {X : C} {Y : C} (σ : F G) (f : X Y) (x : F.obj X) :
          σ.app Y (F.map f x) = G.map f (σ.app X x)
          @[simp]
          theorem CategoryTheory.FunctorToTypes.comp {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C (Type w)) (G : CategoryTheory.Functor C (Type w)) (H : CategoryTheory.Functor C (Type w)) {X : C} (σ : F G) (τ : G H) (x : F.obj X) :
          (CategoryTheory.CategoryStruct.comp σ τ).app X x = τ.app X (σ.app X x)
          @[simp]
          theorem CategoryTheory.FunctorToTypes.eqToHom_map_comp_apply {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C (Type w)) {X : C} {Y : C} {Z : C} (p : X = Y) (q : Y = Z) (x : F.obj X) :
          @[simp]
          theorem CategoryTheory.FunctorToTypes.hcomp {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C (Type w)) (G : CategoryTheory.Functor C (Type w)) (σ : F G) {D : Type u'} [𝒟 : CategoryTheory.Category.{u', u'} D] (I : CategoryTheory.Functor D C) (J : CategoryTheory.Functor D C) (ρ : I J) {W : D} (x : (CategoryTheory.Functor.comp I F).obj W) :
          (ρ σ).app W x = G.map (ρ.app W) (σ.app (I.obj W) x)
          @[simp]
          theorem CategoryTheory.FunctorToTypes.map_inv_map_hom_apply {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C (Type w)) {X : C} {Y : C} (f : X Y) (x : F.obj X) :
          F.map f.inv (F.map f.hom x) = x
          @[simp]
          theorem CategoryTheory.FunctorToTypes.map_hom_map_inv_apply {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C (Type w)) {X : C} {Y : C} (f : X Y) (y : F.obj Y) :
          F.map f.hom (F.map f.inv y) = y
          @[simp]
          theorem CategoryTheory.FunctorToTypes.hom_inv_id_app_apply {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C (Type w)) (G : CategoryTheory.Functor C (Type w)) (α : F G) (X : C) (x : F.obj X) :
          α.inv.app X (α.hom.app X x) = x
          @[simp]
          theorem CategoryTheory.FunctorToTypes.inv_hom_id_app_apply {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C (Type w)) (G : CategoryTheory.Functor C (Type w)) (α : F G) (X : C) (x : G.obj X) :
          α.hom.app X (α.inv.app X x) = x

          The isomorphism between a Type which has been ULifted to the same universe, and the original type.

          Equations
          Instances For

            The functor embedding Type u into Type (max u v). Write this as uliftFunctor.{5, 2} to get Type 2 ⥤ Type 5.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              @[simp]
              theorem CategoryTheory.uliftFunctor_map {X : Type u} {Y : Type u} (f : X Y) (x : ULift.{v, u} X) :
              CategoryTheory.uliftFunctor.{v, u} .map f x = { down := f x.down }
              Equations
              • One or more equations did not get rendered due to their size.

              Any term x of a type X corresponds to a morphism PUnit ⟶ X.

              Equations
              Instances For

                A morphism in Type is a monomorphism if and only if it is injective.

                See .

                A morphism in Type is an epimorphism if and only if it is surjective.

                See .

                ofTypeFunctor m converts from Lean's Type-based Category to CategoryTheory. This allows us to use these functors in category theory.

                Equations
                Instances For
                  @[simp]
                  theorem CategoryTheory.ofTypeFunctor_map (m : Type u → Type v) [Functor m] [LawfulFunctor m] {α : Type u} {β : Type u} (f : αβ) :
                  def Equiv.toIso {X : Type u} {Y : Type u} (e : X Y) :
                  X Y

                  Any equivalence between types in the same universe gives a categorical isomorphism between those types.

                  Equations
                  • Equiv.toIso e = { hom := e.toFun, inv := e.invFun, hom_inv_id := , inv_hom_id := }
                  Instances For
                    @[simp]
                    theorem Equiv.toIso_hom {X : Type u} {Y : Type u} {e : X Y} :
                    (Equiv.toIso e).hom = e
                    @[simp]
                    theorem Equiv.toIso_inv {X : Type u} {Y : Type u} {e : X Y} :
                    (Equiv.toIso e).inv = e.symm
                    def CategoryTheory.Iso.toEquiv {X : Type u} {Y : Type u} (i : X Y) :
                    X Y

                    Any isomorphism between types gives an equivalence.

                    Equations
                    • i.toEquiv = { toFun := i.hom, invFun := i.inv, left_inv := , right_inv := }
                    Instances For
                      @[simp]
                      theorem CategoryTheory.Iso.toEquiv_fun {X : Type u} {Y : Type u} (i : X Y) :
                      i.toEquiv = i.hom
                      @[simp]
                      theorem CategoryTheory.Iso.toEquiv_symm_fun {X : Type u} {Y : Type u} (i : X Y) :
                      i.symm = i.inv
                      @[simp]
                      theorem CategoryTheory.Iso.toEquiv_comp {X : Type u} {Y : Type u} {Z : Type u} (f : X Y) (g : Y Z) :
                      (f ≪≫ g).toEquiv = f.trans g.toEquiv

                      A morphism in Type u is an isomorphism if and only if it is bijective.

                      @[simp]
                      theorem equivIsoIso_hom {X : Type u} {Y : Type u} (e : X Y) :
                      equivIsoIso.hom e = Equiv.toIso e
                      @[simp]
                      theorem equivIsoIso_inv {X : Type u} {Y : Type u} (i : X Y) :
                      equivIsoIso.inv i = i.toEquiv
                      def equivIsoIso {X : Type u} {Y : Type u} :
                      X Y X Y

                      Equivalences (between types in the same universe) are the same as (isomorphic to) isomorphisms of types.

                      Equations
                      • equivIsoIso = { hom := fun (e : X Y) => Equiv.toIso e, inv := fun (i : X Y) => i.toEquiv, hom_inv_id := , inv_hom_id := }
                      Instances For
                        def equivEquivIso {X : Type u} {Y : Type u} :
                        X Y (X Y)

                        Equivalences (between types in the same universe) are the same as (equivalent to) isomorphisms of types.

                        Equations
                        • equivEquivIso = equivIsoIso.toEquiv
                        Instances For
                          @[simp]
                          theorem equivEquivIso_hom {X : Type u} {Y : Type u} (e : X Y) :
                          equivEquivIso e = Equiv.toIso e
                          @[simp]
                          theorem equivEquivIso_inv {X : Type u} {Y : Type u} (e : X Y) :
                          equivEquivIso.symm e = e.toEquiv