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.

TODO

• show that both functors of the equivalence overEquivalence U are continuous and induce an equivalence between Sheaf ((Opens.grothendieckTopology X).over U) A and Sheaf (Opens.grothendieckTopology U) A for any category A.

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_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_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_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_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.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_functor_obj {X : Type u} [TopologicalSpace X] (U : Opens X) (V : CategoryTheory.Over U) : ↑(U.overEquivalence.functor.obj V) = Subtype.val ⁻¹' ↑V.left