# Documentation

Mathlib.Topology.Category.TopCat.Opens

# The category of open sets in a topological space. #

We define toTopCat : Opens X ⥤ TopCat and map (f : X ⟶ Y) : Opens Y ⥤ Opens X, given by taking preimages of open sets.

Unfortunately Opens isn't (usefully) a functor TopCat ⥤ Cat. (One can in fact define such a functor, but using it results in unresolvable Eq.rec terms in goals.)

Really it's a 2-functor from (spaces, continuous functions, equalities) to (categories, functors, natural isomorphisms). We don't attempt to set up the full theory here, but do provide the natural isomorphisms mapId : map (𝟙 X) ≅ 𝟭 (opens X) and mapComp : map (f ≫ g) ≅ map g ⋙ map f.

Beyond that, there's a collection of simp lemmas for working with these constructions.

Since Opens X has a partial order, it automatically receives a Category instance. Unfortunately, because we do not allow morphisms in Prop, the morphisms U ⟶ V are not just proofs U ≤ V, but rather ULift (PLift (U ≤ V)).

instance TopologicalSpace.Opens.opensHomHasCoeToFun {X : TopCat} {U : } {V : } :
CoeFun (U V) fun x => { x // x U }{ x // x V }

We now construct as morphisms various inclusions of open sets.

noncomputable def TopologicalSpace.Opens.infLELeft {X : TopCat} (U : ) (V : ) :
U V U

The inclusion U ⊓ V ⟶ U as a morphism in the category of open sets.

Instances For
noncomputable def TopologicalSpace.Opens.infLERight {X : TopCat} (U : ) (V : ) :
U V V

The inclusion U ⊓ V ⟶ V as a morphism in the category of open sets.

Instances For
noncomputable def TopologicalSpace.Opens.leSupr {X : TopCat} {ι : Type u_1} (U : ) (i : ι) :
U i iSup U

The inclusion U i ⟶ supr U as a morphism in the category of open sets.

Instances For
noncomputable def TopologicalSpace.Opens.botLE {X : TopCat} (U : ) :

The inclusion ⊥ ⟶ U as a morphism in the category of open sets.

Instances For
noncomputable def TopologicalSpace.Opens.leTop {X : TopCat} (U : ) :

The inclusion U ⟶ ⊤ as a morphism in the category of open sets.

Instances For
theorem TopologicalSpace.Opens.infLELeft_apply {X : TopCat} (U : ) (V : ) (x : { x // x U V }) :
(fun x => { val := x, property := (_ : x U) }) x = { val := x, property := (_ : x U) }
@[simp]
theorem TopologicalSpace.Opens.infLELeft_apply_mk {X : TopCat} (U : ) (V : ) (x : X) (m : x U V) :
(fun x => { val := x, property := (_ : x U) }) { val := x, property := m } = { val := x, property := (_ : x U) }
@[simp]
theorem TopologicalSpace.Opens.leSupr_apply_mk {X : TopCat} {ι : Type u_1} (U : ) (i : ι) (x : X) (m : x U i) :
(fun x => { val := x, property := (_ : x ↑(iSup U)) }) { val := x, property := m } = { val := x, property := (_ : x ↑(iSup U)) }

The functor from open sets in X to Top, realising each open set as a topological space itself.

Instances For
@[simp]
theorem TopologicalSpace.Opens.toTopCat_map (X : TopCat) {U : } {V : } {f : U V} {x : X} {h : x U} :
↑(().map f) { val := x, property := h } = { val := x, property := (_ : x V) }
@[simp]
theorem TopologicalSpace.Opens.inclusion_apply {X : TopCat} (U : ) :
= Subtype.val
def TopologicalSpace.Opens.inclusion {X : TopCat} (U : ) :
().obj U X

The inclusion map from an open subset to the whole space, as a morphism in TopCat.

Instances For

The inclusion of the top open subset (i.e. the whole space) is an isomorphism.

Instances For
def TopologicalSpace.Opens.map {X : TopCat} {Y : TopCat} (f : X Y) :

Opens.map f gives the functor from open sets in Y to open set in X, given by taking preimages under f.

Instances For
theorem TopologicalSpace.Opens.map_coe {X : TopCat} {Y : TopCat} (f : X Y) (U : ) :
↑(().obj U) = f ⁻¹' U
@[simp]
theorem TopologicalSpace.Opens.map_obj {X : TopCat} {Y : TopCat} (f : X Y) (U : Set Y) (p : ) :
().obj { carrier := U, is_open' := p } = { carrier := f ⁻¹' U, is_open' := (_ : IsOpen (f ⁻¹' U)) }
@[simp]
@[simp]
theorem TopologicalSpace.Opens.map_id_obj' {X : TopCat} (U : Set X) (p : ) :
().obj { carrier := U, is_open' := p } = { carrier := U, is_open' := p }
@[simp]
theorem TopologicalSpace.Opens.map_id_obj_unop {X : TopCat} (U : ) :
().obj U.unop = U.unop
@[simp]
theorem TopologicalSpace.Opens.op_map_id_obj {X : TopCat} (U : ) :
.obj U = U
noncomputable def TopologicalSpace.Opens.leMapTop {X : TopCat} {Y : TopCat} (f : X Y) (U : ) :
U ().obj

The inclusion U ⟶ (map f).obj ⊤ as a morphism in the category of open sets.

Instances For
@[simp]
theorem TopologicalSpace.Opens.map_comp_obj {X : TopCat} {Y : TopCat} {Z : TopCat} (f : X Y) (g : Y Z) (U : ) :
= ().obj (().obj U)
@[simp]
theorem TopologicalSpace.Opens.map_comp_obj' {X : TopCat} {Y : TopCat} {Z : TopCat} (f : X Y) (g : Y Z) (U : Set Z) (p : ) :
().obj { carrier := U, is_open' := p } = ().obj (().obj { carrier := U, is_open' := p })
@[simp]
theorem TopologicalSpace.Opens.map_comp_map {X : TopCat} {Y : TopCat} {Z : TopCat} (f : X Y) (g : Y Z) {U : } {V : } (i : U V) :
= ().map (().map i)
@[simp]
theorem TopologicalSpace.Opens.map_comp_obj_unop {X : TopCat} {Y : TopCat} {Z : TopCat} (f : X Y) (g : Y Z) (U : ) :
().obj U.unop = ().obj (().obj U.unop)
@[simp]
theorem TopologicalSpace.Opens.op_map_comp_obj {X : TopCat} {Y : TopCat} {Z : TopCat} (f : X Y) (g : Y Z) (U : ) :
.obj U = ().op.obj (().op.obj U)
theorem TopologicalSpace.Opens.map_iSup {X : TopCat} {Y : TopCat} (f : X Y) {ι : Type u_1} (U : ) :
().obj (iSup U) = iSup (().toPrefunctor.obj U)
@[simp]
theorem TopologicalSpace.Opens.mapId_inv_app (X : TopCat) (U : ) :
().inv.app U = CategoryTheory.eqToHom (_ : )
@[simp]
theorem TopologicalSpace.Opens.mapId_hom_app (X : TopCat) (U : ) :
().hom.app U = CategoryTheory.eqToHom (_ : )

The functor Opens X ⥤ Opens X given by taking preimages under the identity function is naturally isomorphic to the identity functor.

Instances For
@[simp]
theorem TopologicalSpace.Opens.mapComp_hom_app {X : TopCat} {Y : TopCat} {Z : TopCat} (f : X Y) (g : Y Z) (U : ) :
().hom.app U = CategoryTheory.eqToHom (_ : = ().obj (().obj U))
@[simp]
theorem TopologicalSpace.Opens.mapComp_inv_app {X : TopCat} {Y : TopCat} {Z : TopCat} (f : X Y) (g : Y Z) (U : ) :
().inv.app U = CategoryTheory.eqToHom (_ : ().obj (().obj U) = )
def TopologicalSpace.Opens.mapComp {X : TopCat} {Y : TopCat} {Z : TopCat} (f : X Y) (g : Y Z) :

The natural isomorphism between taking preimages under f ≫ g, and the composite of taking preimages under g, then preimages under f.

Instances For
theorem TopologicalSpace.Opens.map_comp_eq {X : TopCat} {Y : TopCat} {Z : TopCat} (f : X Y) (g : Y Z) :
def TopologicalSpace.Opens.mapIso {X : TopCat} {Y : TopCat} (f : X Y) (g : X Y) (h : f = g) :

If two continuous maps f g : X ⟶ Y are equal, then the functors Opens Y ⥤ Opens X they induce are isomorphic.

Instances For
theorem TopologicalSpace.Opens.map_eq {X : TopCat} {Y : TopCat} (f : X Y) (g : X Y) (h : f = g) :
@[simp]
theorem TopologicalSpace.Opens.mapIso_refl {X : TopCat} {Y : TopCat} (f : X Y) (h : f = f) :
@[simp]
theorem TopologicalSpace.Opens.mapIso_hom_app {X : TopCat} {Y : TopCat} (f : X Y) (g : X Y) (h : f = g) (U : ) :
().hom.app U = CategoryTheory.eqToHom (_ : ().obj U = ().obj U)
@[simp]
theorem TopologicalSpace.Opens.mapIso_inv_app {X : TopCat} {Y : TopCat} (f : X Y) (g : X Y) (h : f = g) (U : ) :
().inv.app U = CategoryTheory.eqToHom (_ : ().obj U = ().obj U)
@[simp]
theorem TopologicalSpace.Opens.mapMapIso_unitIso {X : TopCat} {Y : TopCat} (H : X Y) :
().unitIso = CategoryTheory.NatIso.ofComponents fun U => CategoryTheory.eqToIso (_ : U = { carrier := H.inv ⁻¹' ↑((CategoryTheory.Functor.mk { obj := fun U => { carrier := H.hom ⁻¹' U, is_open' := (_ : IsOpen (H.hom ⁻¹' U)) }, map := fun {X Y} i => { down := { down := (_ : ∀ (x : X), x ↑((fun U => { carrier := H.hom ⁻¹' U, is_open' := (_ : IsOpen (H.hom ⁻¹' U)) }) X)H.hom x Y) } } }).obj U), is_open' := (_ : IsOpen (H.inv ⁻¹' ↑((CategoryTheory.Functor.mk { obj := fun U => { carrier := H.hom ⁻¹' U, is_open' := (_ : IsOpen (H.hom ⁻¹' U)) }, map := fun {X Y} i => { down := { down := (_ : ∀ (x : X), x ↑((fun U => { carrier := H.hom ⁻¹' U, is_open' := (_ : IsOpen (H.hom ⁻¹' U)) }) X)H.hom x Y) } } }).obj U))) })
@[simp]
theorem TopologicalSpace.Opens.mapMapIso_counitIso {X : TopCat} {Y : TopCat} (H : X Y) :
().counitIso = CategoryTheory.NatIso.ofComponents fun U => CategoryTheory.eqToIso (_ : { carrier := H.hom ⁻¹' ↑((CategoryTheory.Functor.mk { obj := fun U => { carrier := H.inv ⁻¹' U, is_open' := (_ : IsOpen (H.inv ⁻¹' U)) }, map := fun {X Y} i => { down := { down := (_ : ∀ (x : Y), x ↑((fun U => { carrier := H.inv ⁻¹' U, is_open' := (_ : IsOpen (H.inv ⁻¹' U)) }) X)H.inv x Y) } } }).obj U), is_open' := (_ : IsOpen (H.hom ⁻¹' ↑((CategoryTheory.Functor.mk { obj := fun U => { carrier := H.inv ⁻¹' U, is_open' := (_ : IsOpen (H.inv ⁻¹' U)) }, map := fun {X Y} i => { down := { down := (_ : ∀ (x : Y), x ↑((fun U => { carrier := H.inv ⁻¹' U, is_open' := (_ : IsOpen (H.inv ⁻¹' U)) }) X)H.inv x Y) } } }).obj U))) } = U)
@[simp]
theorem TopologicalSpace.Opens.mapMapIso_functor {X : TopCat} {Y : TopCat} (H : X Y) :
().functor =
@[simp]
theorem TopologicalSpace.Opens.mapMapIso_inverse {X : TopCat} {Y : TopCat} (H : X Y) :
().inverse =

A homeomorphism of spaces gives an equivalence of categories of open sets.

TODO: define OrderIso.equivalence, use it.

Instances For
@[simp]
theorem IsOpenMap.functor_obj_coe {X : TopCat} {Y : TopCat} {f : X Y} (hf : ) (U : ) :
↑(().obj U) = f '' U
def IsOpenMap.functor {X : TopCat} {Y : TopCat} {f : X Y} (hf : ) :

An open map f : X ⟶ Y induces a functor Opens X ⥤ Opens Y.

Instances For
def IsOpenMap.adjunction {X : TopCat} {Y : TopCat} {f : X Y} (hf : ) :

An open map f : X ⟶ Y induces an adjunction between Opens X and Opens Y.

Instances For
instance IsOpenMap.functorFullOfMono {X : TopCat} {Y : TopCat} {f : X Y} (hf : ) [H : ] :
instance IsOpenMap.functor_faithful {X : TopCat} {Y : TopCat} {f : X Y} (hf : ) :
@[simp]
@[simp]
theorem TopologicalSpace.Opens.adjunction_counit_app_self {X : TopCat} (U : ) :
().counit.app U = CategoryTheory.eqToHom (_ : ().obj () = U)
theorem TopologicalSpace.Opens.functor_obj_map_obj {X : TopCat} {Y : TopCat} {f : X Y} (hf : ) (U : ) :
().obj (().obj U) = ().obj U
@[simp]
theorem TopologicalSpace.Opens.functor_map_eq_inf {X : TopCat} (U : ) (V : ) :
().obj () = V U
theorem TopologicalSpace.Opens.map_functor_eq' {X : TopCat} {U : TopCat} (f : U X) (hf : ) (V : ) :
().obj ((IsOpenMap.functor (_ : )).obj V) = V
@[simp]
theorem TopologicalSpace.Opens.map_functor_eq {X : TopCat} {U : } (V : TopologicalSpace.Opens { x // x U }) :
().obj (().obj V) = V
@[simp]
theorem TopologicalSpace.Opens.adjunction_counit_map_functor {X : TopCat} {U : } (V : TopologicalSpace.Opens { x // x U }) :
().counit.app (().obj V) = CategoryTheory.eqToHom (_ : (CategoryTheory.Functor.comp () ()).obj (().obj V) = ().obj (().obj V))