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.18) (f : x ⟶ α) => ∃ (x_1 : α), ∀ (y : x), f y = x_1, downward_closed := ⋯ }

@[simp]

theorem CategoryTheory.discreteSieve_apply (α x✝ : Type u) (f : x✝ ⟶ α) : (discreteSieve α).arrows f = ∃ (x : α), ∀ (y : x✝), 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'.

@[deprecated CategoryTheory.Presieve.isSheaf_yoneda' (since := "2024-11-26")]

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

Alias of CategoryTheory.Presieve.isSheaf_yoneda'.

---

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'_map_val {X✝ Y✝ : Type u} (f : X✝ ⟶ Y✝) : (yoneda'.map f).val = yoneda.map f

@[simp]

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

@[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 α)) (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.13 + 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})) : 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 α (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

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

@[simp]

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

@[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 ⋯ α f

theorem CategoryTheory.eval_map (S : Functor Type uᵒᵖ (Type u)) (α β : Type u) (f : β ⟶ α) (s : S.obj (Opposite.op α)) (x : β) : eval S β (S.map f.op s) x = eval S α s (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.36ᵒᵖ) => (CategoryTheory.evalEquiv S hs (Opposite.unop α)).toIso) ⋯

@[simp]

theorem CategoryTheory.equivYoneda_hom_app (S : Functor Type uᵒᵖ (Type u)) (hs : Presheaf.IsSheaf typesGrothendieckTopology S) (X : Type uᵒᵖ) (a✝ : S.obj X) : (equivYoneda S hs).hom.app X a✝ = (evalEquiv S hs (Opposite.unop X)) a✝

@[simp]

theorem CategoryTheory.equivYoneda_inv_app (S : Functor Type uᵒᵖ (Type u)) (hs : Presheaf.IsSheaf typesGrothendieckTopology S) (X : Type uᵒᵖ) (a✝ : (yoneda.obj (S.obj (Opposite.op PUnit.{u + 1}))).obj X) : (equivYoneda S hs).inv.app X a✝ = (evalEquiv S hs (Opposite.unop X)).symm a✝

noncomputable def CategoryTheory.equivYoneda' (S : Sheaf typesGrothendieckTopology (Type u)) : S ≅ yoneda'.obj (S.val.obj (Opposite.op PUnit.{u + 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 := ⋯ }

@[simp]

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

@[simp]

theorem CategoryTheory.equivYoneda'_inv_val (S : Sheaf typesGrothendieckTopology (Type u)) : (equivYoneda' S).inv.val = (equivYoneda S.val ⋯).inv

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

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

yoneda' induces an equivalence of category 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_counitIso_hom_app_val_app (X : Sheaf typesGrothendieckTopology (Type u)) (X✝ : Type uᵒᵖ) (a✝ : (yoneda.obj (X.val.obj (Opposite.op PUnit.{u + 1}))).obj X✝) : (typeEquiv.counitIso.hom.app X).val.app X✝ a✝ = (evalEquiv X.val ⋯ (Opposite.unop X✝)).symm a✝

@[simp]

theorem CategoryTheory.typeEquiv_unitIso_inv_app (X : Type u) (a✝ : (yoneda'.comp ((sheafToPresheaf typesGrothendieckTopology (Type u)).comp ((evaluation Type uᵒᵖ (Type u)).obj (Opposite.op PUnit.{u + 1})))).obj X) : typeEquiv.unitIso.inv.app X a✝ = a✝ PUnit.unit

@[simp]

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

@[simp]

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

@[simp]

theorem CategoryTheory.typeEquiv_unitIso_hom_app (X : Type u) (a✝ : (Functor.id (Type u)).obj X) : typeEquiv.unitIso.hom.app X a✝ = fun (x : PUnit.{u + 1}) => a✝

@[simp]

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

@[simp]

theorem CategoryTheory.typeEquiv_counitIso_inv_app_val_app (X : Sheaf typesGrothendieckTopology (Type u)) (X✝ : Type uᵒᵖ) (a✝ : X.val.obj X✝) : (typeEquiv.counitIso.inv.app X).val.app X✝ a✝ = (evalEquiv X.val ⋯ (Opposite.unop X✝)) a✝

@[simp]

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

@[simp]

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

instance CategoryTheory.subcanonical_typesGrothendieckTopology : typesGrothendieckTopology.Subcanonical

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