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

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

• CategoryTheory.Functor.sections F = {u : (j : J) → F.toPrefunctor.obj j | ∀ {j j' : J} (f : j ⟶ j'), F.toPrefunctor.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 : ↑(CategoryTheory.Functor.sections F)) {j : J} {j' : J} (f : j ⟶ j') : F.toPrefunctor.map f (↑s j) = ↑s j'

@[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 : ↑(CategoryTheory.Functor.sections F)) (j : J) : ↑((CategoryTheory.Functor.sectionsFunctor J).toPrefunctor.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).toPrefunctor.obj F = ↑(CategoryTheory.Functor.sections F)

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.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.toPrefunctor.obj X) : F.toPrefunctor.map (CategoryTheory.CategoryStruct.comp f g) a = F.toPrefunctor.map g (F.toPrefunctor.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.toPrefunctor.obj X) : F.toPrefunctor.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.toPrefunctor.obj X) : σ.app Y (F.toPrefunctor.map f x) = G.toPrefunctor.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.toPrefunctor.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.toPrefunctor.obj X) : F.toPrefunctor.map (CategoryTheory.eqToHom q) (F.toPrefunctor.map (CategoryTheory.eqToHom p) x) = F.toPrefunctor.map (CategoryTheory.eqToHom (_ : X = Z)) 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).toPrefunctor.obj W) : (ρ ◫ σ).app W x = G.toPrefunctor.map (ρ.app W) (σ.app (I.toPrefunctor.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.toPrefunctor.obj X) : F.toPrefunctor.map f.inv (F.toPrefunctor.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.toPrefunctor.obj Y) : F.toPrefunctor.map f.hom (F.toPrefunctor.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.toPrefunctor.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.toPrefunctor.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 = CategoryTheory.Iso.mk (fun (a : ULift.{u, u} V) => a.down) fun (a : V) => { 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

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

@[simp]

theorem CategoryTheory.uliftFunctor_map {X : Type u} {Y : Type u} (f : X ⟶ Y) (x : ULift.{v, u} X) : CategoryTheory.uliftFunctor.{v, u} .toPrefunctor.map f x = { down := f x.down }

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

Equations

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

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

Equations

• CategoryTheory.uliftFunctor_faithful = (_ : CategoryTheory.Faithful CategoryTheory.uliftFunctor.{u_2, u_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 .

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 .

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 : Type u} (f : X ⟶ Y) => 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).toPrefunctor.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.SplitEpiCategory (Type u))

@[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 : X ≃ Y) => Equiv.toIso e) fun (i : X ≅ Y) => 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