# 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 cannot 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`).

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

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

source
theorem CategoryTheory.types_hom {α β : Type u} :
(α ⟶ β) = (α → β)
source
theorem CategoryTheory.types_ext {α β : Type u} (f g : α ⟶ β) (h : ∀ (a : α), f a = g a) :
f = g
source
theorem CategoryTheory.types_ext_iff {α β : Type u} {f g : α ⟶ β} :
f = g ↔ ∀ (a : α), f a = g a
source
theorem CategoryTheory.types_id (X : Type u) :
CategoryStruct.id X = id
source
theorem CategoryTheory.types_comp {X Y Z : Type u} (f : X ⟶ Y) (g : Y ⟶ Z) :
CategoryStruct.comp f g = g ∘ f
source
@[simp]
theorem CategoryTheory.types_id_apply (X : Type u) (x : X) :
CategoryStruct.id X x = x
source
@[simp]
theorem CategoryTheory.types_comp_apply {X Y Z : Type u} (f : X ⟶ Y) (g : Y ⟶ Z) (x : X) :
CategoryStruct.comp f g x = g (f x)
source
@[simp]
theorem CategoryTheory.hom_inv_id_apply {X Y : Type u} (f : X ≅ Y) (x : X) :
f.inv (f.hom x) = x
source
@[simp]
theorem CategoryTheory.inv_hom_id_apply {X Y : Type u} (f : X ≅ Y) (y : Y) :
f.hom (f.inv y) = y
source
@[reducible, inline]
abbrev CategoryTheory.asHom {α β : Type u} (f : α → β) :
α ⟶ β

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

Equations

- CategoryTheory.asHom f = f

Instances For

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

Instances For

source
def CategoryTheory.Functor.sections {J : Type u} [Category.{v, u} J] (F : 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'}

Instances For

source
@[simp]
theorem CategoryTheory.Functor.sections_property {J : Type u} [Category.{v, u} J] {F : Functor J (Type w)} (s : ↑F.sections) {j j' : J} (f : j ⟶ j') :
F.map f (↑s j) = ↑s j'
source
theorem CategoryTheory.Functor.sections_ext_iff {J : Type u} [Category.{v, u} J] {F : Functor J (Type w)} {x y : ↑F.sections} :
x = y ↔ ∀ (j : J), ↑x j = ↑y j
source
def CategoryTheory.Functor.sectionsFunctor (J : Type u) [Category.{v, u} J] :
Functor (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.

Instances For

source
@[simp]
theorem CategoryTheory.Functor.sectionsFunctor_obj (J : Type u) [Category.{v, u} J] (F : Functor J (Type w)) :
(sectionsFunctor J).obj F = ↑F.sections
source
@[simp]
theorem CategoryTheory.Functor.sectionsFunctor_map_coe (J : Type u) [Category.{v, u} J] {F G : Functor J (Type w)} (φ : F ⟶ G) (x : ↑F.sections) (j : J) :
↑((sectionsFunctor J).map φ x) j = φ.app j (↑x j)
source
@[simp]
theorem CategoryTheory.FunctorToTypes.map_comp_apply {C : Type u} [Category.{v, u} C] (F : Functor C (Type w)) {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) (a : F.obj X) :
F.map (CategoryStruct.comp f g) a = F.map g (F.map f a)
source
@[simp]
theorem CategoryTheory.FunctorToTypes.map_id_apply {C : Type u} [Category.{v, u} C] (F : Functor C (Type w)) {X : C} (a : F.obj X) :
F.map (CategoryStruct.id X) a = a
source
theorem CategoryTheory.FunctorToTypes.naturality {C : Type u} [Category.{v, u} C] (F G : Functor C (Type w)) {X Y : C} (σ : F ⟶ G) (f : X ⟶ Y) (x : F.obj X) :
σ.app Y (F.map f x) = G.map f (σ.app X x)
source
@[simp]
theorem CategoryTheory.FunctorToTypes.comp {C : Type u} [Category.{v, u} C] (F G H : Functor C (Type w)) {X : C} (σ : F ⟶ G) (τ : G ⟶ H) (x : F.obj X) :
(CategoryStruct.comp σ τ).app X x = τ.app X (σ.app X x)
source
@[simp]
theorem CategoryTheory.FunctorToTypes.eqToHom_map_comp_apply {C : Type u} [Category.{v, u} C] (F : Functor C (Type w)) {X Y Z : C} (p : X = Y) (q : Y = Z) (x : F.obj X) :
F.map (eqToHom q) (F.map (eqToHom p) x) = F.map (eqToHom ⋯) x
source
@[simp]
theorem CategoryTheory.FunctorToTypes.hcomp {C : Type u} [Category.{v, u} C] (F G : Functor C (Type w)) (σ : F ⟶ G) {D : Type u'} [𝒟 : Category.{u', u'} D] (I J : 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)
source
@[simp]
theorem CategoryTheory.FunctorToTypes.map_inv_map_hom_apply {C : Type u} [Category.{v, u} C] (F : Functor C (Type w)) {X Y : C} (f : X ≅ Y) (x : F.obj X) :
F.map f.inv (F.map f.hom x) = x
source
@[simp]
theorem CategoryTheory.FunctorToTypes.map_hom_map_inv_apply {C : Type u} [Category.{v, u} C] (F : Functor C (Type w)) {X Y : C} (f : X ≅ Y) (y : F.obj Y) :
F.map f.hom (F.map f.inv y) = y
source
@[simp]
theorem CategoryTheory.FunctorToTypes.hom_inv_id_app_apply {C : Type u} [Category.{v, u} C] (F G : Functor C (Type w)) (α : F ≅ G) (X : C) (x : F.obj X) :
α.inv.app X (α.hom.app X x) = x
source
@[simp]
theorem CategoryTheory.FunctorToTypes.inv_hom_id_app_apply {C : Type u} [Category.{v, u} C] (F G : Functor C (Type w)) (α : F ≅ G) (X : C) (x : G.obj X) :
α.hom.app X (α.inv.app X x) = x
source
theorem CategoryTheory.FunctorToTypes.naturality_symm {C : Type u} [Category.{v, u} C] {F : Functor C (Type u_1)} {G : Functor C (Type u_2)} (e : (j : C) → F.obj j ≃ G.obj j) (naturality : ∀ {j j' : C} (f : j ⟶ j'), ⇑(e j') ∘ F.map f = G.map f ∘ ⇑(e j)) {j j' : C} (f : j ⟶ j') :
⇑(e j').symm ∘ G.map f = F.map f ∘ ⇑(e j).symm
source
def CategoryTheory.uliftTrivial (V : Type u) :
ULift.{u, u} V ≅ V

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

Equations

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

Instances For

source
def CategoryTheory.uliftFunctor :
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.

Instances For

source
@[simp]
theorem CategoryTheory.uliftFunctor_obj {X : Type u} :
uliftFunctor.{v, u}.obj X = ULift.{v, u} X
source
@[simp]
theorem CategoryTheory.uliftFunctor_map {X Y : Type u} (f : X ⟶ Y) (x : ULift.{v, u} X) :
uliftFunctor.{v, u}.map f x = { down := f x.down }
source
def CategoryTheory.fullyFaithfulULiftFunctor :
uliftFunctor.{v, u}.FullyFaithful

`uliftFunctor : Type u ⥤ Type max u v` is fully faithful.

Equations

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

Instances For

source
instance CategoryTheory.uliftFunctor_full :
uliftFunctor.{v, u}.Full
source
instance CategoryTheory.uliftFunctor_faithful :
uliftFunctor.{v, u}.Faithful
source
def CategoryTheory.uliftFunctorTrivial :
uliftFunctor.{u, u} ≅ 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

Instances For

source
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

Instances For

source
theorem CategoryTheory.homOfElement_eq_iff {X : Type u} (x y : X) :
homOfElement x = homOfElement y ↔ x = y
source
theorem CategoryTheory.mono_iff_injective {X Y : Type u} (f : X ⟶ Y) :
Mono f ↔ Function.Injective f

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

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

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

source
theorem CategoryTheory.surjective_of_epi {X Y : Type u} (f : X ⟶ Y) [hf : Epi f] :
Function.Surjective f
source
def CategoryTheory.ofTypeFunctor (m : Type u → Type v) [_root_.Functor m] [LawfulFunctor m] :
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.22} (f : X ⟶ Y) => Functor.map f, map_id := ⋯, map_comp := ⋯ }

Instances For

source
@[simp]
theorem CategoryTheory.ofTypeFunctor_obj (m : Type u → Type v) [_root_.Functor m] [LawfulFunctor m] :
(ofTypeFunctor m).obj = m
source
@[simp]
theorem CategoryTheory.ofTypeFunctor_map (m : Type u → Type v) [_root_.Functor m] [LawfulFunctor m] {α β : Type u} (f : α → β) :
(ofTypeFunctor m).map f = _root_.Functor.map f
source
def Equiv.toIso {X 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 := ⋯ }

Instances For

source
@[simp]
theorem Equiv.toIso_hom {X Y : Type u} {e : X ≃ Y} :
e.toIso.hom = ⇑e
source
@[simp]
theorem Equiv.toIso_inv {X Y : Type u} {e : X ≃ Y} :
e.toIso.inv = ⇑e.symm
source
def CategoryTheory.Iso.toEquiv {X 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

source
@[simp]
theorem CategoryTheory.Iso.toEquiv_fun {X Y : Type u} (i : X ≅ Y) :
⇑i.toEquiv = i.hom
source
@[simp]
theorem CategoryTheory.Iso.toEquiv_symm_fun {X Y : Type u} (i : X ≅ Y) :
⇑i.toEquiv.symm = i.inv
source
@[simp]
theorem CategoryTheory.Iso.toEquiv_id (X : Type u) :
(refl X).toEquiv = Equiv.refl X
source
@[simp]
theorem CategoryTheory.Iso.toEquiv_comp {X Y Z : Type u} (f : X ≅ Y) (g : Y ≅ Z) :
(f ≪≫ g).toEquiv = f.toEquiv.trans g.toEquiv
source
theorem CategoryTheory.isIso_iff_bijective {X Y : Type u} (f : X ⟶ Y) :
IsIso f ↔ Function.Bijective f

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

source
instance CategoryTheory.instSplitEpiCategoryType :
SplitEpiCategory (Type u)
source
theorem CategoryTheory.isSplitEpi_iff_surjective {X Y : Type u} (f : X ⟶ Y) :
IsSplitEpi f ↔ Function.Surjective f
source
def equivIsoIso {X 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 := ⋯ }

Instances For

source
@[simp]
theorem equivIsoIso_hom {X Y : Type u} (e : X ≃ Y) :
equivIsoIso.hom e = e.toIso
source
@[simp]
theorem equivIsoIso_inv {X Y : Type u} (i : X ≅ Y) :
equivIsoIso.inv i = i.toEquiv
source
def equivEquivIso {X 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

source
@[simp]
theorem equivEquivIso_hom {X Y : Type u} (e : X ≃ Y) :
equivEquivIso e = e.toIso
source
@[simp]
theorem equivEquivIso_inv {X Y : Type u} (e : X ≅ Y) :
equivEquivIso.symm e = e.toEquiv