mathlibdocumentation

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
def category_theory.discrete_sieve (α : Type u) :

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 : β α) :
= ∃ (x : α), ∀ (y : β), f y = x
def category_theory.discrete_presieve (α : Type u) :

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

Equations
• = λ (β : Type u) (f : β α), ∃ (x : β), ∀ (y : β), y = x
@[simp]
theorem category_theory.yoneda'_obj_val (α : Type u) :

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

Equations
@[simp]
theorem category_theory.yoneda'_map_val (α β : Type u) (f : α β) :
def category_theory.eval (P : (Type u)ᵒᵖ Type u) (α : Type u) (s : P.obj (opposite.op α)) (x : α) :
P.obj

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) (α : Type u) (f : α → S.obj ) :

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

Equations
theorem category_theory.eval_types_glue {S : (Type u)ᵒᵖ Type u} {α : Type u} (f : α → S.obj ) :
α f) = f
theorem category_theory.types_glue_eval {S : (Type u)ᵒᵖ Type u} {α : Type u} (s : S.obj (opposite.op α)) :
s) = s
@[simp]
theorem category_theory.eval_equiv_symm_apply (S : (Type u)ᵒᵖ Type u) (α : Type u) (f : α → S.obj ) :
α).symm) f = f
noncomputable def category_theory.eval_equiv (S : (Type u)ᵒᵖ Type u) (α : Type u) :
S.obj (opposite.op α) (α → S.obj

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

Equations
@[simp]
theorem category_theory.eval_equiv_apply (S : (Type u)ᵒᵖ Type u) (α : Type u) (s : S.obj (opposite.op α)) (x : α) :
α) s x = s x
theorem category_theory.eval_map (S : (Type u)ᵒᵖ Type u) (α β : Type u) (f : β α) (s : S.obj (opposite.op α)) (x : β) :
(S.map f.op s) x = s (f x)
noncomputable def category_theory.equiv_yoneda (S : (Type u)ᵒᵖ Type u)  :

Given a sheaf S, construct an isomorphism S ≅ [-, S(*)].

Equations
@[simp]
theorem category_theory.equiv_yoneda_hom_app (S : (Type u)ᵒᵖ Type u) (X : (Type u)ᵒᵖ) (ᾰ : S.obj X) :
.hom.app X = (opposite.unop X))
@[simp]
theorem category_theory.equiv_yoneda_inv_app (S : (Type u)ᵒᵖ Type u) (X : (Type u)ᵒᵖ) (ᾰ : (category_theory.yoneda.obj (S.obj (opposite.op punit))).obj X) :
.inv.app X =
@[simp]
noncomputable def category_theory.equiv_yoneda'  :

Given a sheaf S, construct an isomorphism S ≅ [-, S(*)].

Equations
@[simp]
theorem category_theory.eval_app (f : S₁ S₂) (α : Type u) (s : S₁.val.obj (opposite.op α)) (x : α) :
(f.val.app (opposite.op α) s) x = f.val.app α s x)
noncomputable def category_theory.type_equiv  :

yoneda' induces an equivalence of category between Type u and Sheaf types_grothendieck_topology.

Equations
@[simp]
theorem category_theory.type_equiv_counit_iso_inv_app_val_app (X_1 : (Type u)ᵒᵖ) (ᾰ : X.val.obj X_1) :
X_1 = (opposite.unop X_1))
@[simp]
theorem category_theory.type_equiv_unit_iso_inv_app (X : Type u)  :
= (ᾰ λ (x : X) (_x : punit), x) punit.star
@[simp]
@[simp]
theorem category_theory.type_equiv_unit_iso_hom_app (X : Type u) (ᾰ : (𝟭 (Type u)).obj X) :
= (λ (_x : punit), ᾰ) λ (f : punit X),
@[simp]
theorem category_theory.type_equiv_functor_map_val_app (α β : Type u) (f : α β) (Y : (Type u)ᵒᵖ) (g : {obj := λ (Y : (Type u)ᵒᵖ), , map := λ (Y Y' : (Type u)ᵒᵖ) (f : Y Y') (g : α), f.unop g, map_id' := _, map_comp' := _}.obj Y) (ᾰ : opposite.unop Y) :
g = f (g ᾰ)
@[simp]
theorem category_theory.type_equiv_inverse_map (f : _x _x_1) (ᾰ : ((category_theory.evaluation (Type u)ᵒᵖ (Type u)).obj .obj ) :
= f.val.app
@[simp]
@[simp]
theorem category_theory.type_equiv_functor_obj_val_obj (α : Type u) (Y : (Type u)ᵒᵖ) :
= α)
@[simp]
theorem category_theory.type_equiv_functor_obj_val_map (α : Type u) (Y Y' : (Type u)ᵒᵖ) (f : Y Y') (g : α) (ᾰ : opposite.unop Y') :
g = g (f.unop ᾰ)