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

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

Equations

• CategoryTheory.asHom f = f

def CategoryTheory.«term↾_» : Lean.ParserDescr

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

Equations

• CategoryTheory.«term↾_» = Lean.ParserDescr.node `CategoryTheory.term↾_ 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "↾") (Lean.ParserDescr.cat `term 200))

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

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

@[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') : 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} [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) : C.map CategoryTheory.CategoryStruct.toQuiver (Type w) CategoryTheory.CategoryStruct.toQuiver F.toPrefunctor X Z (CategoryTheory.CategoryStruct.comp f g) 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} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C (Type w)) {X : C} (a : F.obj X) : C.map CategoryTheory.CategoryStruct.toQuiver (Type w) CategoryTheory.CategoryStruct.toQuiver F.toPrefunctor X X (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) : 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} [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) : C.app inst✝ (Type w) CategoryTheory.types F H (CategoryTheory.CategoryStruct.comp σ τ) 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} [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) : D.app 𝒟 (Type w) CategoryTheory.types (CategoryTheory.Functor.comp I F) (CategoryTheory.Functor.comp J G) (ρ ◫ σ) 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} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C (Type w)) {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} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C (Type w)) {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} [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) : 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} [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) : C.app inst✝ (Type w) CategoryTheory.types F G α.hom X (C.app inst✝ (Type w) CategoryTheory.types G F α.inv 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 = CategoryTheory.Iso.mk (fun a => a.down) fun a => { down := a }

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

• CategoryTheory.uliftFunctor.{v, u} = CategoryTheory.Functor.mk { obj := fun X => ULift.{v, u} X, map := fun {X Y} f x => { down := f x.down } }

@[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.uliftFunctorFull : CategoryTheory.Full CategoryTheory.uliftFunctor.{u_1, u}

Equations

• CategoryTheory.uliftFunctorFull = CategoryTheory.Full.mk fun {X Y} f x => (f { down := x }).down

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

Equations

• CategoryTheory.uliftFunctor_faithful = CategoryTheory.uliftFunctor_faithful.proof_1

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

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 = CategoryTheory.Functor.mk { obj := m, map := fun {X Y} f => Functor.map f }

@[simp]

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

• Equiv.toIso e = CategoryTheory.Iso.mk e.toFun e.invFun

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

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

@[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) : (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.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.instSplitEpiCategoryTypeTypes : CategoryTheory.SplitEpiCategory (Type u)

Equations

• CategoryTheory.instSplitEpiCategoryTypeTypes = CategoryTheory.instSplitEpiCategoryTypeTypes.proof_1

@[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 = CategoryTheory.Iso.mk (fun e => Equiv.toIso e) fun i => i.toEquiv

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 = Equiv.toIso e

@[simp]

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