mathlib documentation

category_theory.sites.types

Grothendieck Topology and Sheaves on the Category of Types #

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
@[simp]
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
noncomputable def category_theory.types_glue (S : (Type u)ᵒᵖ Type u) (hs : category_theory.presieve.is_sheaf category_theory.types_grothendieck_topology S) (α : Type u) (f : α → S.obj (opposite.op punit)) :

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)
theorem category_theory.eval_app (S₁ S₂ : category_theory.SheafOfTypes category_theory.types_grothendieck_topology) (f : S₁ S₂) (α : Type u) (s : S₁.val.obj (opposite.op α)) (x : α) :
@[simp]
theorem category_theory.type_equiv_unit_iso_hom_app (X : Type u) (ᾰ : (𝟭 (Type u)).obj 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') :