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.

Equations

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

@[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.

Equations

• CategoryTheory.discreteSieve α = { arrows := fun (x : Type u) (f : x ⟶ α) => ∃ (x_1 : α), ∀ (y : x), f y = x_1, downward_closed := ⋯ }

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

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

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

Equations

• CategoryTheory.discretePresieve α x = ∃ (x : β), ∀ (y : β), y = x

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

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.

Equations

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

@[simp]

theorem CategoryTheory.yoneda'_comp : CategoryTheory.yoneda'.comp (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 α.

Equations

• CategoryTheory.eval P α s x = P.map (CategoryTheory.asHom fun (x_1 : PUnit.{u + 1} ) => x).op s

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.

Equations

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

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(*)).

Equations

• CategoryTheory.evalEquiv S hs α = { toFun := CategoryTheory.eval S α, invFun := CategoryTheory.typesGlue S hs α, left_inv := ⋯, right_inv := ⋯ }

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 β (S.map 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), (CategoryTheory.equivYoneda S hs).inv.app 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), (CategoryTheory.equivYoneda S hs).hom.app 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(*)].

Equations

• CategoryTheory.equivYoneda S hs = CategoryTheory.NatIso.ofComponents (fun (α : Type uᵒᵖ) => (CategoryTheory.evalEquiv S hs α.unop).toIso) ⋯

@[simp]

theorem CategoryTheory.equivYoneda'_hom_val (S : CategoryTheory.SheafOfTypes CategoryTheory.typesGrothendieckTopology) : (CategoryTheory.equivYoneda' S).hom.val = (CategoryTheory.equivYoneda S.val ⋯).hom

@[simp]

theorem CategoryTheory.equivYoneda'_inv_val (S : CategoryTheory.SheafOfTypes CategoryTheory.typesGrothendieckTopology) : (CategoryTheory.equivYoneda' S).inv.val = (CategoryTheory.equivYoneda 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(*)].

Equations

• CategoryTheory.equivYoneda' S = { hom := { val := (CategoryTheory.equivYoneda S.val ⋯).hom }, inv := { val := (CategoryTheory.equivYoneda S.val ⋯).inv }, hom_inv_id := ⋯, inv_hom_id := ⋯ }

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 α (f.val.app (Opposite.op α) s) x = f.val.app (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), (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 : 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), (CategoryTheory.typeEquiv.functor.obj α).val.map 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), 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 : PUnit.{u + 1} ⟶ X) => 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 : Type u) => { obj := fun (Y : Type uᵒᵖ) => Y.unop ⟶ X, map := fun {X_1 Y : Type uᵒᵖ} (f : X_1 ⟶ Y) (g : (fun (Y : Type uᵒᵖ) => Y.unop ⟶ X) X_1) => CategoryTheory.CategoryStruct.comp f.unop g, 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 : (CategoryTheory.yoneda'.comp ((CategoryTheory.sheafOfTypesToPresheaf CategoryTheory.typesGrothendieckTopology).comp ((CategoryTheory.evaluation Type uᵒᵖ (Type u)).obj (Opposite.op 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 : CategoryTheory.SheafOfTypes CategoryTheory.typesGrothendieckTopology) (X : Type uᵒᵖ) : ∀ (a : (CategoryTheory.yoneda.obj (X✝.val.obj (Opposite.op PUnit.{u + 1} ))).obj X), (CategoryTheory.typeEquiv.counitIso.hom.app X✝).val.app X a = (CategoryTheory.evalEquiv 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.

Equations

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

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

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