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.
Equations
- category_theory.types_grothendieck_topology = {sieves := λ (α : Type u) (S : category_theory.sieve α), ∀ (x : α), ⇑S (λ (_x : punit), x), top_mem' := category_theory.types_grothendieck_topology._proof_1, pullback_stable' := category_theory.types_grothendieck_topology._proof_2, transitive' := category_theory.types_grothendieck_topology._proof_3}
The discrete sieve on a type, which only includes arrows whose image is a subsingleton.
Equations
- category_theory.discrete_sieve α = {arrows := λ (β : Type u) (f : β ⟶ α), ∃ (x : α), ∀ (y : β), f y = x, downward_closed' := _}
@[simp]
theorem
category_theory.discrete_sieve_apply
(α β : Type u)
(f : β ⟶ α) :
⇑(category_theory.discrete_sieve α) f = ∃ (x : α), ∀ (y : β), f y = x
The discrete presieve on a type, which only includes arrows whose domain is a singleton.
Equations
- category_theory.discrete_presieve α = λ (β : Type u) (f : β ⟶ α), ∃ (x : β), ∀ (y : β), y = x
@[simp]
The yoneda functor that sends a type to a sheaf over the category of types
@[simp]
def
category_theory.eval
(P : (Type u)ᵒᵖ ⥤ Type u)
(α : Type u)
(s : P.obj (opposite.op α))
(x : α) :
P.obj (opposite.op punit)
Given a presheaf P on the category of types, construct
a map P(α) → (α → P(*)) for all type α.
Equations
- category_theory.eval P α s x = P.map (category_theory.as_hom (λ (_x : punit), x)).op s
noncomputable
def
category_theory.types_glue
(S : (Type u)ᵒᵖ ⥤ Type u)
(hs : category_theory.presieve.is_sheaf category_theory.types_grothendieck_topology S)
(α : Type u)
(f : α → S.obj (opposite.op punit)) :
S.obj (opposite.op α)
Given a sheaf S on the category of types, construct a map
(α → S(*)) → S(α) that is inverse to eval.
Equations
- category_theory.types_glue S hs α f = _.amalgamate (λ (β : Type u) (g : β ⟶ α) (hg : category_theory.discrete_presieve α g), S.map (category_theory.as_hom (λ (x : β), punit.star)).op (f (g (classical.some hg)))) _
theorem
category_theory.eval_types_glue
{S : (Type u)ᵒᵖ ⥤ Type u}
{hs : category_theory.presieve.is_sheaf category_theory.types_grothendieck_topology S}
{α : Type u}
(f : α → S.obj (opposite.op punit)) :
category_theory.eval S α (category_theory.types_glue S hs α f) = f
theorem
category_theory.types_glue_eval
{S : (Type u)ᵒᵖ ⥤ Type u}
{hs : category_theory.presieve.is_sheaf category_theory.types_grothendieck_topology S}
{α : Type u}
(s : S.obj (opposite.op α)) :
category_theory.types_glue S hs α (category_theory.eval S α s) = s
@[simp]
theorem
category_theory.eval_equiv_symm_apply
(S : (Type u)ᵒᵖ ⥤ Type u)
(hs : category_theory.presieve.is_sheaf category_theory.types_grothendieck_topology S)
(α : Type u)
(f : α → S.obj (opposite.op punit)) :
⇑((category_theory.eval_equiv S hs α).symm) f = category_theory.types_glue S hs α f
noncomputable
def
category_theory.eval_equiv
(S : (Type u)ᵒᵖ ⥤ Type u)
(hs : category_theory.presieve.is_sheaf category_theory.types_grothendieck_topology S)
(α : Type u) :
S.obj (opposite.op α) ≃ (α → S.obj (opposite.op punit))
Given a sheaf S, construct an equivalence S(α) ≃ (α → S(*)).
Equations
- category_theory.eval_equiv S hs α = {to_fun := category_theory.eval S α, inv_fun := category_theory.types_glue S hs α, left_inv := _, right_inv := _}
@[simp]
theorem
category_theory.eval_equiv_apply
(S : (Type u)ᵒᵖ ⥤ Type u)
(hs : category_theory.presieve.is_sheaf category_theory.types_grothendieck_topology S)
(α : Type u)
(s : S.obj (opposite.op α))
(x : α) :
⇑(category_theory.eval_equiv S hs α) s x = category_theory.eval S α s x
theorem
category_theory.eval_map
(S : (Type u)ᵒᵖ ⥤ Type u)
(α β : Type u)
(f : β ⟶ α)
(s : S.obj (opposite.op α))
(x : β) :
category_theory.eval S β (S.map f.op s) x = category_theory.eval S α s (f x)
noncomputable
def
category_theory.equiv_yoneda
(S : (Type u)ᵒᵖ ⥤ Type u)
(hs : category_theory.presieve.is_sheaf category_theory.types_grothendieck_topology S) :
S ≅ category_theory.yoneda.obj (S.obj (opposite.op punit))
Given a sheaf S, construct an isomorphism S ≅ [-, S(*)].
Equations
- category_theory.equiv_yoneda S hs = category_theory.nat_iso.of_components (λ (α : (Type u)ᵒᵖ), (category_theory.eval_equiv S hs (opposite.unop α)).to_iso) _
@[simp]
theorem
category_theory.equiv_yoneda_hom_app
(S : (Type u)ᵒᵖ ⥤ Type u)
(hs : category_theory.presieve.is_sheaf category_theory.types_grothendieck_topology S)
(X : (Type u)ᵒᵖ)
(ᾰ : S.obj X) :
(category_theory.equiv_yoneda S hs).hom.app X ᾰ = ⇑(category_theory.eval_equiv S hs (opposite.unop X)) ᾰ
@[simp]
theorem
category_theory.equiv_yoneda_inv_app
(S : (Type u)ᵒᵖ ⥤ Type u)
(hs : category_theory.presieve.is_sheaf category_theory.types_grothendieck_topology S)
(X : (Type u)ᵒᵖ)
(ᾰ : (category_theory.yoneda.obj (S.obj (opposite.op punit))).obj X) :
(category_theory.equiv_yoneda S hs).inv.app X ᾰ = category_theory.types_glue S hs (opposite.unop X) ᾰ
noncomputable
def
category_theory.equiv_yoneda'
(S : category_theory.SheafOfTypes category_theory.types_grothendieck_topology) :
S ≅ category_theory.yoneda'.obj (S.val.obj (opposite.op punit))
Given a sheaf S, construct an isomorphism S ≅ [-, S(*)].
Equations
- category_theory.equiv_yoneda' S = {hom := {val := (category_theory.equiv_yoneda S.val _).hom}, inv := {val := (category_theory.equiv_yoneda S.val _).inv}, hom_inv_id' := _, inv_hom_id' := _}
theorem
category_theory.eval_app
(S₁ S₂ : category_theory.SheafOfTypes category_theory.types_grothendieck_topology)
(f : S₁ ⟶ S₂)
(α : Type u)
(s : S₁.val.obj (opposite.op α))
(x : α) :
category_theory.eval S₂.val α (f.val.app (opposite.op α) s) x = f.val.app (opposite.op punit) (category_theory.eval S₁.val α s x)
yoneda' induces an equivalence of category between Type u and
Sheaf types_grothendieck_topology.
Equations
- category_theory.type_equiv = category_theory.equivalence.mk category_theory.yoneda' (category_theory.SheafOfTypes_to_presheaf category_theory.types_grothendieck_topology ⋙ (category_theory.evaluation (Type u)ᵒᵖ (Type u)).obj (opposite.op punit)) (category_theory.nat_iso.of_components (λ (α : Type u), {hom := λ (x : (𝟭 (Type u)).obj α) (_x : opposite.unop (opposite.op punit)), x, inv := λ (f : (category_theory.yoneda' ⋙ category_theory.SheafOfTypes_to_presheaf category_theory.types_grothendieck_topology ⋙ (category_theory.evaluation (Type u)ᵒᵖ (Type u)).obj (opposite.op punit)).obj α), f punit.star, hom_inv_id' := _, inv_hom_id' := _}) category_theory.type_equiv._proof_3) (category_theory.nat_iso.of_components (λ (S : category_theory.SheafOfTypes category_theory.types_grothendieck_topology), category_theory.equiv_yoneda' S) category_theory.type_equiv._proof_4).symm
@[simp]
theorem
category_theory.type_equiv_counit_iso_inv_app_val_app
(X : category_theory.SheafOfTypes category_theory.types_grothendieck_topology)
(X_1 : (Type u)ᵒᵖ)
(ᾰ : X.val.obj X_1) :
(category_theory.type_equiv.counit_iso.inv.app X).val.app X_1 ᾰ = ⇑(category_theory.eval_equiv X.val _ (opposite.unop X_1)) ᾰ
@[simp]
theorem
category_theory.type_equiv_unit_iso_inv_app
(X : Type u)
(ᾰ : (category_theory.yoneda' ⋙ category_theory.SheafOfTypes_to_presheaf category_theory.types_grothendieck_topology ⋙ (category_theory.evaluation (Type u)ᵒᵖ (Type u)).obj (opposite.op punit)).obj X) :
category_theory.type_equiv.unit_iso.inv.app X ᾰ = category_theory.types_glue (category_theory.yoneda.obj X) _ punit (ᾰ ≫ λ (x : X) (_x : punit), x) punit.star
@[simp]
theorem
category_theory.type_equiv_counit_iso_hom_app_val_app
(X : category_theory.SheafOfTypes category_theory.types_grothendieck_topology)
(X_1 : (Type u)ᵒᵖ)
(ᾰ : (category_theory.yoneda.obj (X.val.obj (opposite.op punit))).obj X_1) :
(category_theory.type_equiv.counit_iso.hom.app X).val.app X_1 ᾰ = category_theory.types_glue X.val _ (opposite.unop X_1) ᾰ
@[simp]
theorem
category_theory.type_equiv_unit_iso_hom_app
(X : Type u)
(ᾰ : (𝟭 (Type u)).obj X) :
category_theory.type_equiv.unit_iso.hom.app X ᾰ = ⇑(category_theory.eval_equiv (category_theory.yoneda.obj X) _ punit) (λ (_x : punit), ᾰ) ≫ λ (f : punit ⟶ X), f punit.star
@[simp]
theorem
category_theory.type_equiv_functor_map_val_app
(α β : Type u)
(f : α ⟶ β)
(Y : (Type u)ᵒᵖ)
(g : {obj := λ (Y : (Type u)ᵒᵖ), opposite.unop Y ⟶ α, map := λ (Y Y' : (Type u)ᵒᵖ) (f : Y ⟶ Y') (g : opposite.unop Y ⟶ α), f.unop ≫ g, map_id' := _, map_comp' := _}.obj Y)
(ᾰ : opposite.unop Y) :
@[simp]
theorem
category_theory.type_equiv_inverse_map
(_x _x_1 : category_theory.SheafOfTypes category_theory.types_grothendieck_topology)
(f : _x ⟶ _x_1)
(ᾰ : ((category_theory.evaluation (Type u)ᵒᵖ (Type u)).obj (opposite.op punit)).obj ((category_theory.SheafOfTypes_to_presheaf category_theory.types_grothendieck_topology).obj _x)) :
category_theory.type_equiv.inverse.map f ᾰ = f.val.app (opposite.op punit) ᾰ
@[simp]
theorem
category_theory.type_equiv_functor_obj_val_obj
(α : Type u)
(Y : (Type u)ᵒᵖ) :
(category_theory.type_equiv.functor.obj α).val.obj Y = (opposite.unop Y ⟶ α)
@[simp]
theorem
category_theory.type_equiv_functor_obj_val_map
(α : Type u)
(Y Y' : (Type u)ᵒᵖ)
(f : Y ⟶ Y')
(g : opposite.unop Y ⟶ α)
(ᾰ : opposite.unop Y') :