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

• epimorphisms are surjections and monomorphisms are injections,
• Iso is both Iso and Equiv to Equiv (at least within a fixed universe),
• every type level IsLawfulFunctor gives a categorical functor Type ⥤ Type (the corresponding fact about monads is in Mathlib/CategoryTheory/Monad/Types.lean).
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_id_apply (X : Type u) (x : X) :
CategoryTheory.CategoryStruct.id (Type u) CategoryTheory.Category.toCategoryStruct X x = x
@[simp]
theorem CategoryTheory.types_comp_apply {X : Type u} {Y : Type u} {Z : Type u} (f : X Y) (g : Y Z) (x : X) :
CategoryTheory.CategoryStruct.comp (Type u) CategoryTheory.Category.toCategoryStruct X Y Z f g x = g (f x)
@[simp]
theorem CategoryTheory.hom_inv_id_apply {X : Type u} {Y : Type u} (f : X Y) (x : X) :
Type u.inv CategoryTheory.types X Y f (Type u.hom CategoryTheory.types X Y f x) = x
@[simp]
theorem CategoryTheory.inv_hom_id_apply {X : Type u} {Y : Type u} (f : X Y) (y : Y) :
Type u.hom CategoryTheory.types X Y f (Type u.inv CategoryTheory.types X Y f 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.

Instances For

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

Instances For
def CategoryTheory.Functor.sections {J : Type u} (F : ) :
Set ((j : J) → F.obj j)

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.

Instances For
@[simp]
theorem CategoryTheory.Functor.sections_property {J : Type u} {F : } (s : ) {j : J} {j' : J} (f : j j') :
J.map CategoryTheory.CategoryStruct.toQuiver (Type w) CategoryTheory.CategoryStruct.toQuiver F.toPrefunctor j j' f (s j) = s j'
@[simp]
theorem CategoryTheory.FunctorToTypes.map_comp_apply {C : Type u} (F : ) {X : C} {Y : C} {Z : C} (f : X Y) (g : Y Z) (a : F.obj X) :
C.map CategoryTheory.CategoryStruct.toQuiver (Type w) CategoryTheory.CategoryStruct.toQuiver F.toPrefunctor X Z () a = C.map CategoryTheory.CategoryStruct.toQuiver (Type w) CategoryTheory.CategoryStruct.toQuiver F.toPrefunctor Y Z g (C.map CategoryTheory.CategoryStruct.toQuiver (Type w) CategoryTheory.CategoryStruct.toQuiver F.toPrefunctor X Y f a)
@[simp]
theorem CategoryTheory.FunctorToTypes.map_id_apply {C : Type u} (F : ) {X : C} (a : F.obj X) :
C.map CategoryTheory.CategoryStruct.toQuiver (Type w) CategoryTheory.CategoryStruct.toQuiver F.toPrefunctor X X () a = a
theorem CategoryTheory.FunctorToTypes.naturality {C : Type u} (F : ) (G : ) {X : C} {Y : C} (σ : F G) (f : X Y) (x : F.obj X) :
C.app inst✝ (Type w) CategoryTheory.types F G σ Y (C.map CategoryTheory.CategoryStruct.toQuiver (Type w) CategoryTheory.CategoryStruct.toQuiver F.toPrefunctor X Y f x) = C.map CategoryTheory.CategoryStruct.toQuiver (Type w) CategoryTheory.CategoryStruct.toQuiver G.toPrefunctor X Y f (C.app inst✝ (Type w) CategoryTheory.types F G σ X x)
@[simp]
theorem CategoryTheory.FunctorToTypes.comp {C : Type u} (F : ) (G : ) (H : ) {X : C} (σ : F G) (τ : G H) (x : F.obj X) :
C.app inst✝ (Type w) CategoryTheory.types F H () X x = C.app inst✝ (Type w) CategoryTheory.types G H τ X (C.app inst✝ (Type w) CategoryTheory.types F G σ X x)
@[simp]
theorem CategoryTheory.FunctorToTypes.hcomp {C : Type u} (F : ) (G : ) (σ : F G) {D : Type u'} [𝒟 : ] (I : ) (J : ) (ρ : I J) {W : D} (x : ().obj W) :
D.app 𝒟 (Type w) CategoryTheory.types () () (ρ σ) W x = C.map CategoryTheory.CategoryStruct.toQuiver (Type w) CategoryTheory.CategoryStruct.toQuiver G.toPrefunctor (I.obj W) (J.obj W) (ρ.app W) (C.app inst✝ (Type w) CategoryTheory.types F G σ (I.obj W) x)
@[simp]
theorem CategoryTheory.FunctorToTypes.map_inv_map_hom_apply {C : Type u} (F : ) {X : C} {Y : C} (f : X Y) (x : F.obj X) :
C.map CategoryTheory.CategoryStruct.toQuiver (Type w) CategoryTheory.CategoryStruct.toQuiver F.toPrefunctor Y X f.inv (C.map CategoryTheory.CategoryStruct.toQuiver (Type w) CategoryTheory.CategoryStruct.toQuiver F.toPrefunctor X Y f.hom x) = x
@[simp]
theorem CategoryTheory.FunctorToTypes.map_hom_map_inv_apply {C : Type u} (F : ) {X : C} {Y : C} (f : X Y) (y : F.obj Y) :
C.map CategoryTheory.CategoryStruct.toQuiver (Type w) CategoryTheory.CategoryStruct.toQuiver F.toPrefunctor X Y f.hom (C.map CategoryTheory.CategoryStruct.toQuiver (Type w) CategoryTheory.CategoryStruct.toQuiver F.toPrefunctor Y X f.inv y) = y
@[simp]
theorem CategoryTheory.FunctorToTypes.hom_inv_id_app_apply {C : Type u} (F : ) (G : ) (α : F G) (X : C) (x : F.obj X) :
C.app inst✝ (Type w) CategoryTheory.types G F α.inv X (C.app inst✝ (Type w) CategoryTheory.types F G α.hom X x) = x
@[simp]
theorem CategoryTheory.FunctorToTypes.inv_hom_id_app_apply {C : Type u} (F : ) (G : ) (α : F G) (X : C) (x : G.obj X) :
C.app inst✝ (Type w) CategoryTheory.types F G α.hom X (C.app inst✝ (Type w) CategoryTheory.types G F α.inv X x) = x

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

Instances For

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

Instances For
@[simp]
theorem CategoryTheory.uliftFunctor_map {X : Type u} {Y : Type u} (f : X Y) (x : ) :
= { down := f x.down }

The functor embedding Type u into Type u via ULift is isomorphic to the identity functor.

Instances For
def CategoryTheory.homOfElement {X : Type u} (x : X) :

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

Instances For
theorem CategoryTheory.homOfElement_eq_iff {X : Type u} (x : X) (y : X) :
theorem CategoryTheory.mono_iff_injective {X : Type u} {Y : Type u} (f : X Y) :

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

theorem CategoryTheory.injective_of_mono {X : Type u} {Y : Type u} (f : X Y) [hf : ] :
theorem CategoryTheory.epi_iff_surjective {X : Type u} {Y : Type u} (f : X Y) :

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

theorem CategoryTheory.surjective_of_epi {X : Type u} {Y : Type u} (f : X Y) [hf : ] :
def CategoryTheory.ofTypeFunctor (m : Type u → Type v) [] [] :

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

Instances For
@[simp]
theorem CategoryTheory.ofTypeFunctor_obj (m : Type u → Type v) [] [] :
().toPrefunctor.obj = m
@[simp]
theorem CategoryTheory.ofTypeFunctor_map (m : Type u → Type v) [] [] {α : Type u} {β : Type u} (f : αβ) :
().map 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.

Instances For
@[simp]
theorem Equiv.toIso_hom {X : Type u} {Y : Type u} {e : X Y} :
().hom = e
@[simp]
theorem Equiv.toIso_inv {X : Type u} {Y : Type u} {e : X Y} :
().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.

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_id (X : Type u) :
().toEquiv =
@[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
theorem CategoryTheory.isIso_iff_bijective {X : Type u} {Y : Type u} (f : X Y) :

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

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.

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