# 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 : ) :

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 : ) :

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 : ฮน) :

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
noncomputable def TopologicalSpace.Opens.leMapTop {X : TopCat} {Y : TopCat} (f : X โถ Y) (U : ) :

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 : IsOpenMap โf) (U : ) :
โ(().obj U) = โf '' โU
def IsOpenMap.functor {X : TopCat} {Y : TopCat} {f : X โถ Y} (hf : IsOpenMap โf) :

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 : IsOpenMap โf) :

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 : IsOpenMap โf) [H : ] :
instance IsOpenMap.functor_faithful {X : TopCat} {Y : TopCat} {f : X โถ Y} (hf : IsOpenMap โf) :
@[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 : IsOpenMap โf) (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 : OpenEmbedding โf) (V : ) :
().obj ((IsOpenMap.functor (_ : IsOpenMap โf)).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))