# Documentation

Mathlib.CategoryTheory.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.

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.

Instances For

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

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.

Instances For
def CategoryTheory.eval (P : ) (α : Type u) (s : P.obj ()) (x : α) :
P.obj ()

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

Instances For
noncomputable def CategoryTheory.typesGlue (S : ) (α : Type u) (f : αS.obj ()) :
S.obj ()

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

Instances For
theorem CategoryTheory.eval_typesGlue {S : } {α : Type u} (f : αS.obj ()) :
theorem CategoryTheory.typesGlue_eval {S : } {α : Type u} (s : S.obj ()) :
@[simp]
theorem CategoryTheory.evalEquiv_apply (S : ) (α : Type u) (s : S.obj ()) (x : α) :
↑() s x =
@[simp]
theorem CategoryTheory.evalEquiv_symm_apply (S : ) (α : Type u) (f : αS.obj ()) :
().symm f =
noncomputable def CategoryTheory.evalEquiv (S : ) (α : Type u) :
S.obj () (αS.obj ())

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

Instances For
theorem CategoryTheory.eval_map (S : ) (α : Type u) (β : Type u) (f : β α) (s : S.obj ()) (x : β) :
CategoryTheory.eval S β (.map CategoryTheory.CategoryStruct.toQuiver (Type u) CategoryTheory.CategoryStruct.toQuiver S.toPrefunctor () () f.op s) x = CategoryTheory.eval S α s (f x)
@[simp]
theorem CategoryTheory.equivYoneda_inv_app (S : ) (X : ) :
∀ (a : (CategoryTheory.yoneda.obj (S.obj ())).obj X), .app CategoryTheory.Category.opposite (Type u) CategoryTheory.types (CategoryTheory.yoneda.obj (S.obj ())) S ().inv X a = (CategoryTheory.evalEquiv S hs X.unop).symm a
@[simp]
theorem CategoryTheory.equivYoneda_hom_app (S : ) (X : ) :
∀ (a : S.obj X), .app CategoryTheory.Category.opposite (Type u) CategoryTheory.types S (CategoryTheory.yoneda.obj (S.obj ())) ().hom X a = ↑(CategoryTheory.evalEquiv S hs X.unop) a
noncomputable def CategoryTheory.equivYoneda (S : ) :
S CategoryTheory.yoneda.obj (S.obj ())

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

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 CategoryTheory.yoneda'.obj (S.val.obj ())

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

Instances For
theorem CategoryTheory.eval_app (f : S₁ S₂) (α : Type u) (s : S₁.val.obj ()) (x : α) :
CategoryTheory.eval S₂.val α (.app CategoryTheory.Category.opposite (Type u) CategoryTheory.types S₁.val S₂.val f.val () s) x = .app CategoryTheory.Category.opposite (Type u) CategoryTheory.types S₁.val S₂.val f.val () (CategoryTheory.eval S₁.val α s x)
@[simp]
theorem CategoryTheory.typeEquiv_counitIso_inv_app_val_app (X : ) :
∀ (a : X.val.obj X), .app CategoryTheory.Category.opposite (Type u) CategoryTheory.types X.val (CategoryTheory.yoneda.obj (X.val.obj ())) (CategoryTheory.typeEquiv.counitIso.inv.app X).val 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), .map CategoryTheory.CategoryStruct.toQuiver (Type u) CategoryTheory.CategoryStruct.toQuiver (CategoryTheory.typeEquiv.functor.obj α).val.toPrefunctor X Y f g a = g (f.unop a)
@[simp]
@[simp]
theorem CategoryTheory.typeEquiv_unitIso_hom_app (X : Type u) :
∀ (a : ().obj X), Type u.app CategoryTheory.types (Type u) CategoryTheory.types () () CategoryTheory.typeEquiv.unitIso.hom X a = CategoryTheory.CategoryStruct.comp (↑(CategoryTheory.evalEquiv (CategoryTheory.yoneda.obj X) (_ : ) PUnit.{u + 1} ) fun x => a) fun f =>
@[simp]
theorem CategoryTheory.typeEquiv_inverse_map :
∀ {X Y : } (f : X Y) (a : (().obj ()).obj ()), CategoryTheory.typeEquiv.inverse.map f a = f.val.app () a
@[simp]
theorem CategoryTheory.typeEquiv_functor_map_val_app :
∀ {X Y : Type u} (f : X Y) (Y_1 : ) (g : ((fun X => CategoryTheory.Functor.mk { obj := fun Y => Y.unop X, map := fun {X_1 Y} f g => }) 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 X), Type u.app CategoryTheory.types (Type u) CategoryTheory.types () () CategoryTheory.typeEquiv.unitIso.inv X a = (CategoryTheory.evalEquiv (CategoryTheory.yoneda.obj X) (_ : ) PUnit.{u + 1} ).symm (CategoryTheory.CategoryStruct.comp a fun x x_1 => x) PUnit.unit
@[simp]
theorem CategoryTheory.typeEquiv_counitIso_hom_app_val_app (X : ) :
∀ (a : (CategoryTheory.yoneda.obj (X.val.obj ())).obj X), .app CategoryTheory.Category.opposite (Type u) CategoryTheory.types (CategoryTheory.yoneda.obj (X.val.obj ())) X.val (CategoryTheory.typeEquiv.counitIso.hom.app X).val X a = (CategoryTheory.evalEquiv X.val X.unop).symm a

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

Instances For