# 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
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.discreteSieve_apply (α : Type u) :
∀ (x : Type u) (f : x α), .arrows f = ∃ (x_1 : α), ∀ (y : x), f y = x_1

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

Equations
• = { arrows := fun (x : Type u) (f : x α) => ∃ (x_1 : α), ∀ (y : x), f y = x_1, downward_closed := }
Instances For

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

Equations
• = ∃ (x : β), ∀ (y : β), y = x
Instances For
@[simp]
theorem CategoryTheory.yoneda'_map_val :
∀ {X Y : Type u} (f : X Y), ().val = CategoryTheory.yoneda.map f
@[simp]
theorem CategoryTheory.yoneda'_obj_val (α : Type u) :
().val = CategoryTheory.yoneda.obj α

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.yoneda'_comp :
= CategoryTheory.yoneda
def CategoryTheory.eval (P : ) (α : Type u) (s : P.obj { unop := α }) (x : α) :
P.obj { unop := PUnit.{u + 1} }

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

Equations
Instances For
noncomputable def CategoryTheory.typesGlue (S : ) (α : Type u) (f : αS.obj { unop := PUnit.{u + 1} }) :
S.obj { unop := α }

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem CategoryTheory.eval_typesGlue {S : } {α : Type u} (f : αS.obj { unop := PUnit.{u + 1} }) :
theorem CategoryTheory.typesGlue_eval {S : } {α : Type u} (s : S.obj { unop := α }) :
@[simp]
theorem CategoryTheory.evalEquiv_apply (S : ) (α : Type u) (s : S.obj { unop := α }) (x : α) :
() s x =
@[simp]
theorem CategoryTheory.evalEquiv_symm_apply (S : ) (α : Type u) (f : αS.obj { unop := PUnit.{u + 1} }) :
().symm f =
noncomputable def CategoryTheory.evalEquiv (S : ) (α : Type u) :
S.obj { unop := α } (αS.obj { unop := PUnit.{u + 1} })

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

Equations
• = { toFun := , invFun := , left_inv := , right_inv := }
Instances For
theorem CategoryTheory.eval_map (S : ) (α : Type u) (β : Type u) (f : β α) (s : S.obj { unop := α }) (x : β) :
CategoryTheory.eval S β (S.map f.op s) x = CategoryTheory.eval S α s (f x)
@[simp]
theorem CategoryTheory.equivYoneda_inv_app (S : ) (X : ) :
∀ (a : (CategoryTheory.yoneda.obj (S.obj { unop := PUnit.{u + 1} })).obj X), ().inv.app X a = (CategoryTheory.evalEquiv S hs X.unop).symm a
@[simp]
theorem CategoryTheory.equivYoneda_hom_app (S : ) (X : ) :
∀ (a : S.obj X), ().hom.app X a = (CategoryTheory.evalEquiv S hs X.unop) a
noncomputable def CategoryTheory.equivYoneda (S : ) :
S CategoryTheory.yoneda.obj (S.obj { unop := PUnit.{u + 1} })

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

Equations
Instances For
@[simp]
theorem CategoryTheory.equivYoneda'_hom_val :
.hom.val = ().hom
@[simp]
theorem CategoryTheory.equivYoneda'_inv_val :
.inv.val = ().inv
noncomputable def CategoryTheory.equivYoneda' :
S (S.val.obj { unop := PUnit.{u_1 + 1} })

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

Equations
• = { hom := { val := ().hom }, inv := { val := ().inv }, hom_inv_id := , inv_hom_id := }
Instances For
theorem CategoryTheory.eval_app (f : S₁ S₂) (α : Type u) (s : S₁.val.obj { unop := α }) (x : α) :
CategoryTheory.eval S₂.val α (f.val.app { unop := α } s) x = f.val.app { unop := PUnit.{u + 1} } (CategoryTheory.eval S₁.val α s x)
@[simp]
theorem CategoryTheory.typeEquiv_counitIso_inv_app_val_app (X : ) :
∀ (a : X✝.val.obj X), (CategoryTheory.typeEquiv.counitIso.inv.app X✝).val.app X a = (CategoryTheory.evalEquiv X✝.val X.unop) a
@[simp]
theorem CategoryTheory.typeEquiv_functor_obj_val_obj (α : Type u) (Y : ) :
(CategoryTheory.typeEquiv.functor.obj α).val.obj Y = (Y.unop α)
@[simp]
theorem CategoryTheory.typeEquiv_functor_obj_val_map (α : Type u) :
∀ {X Y : } (f : X Y) (g : X.unop α) (a : Y.unop), (CategoryTheory.typeEquiv.functor.obj α).val.map f g a = g (f.unop a)
@[simp]
@[simp]
theorem CategoryTheory.typeEquiv_unitIso_hom_app (X : Type u) :
∀ (a : .obj X), CategoryTheory.typeEquiv.unitIso.hom.app X a = CategoryTheory.CategoryStruct.comp ((CategoryTheory.evalEquiv (CategoryTheory.yoneda.obj X) PUnit.{u + 1} ) fun (x : PUnit.{u + 1} ) => a) fun (f : ) =>
@[simp]
theorem CategoryTheory.typeEquiv_inverse_map :
∀ {X Y : } (f : X Y) (a : (().obj { unop := PUnit.{u + 1} }).obj ), CategoryTheory.typeEquiv.inverse.map f a = f.val.app { unop := PUnit.{u + 1} } a
@[simp]
theorem CategoryTheory.typeEquiv_functor_map_val_app :
∀ {X Y : Type u} (f : X Y) (Y_1 : ) (g : ((fun (X : Type u) => { obj := fun (Y : ) => Y.unop X, map := fun {X_1 Y : } (f : X_1 Y) (g : (fun (Y : ) => Y.unop X) X_1) => , map_id := , map_comp := }) X).obj Y_1) (a : Y_1.unop), (CategoryTheory.typeEquiv.functor.map f).val.app Y_1 g a = f (g a)
@[simp]
theorem CategoryTheory.typeEquiv_unitIso_inv_app (X : Type u) :
∀ (a : ( ( (().obj { unop := PUnit.{u + 1} }))).obj X), CategoryTheory.typeEquiv.unitIso.inv.app X a = (CategoryTheory.evalEquiv (CategoryTheory.yoneda.obj X) PUnit.{u + 1} ).symm (CategoryTheory.CategoryStruct.comp a fun (x : X) (x_1 : PUnit.{u + 1} ) => x) PUnit.unit
@[simp]
theorem CategoryTheory.typeEquiv_counitIso_hom_app_val_app (X : ) :
∀ (a : (CategoryTheory.yoneda.obj (X✝.val.obj { unop := PUnit.{u + 1} })).obj X), (CategoryTheory.typeEquiv.counitIso.hom.app X✝).val.app X a = (CategoryTheory.evalEquiv X✝.val X.unop).symm a

yoneda' induces an equivalence of category between Type u and SheafOfTypes typesGrothendieckTopology.

Equations
• One or more equations did not get rendered due to their size.
Instances For