Opens and Over categories

In this file, given a topological space X, and U : Opens X, we show that the category Over U (whose objects are the V : Opens X equipped with a morphism V ⟶ U) is equivalent to the category Opens U. This equivalence is bi-continuous, and thus induces an equivalence of sheaf categories.

def TopologicalSpace.Opens.overEquivalence {X : Type u} [TopologicalSpace X] (U : Opens X) : CategoryTheory.Over U ≌ Opens ↥U

If X is a topological space and U : Opens X, then the category Over U is equivalent to Opens ↥U.

Equations

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

@[simp]

theorem TopologicalSpace.Opens.coe_overEquivalence_functor_obj {X : Type u} [TopologicalSpace X] (U : Opens X) (V : CategoryTheory.Over U) : ↑(U.overEquivalence.functor.obj V) = Subtype.val ⁻¹' ↑V.left

@[simp]

theorem TopologicalSpace.Opens.overEquivalence_counitIso_inv_app {X : Type u} [TopologicalSpace X] (U : Opens X) (X✝ : Opens ↥U) : U.overEquivalence.counitIso.inv.app X✝ = CategoryTheory.eqToHom ⋯

@[simp]

theorem TopologicalSpace.Opens.coe_overEquivalence_inverse_obj_left {X : Type u} [TopologicalSpace X] (U : Opens X) (W : Opens ↥U) : ↑(U.overEquivalence.inverse.obj W).left = Subtype.val '' ↑W

@[simp]

theorem TopologicalSpace.Opens.overEquivalence_inverse_obj_right_as {X : Type u} [TopologicalSpace X] (U : Opens X) (W : Opens ↥U) : (U.overEquivalence.inverse.obj W).right.as = PUnit.unit

@[simp]

theorem TopologicalSpace.Opens.overEquivalence_unitIso_inv_app_left {X : Type u} [TopologicalSpace X] (U : Opens X) (X✝ : CategoryTheory.Over U) : (U.overEquivalence.unitIso.inv.app X✝).left = CategoryTheory.eqToHom ⋯

@[simp]

theorem TopologicalSpace.Opens.overEquivalence_unitIso_hom_app_left {X : Type u} [TopologicalSpace X] (U : Opens X) (X✝ : CategoryTheory.Over U) : (U.overEquivalence.unitIso.hom.app X✝).left = CategoryTheory.eqToHom ⋯

@[simp]

theorem TopologicalSpace.Opens.overEquivalence_counitIso_hom_app {X : Type u} [TopologicalSpace X] (U : Opens X) (X✝ : Opens ↥U) : U.overEquivalence.counitIso.hom.app X✝ = CategoryTheory.eqToHom ⋯

@[simp]

theorem TopologicalSpace.Opens.mem_overEquivalence_functor_obj {X : Type u} [TopologicalSpace X] {U : Opens X} {V : CategoryTheory.Over U} {x : ↥U} : x ∈ U.overEquivalence.functor.obj V ↔ ↑x ∈ V.left

instance TopologicalSpace.Opens.instIsDenseSubsiteOverSubtypeMemOverGrothendieckTopologyFunctorOverEquivalence {X : Type u} [TopologicalSpace X] (U : Opens X) : CategoryTheory.Functor.IsDenseSubsite ((Opens.grothendieckTopology X).over U) (Opens.grothendieckTopology ↥U) U.overEquivalence.functor

instance TopologicalSpace.Opens.instIsDenseSubsiteOverSubtypeMemOverGrothendieckTopologyInverseSymmOverEquivalence {X : Type u} [TopologicalSpace X] (U : Opens X) : CategoryTheory.Functor.IsDenseSubsite ((Opens.grothendieckTopology X).over U) (Opens.grothendieckTopology ↥U) U.overEquivalence.symm.inverse

instance TopologicalSpace.Opens.instIsDenseSubsiteSubtypeMemOverGrothendieckTopologyOverInverseOverEquivalence {X : Type u} [TopologicalSpace X] (U : Opens X) : CategoryTheory.Functor.IsDenseSubsite (Opens.grothendieckTopology ↥U) ((Opens.grothendieckTopology X).over U) U.overEquivalence.inverse

def TopologicalSpace.Opens.sheafEquivOver {X : Type u} [TopologicalSpace X] (U : Opens X) {A : Type u_1} [CategoryTheory.Category.{v_1, u_1} A] : CategoryTheory.Sheaf ((Opens.grothendieckTopology X).over U) A ≌ CategoryTheory.Sheaf (Opens.grothendieckTopology ↥U) A

Sheaves on the over category of U are equivalent to sheaves on U as a topological space.

Equations

• U.sheafEquivOver = CategoryTheory.Equivalence.sheafCongr ((Opens.grothendieckTopology X).over U) (Opens.grothendieckTopology ↥U) U.overEquivalence A

@[simp]

theorem TopologicalSpace.Opens.sheafEquivOver_inverse_obj_obj_map {X : Type u} [TopologicalSpace X] (U : Opens X) {A : Type u_1} [CategoryTheory.Category.{v_1, u_1} A] (X✝ : CategoryTheory.Sheaf (Opens.grothendieckTopology ↥U) A) {X✝¹ Y✝ : (CategoryTheory.Over U)ᵒᵖ} (f : X✝¹ ⟶ Y✝) : (U.sheafEquivOver.inverse.obj X✝).obj.map f = X✝.obj.map (U.overEquivalence.functor.map f.unop).op

@[simp]

theorem TopologicalSpace.Opens.sheafEquivOver_unitIso_hom_app_hom_app {X : Type u} [TopologicalSpace X] (U : Opens X) {A : Type u_1} [CategoryTheory.Category.{v_1, u_1} A] (X✝ : CategoryTheory.Sheaf ((Opens.grothendieckTopology X).over U) A) (X✝¹ : (CategoryTheory.Over U)ᵒᵖ) : (U.sheafEquivOver.unitIso.hom.app X✝).hom.app X✝¹ = X✝.obj.map (U.overEquivalence.unitIso.inv.app (Opposite.unop X✝¹)).op

@[simp]

theorem TopologicalSpace.Opens.sheafEquivOver_functor_map_hom_app {X : Type u} [TopologicalSpace X] (U : Opens X) {A : Type u_1} [CategoryTheory.Category.{v_1, u_1} A] {X✝ Y✝ : CategoryTheory.Sheaf ((Opens.grothendieckTopology X).over U) A} (f : X✝ ⟶ Y✝) (X✝¹ : (Opens ↥U)ᵒᵖ) : (U.sheafEquivOver.functor.map f).hom.app X✝¹ = f.hom.app (Opposite.op (U.overEquivalence.inverse.obj (Opposite.unop X✝¹)))

@[simp]

theorem TopologicalSpace.Opens.sheafEquivOver_unitIso_inv_app_hom_app {X : Type u} [TopologicalSpace X] (U : Opens X) {A : Type u_1} [CategoryTheory.Category.{v_1, u_1} A] (X✝ : CategoryTheory.Sheaf ((Opens.grothendieckTopology X).over U) A) (X✝¹ : (CategoryTheory.Over U)ᵒᵖ) : (U.sheafEquivOver.unitIso.inv.app X✝).hom.app X✝¹ = X✝.obj.map (U.overEquivalence.unitIso.hom.app (Opposite.unop X✝¹)).op

@[simp]

theorem TopologicalSpace.Opens.sheafEquivOver_functor_obj_obj_map {X : Type u} [TopologicalSpace X] (U : Opens X) {A : Type u_1} [CategoryTheory.Category.{v_1, u_1} A] (X✝ : CategoryTheory.Sheaf ((Opens.grothendieckTopology X).over U) A) {X✝¹ Y✝ : (Opens ↥U)ᵒᵖ} (f : X✝¹ ⟶ Y✝) : (U.sheafEquivOver.functor.obj X✝).obj.map f = X✝.obj.map (U.overEquivalence.inverse.map f.unop).op

@[simp]

theorem TopologicalSpace.Opens.sheafEquivOver_inverse_obj_obj_obj {X : Type u} [TopologicalSpace X] (U : Opens X) {A : Type u_1} [CategoryTheory.Category.{v_1, u_1} A] (X✝ : CategoryTheory.Sheaf (Opens.grothendieckTopology ↥U) A) (X✝¹ : (CategoryTheory.Over U)ᵒᵖ) : (U.sheafEquivOver.inverse.obj X✝).obj.obj X✝¹ = X✝.obj.obj (Opposite.op (U.overEquivalence.functor.obj (Opposite.unop X✝¹)))

@[simp]

theorem TopologicalSpace.Opens.sheafEquivOver_functor_obj_obj_obj {X : Type u} [TopologicalSpace X] (U : Opens X) {A : Type u_1} [CategoryTheory.Category.{v_1, u_1} A] (X✝ : CategoryTheory.Sheaf ((Opens.grothendieckTopology X).over U) A) (X✝¹ : (Opens ↥U)ᵒᵖ) : (U.sheafEquivOver.functor.obj X✝).obj.obj X✝¹ = X✝.obj.obj (Opposite.op (U.overEquivalence.inverse.obj (Opposite.unop X✝¹)))

@[simp]

theorem TopologicalSpace.Opens.sheafEquivOver_counitIso_hom_app_hom_app {X : Type u} [TopologicalSpace X] (U : Opens X) {A : Type u_1} [CategoryTheory.Category.{v_1, u_1} A] (X✝ : CategoryTheory.Sheaf (Opens.grothendieckTopology ↥U) A) (X✝¹ : (Opens ↥U)ᵒᵖ) : (U.sheafEquivOver.counitIso.hom.app X✝).hom.app X✝¹ = X✝.obj.map (CategoryTheory.eqToHom ⋯).op

@[simp]

theorem TopologicalSpace.Opens.sheafEquivOver_inverse_map_hom_app {X : Type u} [TopologicalSpace X] (U : Opens X) {A : Type u_1} [CategoryTheory.Category.{v_1, u_1} A] {X✝ Y✝ : CategoryTheory.Sheaf (Opens.grothendieckTopology ↥U) A} (f : X✝ ⟶ Y✝) (X✝¹ : (CategoryTheory.Over U)ᵒᵖ) : (U.sheafEquivOver.inverse.map f).hom.app X✝¹ = f.hom.app (Opposite.op (U.overEquivalence.functor.obj (Opposite.unop X✝¹)))

@[simp]

theorem TopologicalSpace.Opens.sheafEquivOver_counitIso_inv_app_hom_app {X : Type u} [TopologicalSpace X] (U : Opens X) {A : Type u_1} [CategoryTheory.Category.{v_1, u_1} A] (X✝ : CategoryTheory.Sheaf (Opens.grothendieckTopology ↥U) A) (X✝¹ : (Opens ↥U)ᵒᵖ) : (U.sheafEquivOver.counitIso.inv.app X✝).hom.app X✝¹ = X✝.obj.map (CategoryTheory.eqToHom ⋯).op

def TopologicalSpace.Opens.overPullbackSheafEquivOver {A : Type u_1} [CategoryTheory.Category.{v_1, u_1} A] {X : TopCat} (U : Opens ↑X) : ((Opens.grothendieckTopology ↑X).overPullback A U).comp U.sheafEquivOver.functor ≅ U.sheafRestrict

overPullback and sheafRestrict are isomorphic under sheafEquivOver.

Equations

• U.overPullbackSheafEquivOver = CategoryTheory.Iso.refl (((Opens.grothendieckTopology ↑X).overPullback A U).comp U.sheafEquivOver.functor)

instance TopologicalSpace.Opens.instIsRightAdjointSheafSubtypeCarrierMemGrothendieckTopologySheafRestrictOfOverOverOverPullback {A : Type u_1} [CategoryTheory.Category.{v_1, u_1} A] {X : TopCat} (U : Opens ↑X) [((Opens.grothendieckTopology ↑X).overPullback A U).IsRightAdjoint] : U.sheafRestrict.IsRightAdjoint

def TopologicalSpace.Opens.sheafRestrictSheafEquivOver {A : Type u_1} [CategoryTheory.Category.{v_1, u_1} A] {X : TopCat} (U : Opens ↑X) : U.sheafRestrict.comp U.sheafEquivOver.inverse ≅ (Opens.grothendieckTopology ↑X).overPullback A U

overPullback and sheafRestrict are isomorphic under sheafEquivOver.

Equations

• U.sheafRestrictSheafEquivOver = U.overPullbackSheafEquivOver.isoCompInverse.symm