mathlib3 documentation

category_theory.types

The category `Type`. #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.) The notation is enabled using open_locale category_theory.Type.

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:

epimorphisms are surjections and monomorphisms are injections,
iso is both iso and equiv to equiv (at least within a fixed universe),
every type level is_lawful_functor gives a categorical functor Type ⥤ Type (the corresponding fact about monads is in src/category_theory/monad/types.lean).

@[protected, instance]

def category_theory.types :

category_theory.large_category (Type u)

Equations

category_theory.types = {to_category_struct := {to_quiver := {hom := λ (a b : Type u), a → b}, id := λ (a : Type u), id, comp := λ (_x _x_1 _x_2 : Type u) (f : _x ⟶ _x_1) (g : _x_1 ⟶ _x_2), g ∘ f}, id_comp' := category_theory.types._proof_1, comp_id' := category_theory.types._proof_2, assoc' := category_theory.types._proof_3}

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

@[reducible]

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

α ⟶ β

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

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

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

category_theory.ulift_trivial V = {hom := id (λ (ᾰ : ulift V), ᾰ.cases_on (λ (ᾰ : V), ᾰ)), inv := ulift.up V, hom_inv_id' := _, inv_hom_id' := _}

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

category_theory.ulift_functor = {obj := λ (X : Type u), ulift X, map := λ (X Y : Type u) (f : X ⟶ Y) (x : ulift X), {down := f x.down}, map_id' := category_theory.ulift_functor._proof_1, map_comp' := category_theory.ulift_functor._proof_2}

Instances for category_theory.ulift_functor

@[simp]

theorem category_theory.ulift_functor_map {X Y : Type u} (f : X ⟶ Y) (x : ulift X) :

category_theory.ulift_functor.map f x = {down := f x.down}

@[protected, instance]

def category_theory.ulift_functor_full :

category_theory.full category_theory.ulift_functor

Equations

category_theory.ulift_functor_full = {preimage := λ (X Y : Type u) (f : category_theory.ulift_functor.obj X ⟶ category_theory.ulift_functor.obj Y) (x : X), (f {down := x}).down, witness' := category_theory.ulift_functor_full._proof_1}

@[protected, instance]

def category_theory.ulift_functor_faithful :

category_theory.faithful category_theory.ulift_functor

def category_theory.ulift_functor_trivial :

category_theory.ulift_functor ≅ 𝟭 (Type u)

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

Equations

category_theory.ulift_functor_trivial = category_theory.nat_iso.of_components category_theory.ulift_trivial category_theory.ulift_functor_trivial._proof_1

def category_theory.hom_of_element {X : Type u} (x : X) :

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

Equations

category_theory.hom_of_element x = λ (_x : punit), x

theorem category_theory.hom_of_element_eq_iff {X : Type u} (x y : X) :

category_theory.hom_of_element x = category_theory.hom_of_element y ↔ x = y

theorem category_theory.mono_iff_injective {X Y : Type u} (f : X ⟶ Y) :

category_theory.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 category_theory.injective_of_mono {X Y : Type u} (f : X ⟶ Y) [hf : category_theory.mono f] :

function.injective f

theorem category_theory.epi_iff_surjective {X Y : Type u} (f : X ⟶ Y) :

category_theory.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 category_theory.surjective_of_epi {X Y : Type u} (f : X ⟶ Y) [hf : category_theory.epi f] :

function.surjective f

def category_theory.of_type_functor (m : Type u → Type 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

category_theory.of_type_functor m = {obj := m, map := λ (α β : Type u), functor.map, map_id' := _, map_comp' := _}

@[simp]

theorem category_theory.of_type_functor_obj (m : Type u → Type v) [functor m] [is_lawful_functor m] :

(category_theory.of_type_functor m).obj = m

@[simp]

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

(category_theory.of_type_functor m).map f = functor.map f

def equiv.to_iso {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.to_iso = {hom := e.to_fun, inv := e.inv_fun, hom_inv_id' := _, inv_hom_id' := _}

@[simp]

theorem equiv.to_iso_hom {X Y : Type u} {e : X ≃ Y} :

e.to_iso.hom = ⇑e

@[simp]

theorem equiv.to_iso_inv {X Y : Type u} {e : X ≃ Y} :

e.to_iso.inv = ⇑(e.symm)

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

X ≃ Y

Any isomorphism between types gives an equivalence.

Equations

i.to_equiv = {to_fun := i.hom, inv_fun := i.inv, left_inv := _, right_inv := _}

@[simp]

theorem category_theory.iso.to_equiv_fun {X Y : Type u} (i : X ≅ Y) :

⇑(i.to_equiv) = i.hom

@[simp]

theorem category_theory.iso.to_equiv_symm_fun {X Y : Type u} (i : X ≅ Y) :

⇑(i.to_equiv.symm) = i.inv

@[simp]

theorem category_theory.iso.to_equiv_id (X : Type u) :

(category_theory.iso.refl X).to_equiv = equiv.refl X

@[simp]

theorem category_theory.iso.to_equiv_comp {X Y Z : Type u} (f : X ≅ Y) (g : Y ≅ Z) :

(f ≪≫ g).to_equiv = f.to_equiv.trans g.to_equiv

theorem category_theory.is_iso_iff_bijective {X Y : Type u} (f : X ⟶ Y) :

category_theory.is_iso f ↔ function.bijective f

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

@[protected, instance]

def category_theory.sort.split_epi_category :

category_theory.split_epi_category (Type u)

Equations

category_theory.sort.split_epi_category = {is_split_epi_of_epi := category_theory.sort.split_epi_category._proof_1}

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

equiv_iso_iso = {hom := λ (e : X ≃ Y), e.to_iso, inv := λ (i : X ≅ Y), i.to_equiv, hom_inv_id' := _, inv_hom_id' := _}

@[simp]

theorem equiv_iso_iso_inv {X Y : Type u} (i : X ≅ Y) :

equiv_iso_iso.inv i = i.to_equiv

@[simp]

theorem equiv_iso_iso_hom {X Y : Type u} (e : X ≃ Y) :

equiv_iso_iso.hom e = e.to_iso

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

equiv_equiv_iso = equiv_iso_iso.to_equiv

@[simp]

theorem equiv_equiv_iso_hom {X Y : Type u} (e : X ≃ Y) :

⇑equiv_equiv_iso e = e.to_iso

@[simp]

theorem equiv_equiv_iso_inv {X Y : Type u} (e : X ≅ Y) :

⇑(equiv_equiv_iso.symm) e = e.to_equiv