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 : 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.

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

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

Equations

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

@[simp]

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

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

def CategoryTheory.discretePresieve (α : Type u) : 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) : Sieve.generate (discretePresieve α) ∈ typesGrothendieckTopology α

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

The sheaf condition for yoneda'.

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

The sheaf condition for yoneda'.

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

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'_obj_obj (α : Type u) : (yoneda'.obj α).obj = yoneda.obj α

@[simp]

theorem CategoryTheory.yoneda'_map_hom {X✝ Y✝ : Type u} (f : X✝ ⟶ Y✝) : (yoneda'.map f).hom = yoneda.map f

@[simp]

theorem CategoryTheory.yoneda'_comp : yoneda'.comp (sheafToPresheaf typesGrothendieckTopology (Type u)) = yoneda

def CategoryTheory.eval (P : Functor Type uᵒᵖ (Type u)) (α : Type u) (s : P.obj (Opposite.op α)) : α ⟶ 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 = TypeCat.ofHom fun (x : α) => (CategoryTheory.ConcreteCategory.hom (P.map (TypeCat.ofHom fun (x_1 : PUnit.{?u.1 + 1}) => x).op)) s

noncomputable def CategoryTheory.typesGlue (S : Functor Type uᵒᵖ (Type u)) (hs : Presieve.IsSheaf 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 : Functor Type uᵒᵖ (Type u)} {hs : Presieve.IsSheaf typesGrothendieckTopology S} {α : Type u} (f : α → S.obj (Opposite.op PUnit.{u + 1})) : ⇑(ConcreteCategory.hom (eval S α (typesGlue S hs α f))) = f

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

noncomputable def CategoryTheory.evalEquiv (S : Functor Type uᵒᵖ (Type u)) (hs : Presheaf.IsSheaf 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

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

@[simp]

theorem CategoryTheory.evalEquiv_symm_apply (S : Functor Type uᵒᵖ (Type u)) (hs : Presheaf.IsSheaf typesGrothendieckTopology S) (α : Type u) (f : α ⟶ S.obj (Opposite.op PUnit.{u + 1})) : (evalEquiv S hs α).symm f = typesGlue S ⋯ α ⇑(ConcreteCategory.hom f)

@[simp]

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

theorem CategoryTheory.eval_map (S : Functor Type uᵒᵖ (Type u)) (α β : Type u) (f : β ⟶ α) (s : (fun (X : Type u) => X) (S.obj (Opposite.op α))) (x : (fun (X : Type u) => X) β) : (ConcreteCategory.hom (eval S β ((ConcreteCategory.hom (S.map f.op)) s))) x = (ConcreteCategory.hom (eval S α s)) ((ConcreteCategory.hom f) x)

noncomputable def CategoryTheory.equivYoneda (S : Functor Type uᵒᵖ (Type u)) (hs : Presheaf.IsSheaf typesGrothendieckTopology S) : S ≅ 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.1ᵒᵖ) => (CategoryTheory.evalEquiv S hs (Opposite.unop α)).toIso) ⋯

@[simp]

theorem CategoryTheory.equivYoneda_inv_app_hom_apply (S : Functor Type uᵒᵖ (Type u)) (hs : Presheaf.IsSheaf typesGrothendieckTopology S) (X : Type uᵒᵖ) (x : Opposite.unop X ⟶ S.obj (Opposite.op PUnit.{u + 1})) : (ConcreteCategory.hom ((equivYoneda S hs).inv.app X)) x = (evalEquiv S hs (Opposite.unop X)).symm x

@[simp]

theorem CategoryTheory.equivYoneda_hom_app_hom_apply_hom_apply (S : Functor Type uᵒᵖ (Type u)) (hs : Presheaf.IsSheaf typesGrothendieckTopology S) (X : Type uᵒᵖ) (x : S.obj (Opposite.op (Opposite.unop X))) (x✝ : Opposite.unop X) : (ConcreteCategory.hom ((ConcreteCategory.hom ((equivYoneda S hs).hom.app X)) x)) x✝ = (ConcreteCategory.hom (S.map (TypeCat.ofHom fun (x : PUnit.{u + 1}) => x✝).op)) x

noncomputable def CategoryTheory.equivYoneda' (S : Sheaf typesGrothendieckTopology (Type u)) : S ≅ yoneda'.obj (S.obj.obj (Opposite.op PUnit.{u + 1}))

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

Equations

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

@[simp]

theorem CategoryTheory.equivYoneda'_inv_hom (S : Sheaf typesGrothendieckTopology (Type u)) : (equivYoneda' S).inv.hom = (equivYoneda S.obj ⋯).inv

@[simp]

theorem CategoryTheory.equivYoneda'_hom_hom (S : Sheaf typesGrothendieckTopology (Type u)) : (equivYoneda' S).hom.hom = (equivYoneda S.obj ⋯).hom

theorem CategoryTheory.eval_app (S₁ S₂ : Sheaf typesGrothendieckTopology (Type u)) (f : S₁ ⟶ S₂) (α : Type u) (s : S₁.obj.obj (Opposite.op α)) (x : α) : (ConcreteCategory.hom (eval S₂.obj α ((ConcreteCategory.hom (f.hom.app (Opposite.op α))) s))) x = (ConcreteCategory.hom (f.hom.app (Opposite.op PUnit.{u + 1}))) ((ConcreteCategory.hom (eval S₁.obj α s)) x)

noncomputable def CategoryTheory.typeEquiv : Type u ≌ Sheaf typesGrothendieckTopology (Type u)

yoneda' induces an equivalence of categories between Type u and Sheaf typesGrothendieckTopology (Type u).

Equations

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

@[simp]

theorem CategoryTheory.typeEquiv_unitIso_hom_app_hom_apply_hom_apply (X : Type u) (x : X) (x✝ : PUnit.{u + 1}) : (ConcreteCategory.hom ((ConcreteCategory.hom (typeEquiv.unitIso.hom.app X)) x)) x✝ = x

@[simp]

theorem CategoryTheory.typeEquiv_counitIso_inv_app_hom_app_hom_apply_hom_apply (X : Sheaf typesGrothendieckTopology (Type u)) (X✝ : Type uᵒᵖ) (x : X.obj.obj (Opposite.op (Opposite.unop X✝))) (x✝ : Opposite.unop X✝) : (ConcreteCategory.hom ((ConcreteCategory.hom ((typeEquiv.counitIso.inv.app X).hom.app X✝)) x)) x✝ = (ConcreteCategory.hom (X.obj.map (TypeCat.ofHom fun (x : PUnit.{u + 1}) => x✝).op)) x

@[simp]

theorem CategoryTheory.typeEquiv_functor_map_hom_app_hom_apply_hom_apply {X✝ Y✝ : Type u} (f : X✝ ⟶ Y✝) (x✝ : Type uᵒᵖ) (g : { obj := fun (Y : Type uᵒᵖ) => Opposite.unop Y ⟶ X✝, map := fun {X Y : Type uᵒᵖ} (f : X ⟶ Y) => TypeCat.ofHom fun (g : Opposite.unop X ⟶ X✝) => CategoryStruct.comp f.unop g, map_id := ⋯, map_comp := ⋯ }.obj x✝) (a✝ : Opposite.unop x✝) : (ConcreteCategory.hom ((ConcreteCategory.hom ((typeEquiv.functor.map f).hom.app x✝)) g)) a✝ = f.hom' (g.hom' a✝)

@[simp]

theorem CategoryTheory.typeEquiv_inverse_map {X✝ Y✝ : Sheaf typesGrothendieckTopology (Type u)} (f : X✝ ⟶ Y✝) : typeEquiv.inverse.map f = f.hom.app (Opposite.op PUnit.{u + 1})

@[simp]

theorem CategoryTheory.typeEquiv_counitIso_hom_app_hom_app_hom_apply (X : Sheaf typesGrothendieckTopology (Type u)) (X✝ : Type uᵒᵖ) (x : Opposite.unop X✝ ⟶ X.obj.obj (Opposite.op PUnit.{u + 1})) : (ConcreteCategory.hom ((typeEquiv.counitIso.hom.app X).hom.app X✝)) x = (evalEquiv X.obj ⋯ (Opposite.unop X✝)).symm x

@[simp]

theorem CategoryTheory.typeEquiv_functor_obj_obj_map_hom_apply_hom_apply (α : Type u) {X✝ Y✝ : Type uᵒᵖ} (f : X✝ ⟶ Y✝) (g : Opposite.unop X✝ ⟶ α) (a✝ : Opposite.unop Y✝) : (ConcreteCategory.hom ((ConcreteCategory.hom ((typeEquiv.functor.obj α).obj.map f)) g)) a✝ = g.hom' (f.unop.hom' a✝)

@[simp]

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

@[simp]

theorem CategoryTheory.typeEquiv_unitIso_inv_app_hom_apply (X : Type u) (f : PUnit.{u + 1} ⟶ X) : (ConcreteCategory.hom (typeEquiv.unitIso.inv.app X)) f = (TypeCat.Hom.hom f) PUnit.unit

@[simp]

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

instance CategoryTheory.subcanonical_typesGrothendieckTopology : typesGrothendieckTopology.Subcanonical

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