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

instance CategoryTheory.types : CategoryTheory.LargeCategory (Type u)

Equations

• CategoryTheory.types = CategoryTheory.Category.mk @CategoryTheory.types.proof_1 @CategoryTheory.types.proof_1 @CategoryTheory.types.proof_2

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_id (X : Type u) : CategoryTheory.CategoryStruct.id X = id

theorem CategoryTheory.types_comp {X : Type u} {Y : Type u} {Z : Type u} (f : X ⟶ Y) (g : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp f g = g ∘ f

@[simp]

theorem CategoryTheory.types_id_apply (X : Type u) (x : X) : CategoryTheory.CategoryStruct.id 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 f g x = g (f 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

@[reducible, inline]

abbrev CategoryTheory.asHom {α : Type u} {β : Type u} (f : α → β) : α ⟶ β

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

Equations

• CategoryTheory.asHom f = f

def CategoryTheory.Functor.sections {J : Type u} [CategoryTheory.Category.{v, u} J] (F : CategoryTheory.Functor J (Type w)) : Set ((j : J) → F.obj j)

The sections of a functor F : 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

• F.sections = {u : (j : J) → F.obj j | ∀ {j j' : J} (f : j ⟶ j'), F.map f (u j) = u j'}

@[simp]

theorem CategoryTheory.Functor.sections_property {J : Type u} [CategoryTheory.Category.{v, u} J] {F : CategoryTheory.Functor J (Type w)} (s : ↑F.sections) {j : J} {j' : J} (f : j ⟶ j') : F.map f (↑s j) = ↑s j'

theorem CategoryTheory.Functor.sections_ext_iff {J : Type u} [CategoryTheory.Category.{v, u} J] {F : CategoryTheory.Functor J (Type w)} {x : ↑F.sections} {y : ↑F.sections} : x = y ↔ ∀ (j : J), ↑x j = ↑y j

def CategoryTheory.Functor.sectionsFunctor (J : Type u) [CategoryTheory.Category.{v, u} J] : CategoryTheory.Functor (CategoryTheory.Functor J (Type w)) (Type (max u w))

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

Equations

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

@[simp]

theorem CategoryTheory.Functor.sectionsFunctor_map_coe (J : Type u) [CategoryTheory.Category.{v, u} J] {F : CategoryTheory.Functor J (Type w)} {G : CategoryTheory.Functor J (Type w)} (φ : F ⟶ G) (x : ↑F.sections) (j : J) : ↑((CategoryTheory.Functor.sectionsFunctor J).map φ x) j = φ.app j (↑x j)

@[simp]

theorem CategoryTheory.Functor.sectionsFunctor_obj (J : Type u) [CategoryTheory.Category.{v, u} J] (F : CategoryTheory.Functor J (Type w)) : (CategoryTheory.Functor.sectionsFunctor J).obj F = ↑F.sections

@[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)

@[simp]

theorem CategoryTheory.FunctorToTypes.map_id_apply {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C (Type w)) {X : C} (a : F.obj X) : F.map (CategoryTheory.CategoryStruct.id X) a = 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) : F.map (CategoryTheory.eqToHom q) (F.map (CategoryTheory.eqToHom p) x) = F.map (CategoryTheory.eqToHom ⋯) 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 : (I.comp 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

def CategoryTheory.uliftTrivial (V : Type u) : ULift.{u, u} V ≅ V

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

Equations

• CategoryTheory.uliftTrivial V = { hom := fun (a : ULift.{?u.16, ?u.16} V) => a.down, inv := fun (a : V) => { down := a }, hom_inv_id := ⋯, inv_hom_id := ⋯ }

def CategoryTheory.uliftFunctor : CategoryTheory.Functor (Type u) (Type (max u v))

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.

@[simp]

theorem CategoryTheory.uliftFunctor_obj {X : Type u} : CategoryTheory.uliftFunctor.{v, u} .obj X = ULift.{v, u} X

@[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 }

instance CategoryTheory.uliftFunctor_full : CategoryTheory.uliftFunctor.{u_1, u} .Full

Equations

• CategoryTheory.uliftFunctor_full = ⋯

instance CategoryTheory.uliftFunctor_faithful : CategoryTheory.uliftFunctor.{u_2, u_1} .Faithful

Equations

• CategoryTheory.uliftFunctor_faithful = ⋯

def CategoryTheory.uliftFunctorTrivial : CategoryTheory.uliftFunctor.{u, u} ≅ CategoryTheory.Functor.id (Type u)

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

Equations

• CategoryTheory.uliftFunctorTrivial = CategoryTheory.NatIso.ofComponents CategoryTheory.uliftTrivial @CategoryTheory.uliftFunctorTrivial.proof_1

def CategoryTheory.homOfElement {X : Type u} (x : X) : PUnit.{u + 1} ⟶ X

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

Equations

• CategoryTheory.homOfElement x✝ x = x✝

theorem CategoryTheory.homOfElement_eq_iff {X : Type u} (x : X) (y : X) : CategoryTheory.homOfElement x = CategoryTheory.homOfElement y ↔ x = y

theorem CategoryTheory.mono_iff_injective {X : Type u} {Y : Type u} (f : X ⟶ Y) : CategoryTheory.Mono f ↔ Function.Injective f

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

See https://stacks.math.columbia.edu/tag/003C.

theorem CategoryTheory.injective_of_mono {X : Type u} {Y : Type u} (f : X ⟶ Y) [hf : CategoryTheory.Mono f] : Function.Injective f

theorem CategoryTheory.epi_iff_surjective {X : Type u} {Y : Type u} (f : X ⟶ Y) : CategoryTheory.Epi f ↔ Function.Surjective f

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

See https://stacks.math.columbia.edu/tag/003C.

theorem CategoryTheory.surjective_of_epi {X : Type u} {Y : Type u} (f : X ⟶ Y) [hf : CategoryTheory.Epi f] : Function.Surjective f

def CategoryTheory.ofTypeFunctor (m : Type u → Type v) [Functor m] [LawfulFunctor m] : CategoryTheory.Functor (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.

Equations

• CategoryTheory.ofTypeFunctor m = { obj := m, map := fun {X Y : Type ?u.28} (f : X ⟶ Y) => Functor.map f, map_id := ⋯, map_comp := ⋯ }

@[simp]

theorem CategoryTheory.ofTypeFunctor_obj (m : Type u → Type v) [Functor m] [LawfulFunctor m] : (CategoryTheory.ofTypeFunctor m).obj = m

@[simp]

theorem CategoryTheory.ofTypeFunctor_map (m : Type u → Type v) [Functor m] [LawfulFunctor m] {α : Type u} {β : Type u} (f : α → β) : (CategoryTheory.ofTypeFunctor m).map f = Functor.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.

Equations

• e.toIso = { hom := e.toFun, inv := e.invFun, hom_inv_id := ⋯, inv_hom_id := ⋯ }

@[simp]

theorem Equiv.toIso_hom {X : Type u} {Y : Type u} {e : X ≃ Y} : e.toIso.hom = ⇑e

@[simp]

theorem Equiv.toIso_inv {X : Type u} {Y : Type u} {e : X ≃ Y} : e.toIso.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 := ⋯ }

@[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.toEquiv.symm = i.inv

@[simp]

theorem CategoryTheory.Iso.toEquiv_id (X : Type u) : (CategoryTheory.Iso.refl X).toEquiv = Equiv.refl X

@[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.toEquiv.trans g.toEquiv

theorem CategoryTheory.isIso_iff_bijective {X : Type u} {Y : Type u} (f : X ⟶ Y) : CategoryTheory.IsIso f ↔ Function.Bijective f

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

instance CategoryTheory.instSplitEpiCategoryType : CategoryTheory.SplitEpiCategory (Type u)

Equations

• CategoryTheory.instSplitEpiCategoryType = ⋯

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) => e.toIso, inv := fun (i : X ≅ Y) => i.toEquiv, hom_inv_id := ⋯, inv_hom_id := ⋯ }

@[simp]

theorem equivIsoIso_inv {X : Type u} {Y : Type u} (i : X ≅ Y) : equivIsoIso.inv i = i.toEquiv

@[simp]

theorem equivIsoIso_hom {X : Type u} {Y : Type u} (e : X ≃ Y) : equivIsoIso.hom e = e.toIso

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

@[simp]

theorem equivEquivIso_hom {X : Type u} {Y : Type u} (e : X ≃ Y) : equivEquivIso e = e.toIso

@[simp]

theorem equivEquivIso_inv {X : Type u} {Y : Type u} (e : X ≅ Y) : equivEquivIso.symm e = e.toEquiv