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.

def CategoryTheory.typesGrothendieckTopology : CategoryTheory.GrothendieckTopology (Type u)

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

@[simp]

theorem CategoryTheory.discreteSieve_apply (α : Type u) : ∀ (x : Type u) (f : x ⟶ α), (CategoryTheory.discreteSieve α).arrows f = ∃ x_1, ∀ (y : x), f y = x_1

def CategoryTheory.discreteSieve (α : Type u) : CategoryTheory.Sieve α

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

theorem CategoryTheory.discreteSieve_mem (α : Type u) : CategoryTheory.discreteSieve α ∈ CategoryTheory.GrothendieckTopology.sieves CategoryTheory.typesGrothendieckTopology α

def CategoryTheory.discretePresieve (α : Type u) : CategoryTheory.Presieve α

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

theorem CategoryTheory.generate_discretePresieve_mem (α : Type u) : CategoryTheory.Sieve.generate (CategoryTheory.discretePresieve α) ∈ CategoryTheory.GrothendieckTopology.sieves CategoryTheory.typesGrothendieckTopology α

theorem CategoryTheory.isSheaf_yoneda' {α : Type u} : CategoryTheory.Presieve.IsSheaf CategoryTheory.typesGrothendieckTopology (CategoryTheory.yoneda.obj α)

@[simp]

theorem CategoryTheory.yoneda'_map_val : ∀ {X Y : Type u} (f : X ⟶ Y), (CategoryTheory.yoneda'.map f).val = CategoryTheory.yoneda.map f

@[simp]

theorem CategoryTheory.yoneda'_obj_val (α : Type u) : (CategoryTheory.yoneda'.obj α).val = CategoryTheory.yoneda.obj α

def CategoryTheory.yoneda' : CategoryTheory.Functor (Type u) (CategoryTheory.SheafOfTypes CategoryTheory.typesGrothendieckTopology)

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

@[simp]

theorem CategoryTheory.yoneda'_comp : CategoryTheory.Functor.comp CategoryTheory.yoneda' (CategoryTheory.sheafOfTypesToPresheaf CategoryTheory.typesGrothendieckTopology) = CategoryTheory.yoneda

def CategoryTheory.eval (P : CategoryTheory.Functor Type uᵒᵖ (Type u)) (α : Type u) (s : P.obj (Opposite.op α)) (x : α) : P.obj (Opposite.op PUnit.{u + 1} )

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

noncomputable def CategoryTheory.typesGlue (S : CategoryTheory.Functor Type uᵒᵖ (Type u)) (hs : CategoryTheory.Presieve.IsSheaf CategoryTheory.typesGrothendieckTopology S) (α : Type u) (f : α → S.obj (Opposite.op PUnit.{u + 1} )) : S.obj (Opposite.op α)

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

theorem CategoryTheory.eval_typesGlue {S : CategoryTheory.Functor Type uᵒᵖ (Type u)} {hs : CategoryTheory.Presieve.IsSheaf CategoryTheory.typesGrothendieckTopology S} {α : Type u} (f : α → S.obj (Opposite.op PUnit.{u + 1} )) : CategoryTheory.eval S α (CategoryTheory.typesGlue S hs α f) = f

theorem CategoryTheory.typesGlue_eval {S : CategoryTheory.Functor Type uᵒᵖ (Type u)} {hs : CategoryTheory.Presieve.IsSheaf CategoryTheory.typesGrothendieckTopology S} {α : Type u} (s : S.obj (Opposite.op α)) : CategoryTheory.typesGlue S hs α (CategoryTheory.eval S α s) = s

@[simp]

theorem CategoryTheory.evalEquiv_apply (S : CategoryTheory.Functor Type uᵒᵖ (Type u)) (hs : CategoryTheory.Presieve.IsSheaf CategoryTheory.typesGrothendieckTopology S) (α : Type u) (s : S.obj (Opposite.op α)) (x : α) : ↑(CategoryTheory.evalEquiv S hs α) s x = CategoryTheory.eval S α s x

@[simp]

theorem CategoryTheory.evalEquiv_symm_apply (S : CategoryTheory.Functor Type uᵒᵖ (Type u)) (hs : CategoryTheory.Presieve.IsSheaf CategoryTheory.typesGrothendieckTopology S) (α : Type u) (f : α → S.obj (Opposite.op PUnit.{u + 1} )) : ↑(CategoryTheory.evalEquiv S hs α).symm f = CategoryTheory.typesGlue S hs α f

noncomputable def CategoryTheory.evalEquiv (S : CategoryTheory.Functor Type uᵒᵖ (Type u)) (hs : CategoryTheory.Presieve.IsSheaf CategoryTheory.typesGrothendieckTopology S) (α : Type u) : S.obj (Opposite.op α) ≃ (α → S.obj (Opposite.op PUnit.{u + 1} ))

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

theorem CategoryTheory.eval_map (S : CategoryTheory.Functor Type uᵒᵖ (Type u)) (α : Type u) (β : Type u) (f : β ⟶ α) (s : S.obj (Opposite.op α)) (x : β) : CategoryTheory.eval S β (Type uᵒᵖ.map CategoryTheory.CategoryStruct.toQuiver (Type u) CategoryTheory.CategoryStruct.toQuiver S.toPrefunctor (Opposite.op α) (Opposite.op β) f.op s) x = CategoryTheory.eval S α s (f x)

@[simp]

theorem CategoryTheory.equivYoneda_inv_app (S : CategoryTheory.Functor Type uᵒᵖ (Type u)) (hs : CategoryTheory.Presieve.IsSheaf CategoryTheory.typesGrothendieckTopology S) (X : Type uᵒᵖ) : ∀ (a : (CategoryTheory.yoneda.obj (S.obj (Opposite.op PUnit.{u + 1} ))).obj X), Type uᵒᵖ.app CategoryTheory.Category.opposite (Type u) CategoryTheory.types (CategoryTheory.yoneda.obj (S.obj (Opposite.op PUnit.{u + 1} ))) S (CategoryTheory.equivYoneda S hs).inv X a = ↑(CategoryTheory.evalEquiv S hs X.unop).symm a

@[simp]

theorem CategoryTheory.equivYoneda_hom_app (S : CategoryTheory.Functor Type uᵒᵖ (Type u)) (hs : CategoryTheory.Presieve.IsSheaf CategoryTheory.typesGrothendieckTopology S) (X : Type uᵒᵖ) : ∀ (a : S.obj X), Type uᵒᵖ.app CategoryTheory.Category.opposite (Type u) CategoryTheory.types S (CategoryTheory.yoneda.obj (S.obj (Opposite.op PUnit.{u + 1} ))) (CategoryTheory.equivYoneda S hs).hom X a = ↑(CategoryTheory.evalEquiv S hs X.unop) a

noncomputable def CategoryTheory.equivYoneda (S : CategoryTheory.Functor Type uᵒᵖ (Type u)) (hs : CategoryTheory.Presieve.IsSheaf CategoryTheory.typesGrothendieckTopology S) : S ≅ CategoryTheory.yoneda.obj (S.obj (Opposite.op PUnit.{u + 1} ))

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

@[simp]

theorem CategoryTheory.equivYoneda'_hom_val (S : CategoryTheory.SheafOfTypes CategoryTheory.typesGrothendieckTopology) : (CategoryTheory.equivYoneda' S).hom.val = (CategoryTheory.equivYoneda S.val (_ : CategoryTheory.Presieve.IsSheaf CategoryTheory.typesGrothendieckTopology S.val)).hom

@[simp]

theorem CategoryTheory.equivYoneda'_inv_val (S : CategoryTheory.SheafOfTypes CategoryTheory.typesGrothendieckTopology) : (CategoryTheory.equivYoneda' S).inv.val = (CategoryTheory.equivYoneda S.val (_ : CategoryTheory.Presieve.IsSheaf CategoryTheory.typesGrothendieckTopology S.val)).inv

noncomputable def CategoryTheory.equivYoneda' (S : CategoryTheory.SheafOfTypes CategoryTheory.typesGrothendieckTopology) : S ≅ CategoryTheory.yoneda'.obj (S.val.obj (Opposite.op PUnit.{u_1 + 1} ))

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

theorem CategoryTheory.eval_app (S₁ : CategoryTheory.SheafOfTypes CategoryTheory.typesGrothendieckTopology) (S₂ : CategoryTheory.SheafOfTypes CategoryTheory.typesGrothendieckTopology) (f : S₁ ⟶ S₂) (α : Type u) (s : S₁.val.obj (Opposite.op α)) (x : α) : CategoryTheory.eval S₂.val α (Type uᵒᵖ.app CategoryTheory.Category.opposite (Type u) CategoryTheory.types S₁.val S₂.val f.val (Opposite.op α) s) x = Type uᵒᵖ.app CategoryTheory.Category.opposite (Type u) CategoryTheory.types S₁.val S₂.val f.val (Opposite.op PUnit.{u + 1} ) (CategoryTheory.eval S₁.val α s x)

@[simp]

theorem CategoryTheory.typeEquiv_counitIso_inv_app_val_app (X : CategoryTheory.SheafOfTypes CategoryTheory.typesGrothendieckTopology) (X : Type uᵒᵖ) : ∀ (a : X.val.obj X), Type uᵒᵖ.app CategoryTheory.Category.opposite (Type u) CategoryTheory.types X.val (CategoryTheory.yoneda.obj (X.val.obj (Opposite.op PUnit.{u + 1} ))) (CategoryTheory.typeEquiv.counitIso.inv.app X).val X a = ↑(CategoryTheory.evalEquiv X.val (_ : CategoryTheory.Presieve.IsSheaf CategoryTheory.typesGrothendieckTopology X.val) X.unop) a

@[simp]

theorem CategoryTheory.typeEquiv_functor_obj_val_obj (α : Type u) (Y : Type uᵒᵖ) : (CategoryTheory.typeEquiv.functor.obj α).val.obj Y = (Y.unop ⟶ α)

@[simp]

theorem CategoryTheory.typeEquiv_functor_obj_val_map (α : Type u) : ∀ {X Y : Type uᵒᵖ} (f : X ⟶ Y) (g : X.unop ⟶ α) (a : Y.unop), Type uᵒᵖ.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]

theorem CategoryTheory.typeEquiv_inverse_obj (X : CategoryTheory.SheafOfTypes CategoryTheory.typesGrothendieckTopology) : CategoryTheory.typeEquiv.inverse.obj X = X.val.obj (Opposite.op PUnit.{u + 1} )

@[simp]

theorem CategoryTheory.typeEquiv_unitIso_hom_app (X : Type u) : ∀ (a : (CategoryTheory.Functor.id (Type u)).obj X), Type u.app CategoryTheory.types (Type u) CategoryTheory.types (CategoryTheory.Functor.id (Type u)) (CategoryTheory.Functor.comp CategoryTheory.yoneda' (CategoryTheory.Functor.comp (CategoryTheory.sheafOfTypesToPresheaf CategoryTheory.typesGrothendieckTopology) ((CategoryTheory.evaluation Type uᵒᵖ (Type u)).obj (Opposite.op PUnit.{u + 1} )))) CategoryTheory.typeEquiv.unitIso.hom X a = CategoryTheory.CategoryStruct.comp (↑(CategoryTheory.evalEquiv (CategoryTheory.yoneda.obj X) (_ : CategoryTheory.Presieve.IsSheaf CategoryTheory.typesGrothendieckTopology (CategoryTheory.yoneda'.obj X).val) PUnit.{u + 1} ) fun x => a) fun f => f PUnit.unit

@[simp]

theorem CategoryTheory.typeEquiv_inverse_map : ∀ {X Y : CategoryTheory.SheafOfTypes CategoryTheory.typesGrothendieckTopology} (f : X ⟶ Y) (a : ((CategoryTheory.evaluation Type uᵒᵖ (Type u)).obj (Opposite.op PUnit.{u + 1} )).obj ((CategoryTheory.sheafOfTypesToPresheaf CategoryTheory.typesGrothendieckTopology).obj X)), CategoryTheory.typeEquiv.inverse.map f a = f.val.app (Opposite.op PUnit.{u + 1} ) a

@[simp]

theorem CategoryTheory.typeEquiv_functor_map_val_app : ∀ {X Y : Type u} (f : X ⟶ Y) (Y_1 : Type uᵒᵖ) (g : ((fun X => CategoryTheory.Functor.mk { obj := fun Y => Y.unop ⟶ X, map := fun {X_1 Y} f g => CategoryTheory.CategoryStruct.comp f.unop 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 : (CategoryTheory.Functor.comp CategoryTheory.yoneda' (CategoryTheory.Functor.comp (CategoryTheory.sheafOfTypesToPresheaf CategoryTheory.typesGrothendieckTopology) ((CategoryTheory.evaluation Type uᵒᵖ (Type u)).obj (Opposite.op PUnit.{u + 1} )))).obj X), Type u.app CategoryTheory.types (Type u) CategoryTheory.types (CategoryTheory.Functor.comp CategoryTheory.yoneda' (CategoryTheory.Functor.comp (CategoryTheory.sheafOfTypesToPresheaf CategoryTheory.typesGrothendieckTopology) ((CategoryTheory.evaluation Type uᵒᵖ (Type u)).obj (Opposite.op PUnit.{u + 1} )))) (CategoryTheory.Functor.id (Type u)) CategoryTheory.typeEquiv.unitIso.inv X a = ↑(CategoryTheory.evalEquiv (CategoryTheory.yoneda.obj X) (_ : CategoryTheory.Presieve.IsSheaf CategoryTheory.typesGrothendieckTopology (CategoryTheory.yoneda'.obj X).val) 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 : CategoryTheory.SheafOfTypes CategoryTheory.typesGrothendieckTopology) (X : Type uᵒᵖ) : ∀ (a : (CategoryTheory.yoneda.obj (X.val.obj (Opposite.op PUnit.{u + 1} ))).obj X), Type uᵒᵖ.app CategoryTheory.Category.opposite (Type u) CategoryTheory.types (CategoryTheory.yoneda.obj (X.val.obj (Opposite.op PUnit.{u + 1} ))) X.val (CategoryTheory.typeEquiv.counitIso.hom.app X).val X a = ↑(CategoryTheory.evalEquiv X.val (_ : CategoryTheory.Presieve.IsSheaf CategoryTheory.typesGrothendieckTopology X.val) X.unop).symm a

noncomputable def CategoryTheory.typeEquiv : Type u ≌ CategoryTheory.SheafOfTypes CategoryTheory.typesGrothendieckTopology

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

theorem CategoryTheory.subcanonical_typesGrothendieckTopology : CategoryTheory.Sheaf.Subcanonical CategoryTheory.typesGrothendieckTopology

theorem CategoryTheory.typesGrothendieckTopology_eq_canonical : CategoryTheory.typesGrothendieckTopology = CategoryTheory.Sheaf.canonicalTopology (Type u)