mathlib3 documentation

category_theory.sites.types

Grothendieck Topology and Sheaves on the Category of Types #

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

In this file we define a Grothendieck topology on the category of types, and construct the canonical functor that sends a type to a sheaf over the category of types, and make this an equivalence of categories.

Then we prove that the topology defined is the canonical topology.

A Grothendieck topology associated to the category of all types. A sieve is a covering iff it is jointly surjective.

Equations

The discrete sieve on a type, which only includes arrows whose image is a subsingleton.

Equations
@[simp]
theorem category_theory.discrete_sieve_apply (α β : Type u) (f : β α) :
(category_theory.discrete_sieve α) f = (x : α), (y : β), f y = x

The discrete presieve on a type, which only includes arrows whose domain is a singleton.

Equations

The yoneda functor that sends a type to a sheaf over the category of types

Equations
def category_theory.eval (P : (Type u)ᵒᵖ Type u) (α : Type u) (s : P.obj (opposite.op α)) (x : α) :

Given a presheaf P on the category of types, construct a map P(α) → (α → P(*)) for all type α.

Equations

Given a sheaf S on the category of types, construct a map (α → S(*)) → S(α) that is inverse to eval.

Equations

Given a sheaf S, construct an equivalence S(α) ≃ (α → S(*)).

Equations
theorem category_theory.eval_map (S : (Type u)ᵒᵖ Type u) (α β : Type u) (f : β α) (s : S.obj (opposite.op α)) (x : β) :
category_theory.eval S β (S.map f.op s) x = category_theory.eval S α s (f x)
@[simp]
theorem category_theory.type_equiv_functor_map_val_app (α β : Type u) (f : α β) (Y : (Type u)ᵒᵖ) (g : {obj := λ (Y : (Type u)ᵒᵖ), opposite.unop Y α, map := λ (Y Y' : (Type u)ᵒᵖ) (f : Y Y') (g : opposite.unop Y α), f.unop g, map_id' := _, map_comp' := _}.obj Y) (ᾰ : opposite.unop Y) :
@[simp]
theorem category_theory.type_equiv_functor_obj_val_map (α : Type u) (Y Y' : (Type u)ᵒᵖ) (f : Y Y') (g : opposite.unop Y α) (ᾰ : opposite.unop Y') :