mathlib documentation

category_theory.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 large_category 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 as_hom 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 ulift_functor, 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:

@[instance]

Equations
theorem category_theory.types_hom {α β : Type u} :
β) = (α → β)

theorem category_theory.types_id (X : Type u) :

theorem category_theory.types_comp {X Y Z : Type u} (f : X Y) (g : Y Z) :
f g = g f

@[simp]
theorem category_theory.types_id_apply (X : Type u) (x : X) :
𝟙 X x = x

@[simp]
theorem category_theory.types_comp_apply {X Y Z : Type u} (f : X Y) (g : Y Z) (x : X) :
(f g) x = g (f x)

@[simp]
theorem category_theory.hom_inv_id_apply {X Y : Type u} (f : X Y) (x : X) :
f.inv (f.hom x) = x

@[simp]
theorem category_theory.inv_hom_id_apply {X Y : Type u} (f : X Y) (y : Y) :
f.hom (f.inv y) = y

def category_theory.as_hom {α β : Type u} :
(α → β) β)

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

def category_theory.functor.sections {J : Type u} [category_theory.category J] (F : 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
@[simp]
theorem category_theory.functor_to_types.map_comp_apply {C : Type u} [category_theory.category C] (F : C Type w) {X Y Z : C} (f : X Y) (g : Y Z) (a : F.obj X) :
F.map (f g) a = F.map g (F.map f a)

@[simp]
theorem category_theory.functor_to_types.map_id_apply {C : Type u} [category_theory.category C] (F : C Type w) {X : C} (a : F.obj X) :
F.map (𝟙 X) a = a

theorem category_theory.functor_to_types.naturality {C : Type u} [category_theory.category C] (F G : 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)

@[simp]
theorem category_theory.functor_to_types.comp {C : Type u} [category_theory.category C] (F G H : C Type w) {X : C} (σ : F G) (τ : G H) (x : F.obj X) :
τ).app X x = τ.app X (σ.app X x)

@[simp]
theorem category_theory.functor_to_types.hcomp {C : Type u} [category_theory.category C] (F G : C Type w) (σ : F G) {D : Type u'} [𝒟 : category_theory.category D] (I J : D C) (ρ : I J) {W : D} (x : (I F).obj W) :
σ).app W x = G.map (ρ.app W) (σ.app (I.obj W) x)

@[simp]
theorem category_theory.functor_to_types.map_inv_map_hom_apply {C : Type u} [category_theory.category C] (F : C Type w) {X Y : C} (f : X Y) (x : F.obj X) :
F.map f.inv (F.map f.hom x) = x

@[simp]
theorem category_theory.functor_to_types.map_hom_map_inv_apply {C : Type u} [category_theory.category C] (F : C Type w) {X Y : C} (f : X Y) (y : F.obj Y) :
F.map f.hom (F.map f.inv y) = y

@[simp]
theorem category_theory.functor_to_types.hom_inv_id_app_apply {C : Type u} [category_theory.category C] (F G : C Type w) (α : F G) (X : C) (x : F.obj X) :
α.inv.app X (α.hom.app X x) = x

@[simp]
theorem category_theory.functor_to_types.inv_hom_id_app_apply {C : Type u} [category_theory.category C] (F G : C Type w) (α : F G) (X : C) (x : G.obj X) :
α.hom.app X (α.inv.app X x) = x

def category_theory.ulift_trivial (V : Type u) :

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

Equations
def category_theory.ulift_functor  :
Type u Type (max u v)

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

Equations
@[simp]
theorem category_theory.ulift_functor_map {X Y : Type u} (f : X Y) (x : ulift X) :

@[instance]

Equations
def category_theory.hom_of_element {X : Type u} :
X → (punit X)

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

Equations

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

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

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

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

def category_theory.of_type_functor (m : Type uType v) [functor m] [is_lawful_functor m] :
Type u Type v

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

Equations
@[simp]
theorem category_theory.of_type_functor_map (m : Type uType v) [functor m] [is_lawful_functor m] {α β : Type u} (f : α → β) :

def equiv.to_iso {X Y : Type u} :
X Y(X Y)

Any equivalence between types in the same universe gives a categorical isomorphism between those types.

Equations
@[simp]
theorem equiv.to_iso_hom {X Y : Type u} {e : X Y} :

@[simp]
theorem equiv.to_iso_inv {X Y : Type u} {e : X Y} :

def category_theory.iso.to_equiv {X Y : Type u} :
(X Y)X Y

Any isomorphism between types gives an equivalence.

Equations
@[simp]
theorem category_theory.iso.to_equiv_fun {X Y : Type u} (i : X Y) :

@[simp]
theorem category_theory.iso.to_equiv_symm_fun {X Y : Type u} (i : X Y) :

@[simp]
theorem category_theory.iso.to_equiv_comp {X Y Z : Type u} (f : X Y) (g : Y Z) :

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

Equations
def equiv_iso_iso {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
@[simp]
theorem equiv_iso_iso_inv {X Y : Type u} (i : X Y) :

@[simp]
theorem equiv_iso_iso_hom {X Y : Type u} (e : X Y) :

def equiv_equiv_iso (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
@[simp]
theorem equiv_equiv_iso_hom {X Y : Type u} (e : X Y) :

@[simp]
theorem equiv_equiv_iso_inv {X Y : Type u} (e : X Y) :