# 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 : U V) => { x : X // x U }{ x : X // x V }
Equations
• TopologicalSpace.Opens.opensHomHasCoeToFun = { coe := fun (f : U V) (x : { x : X // x U }) => x, }

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.

Equations
• U.infLELeft V = .hom
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.

Equations
• U.infLERight V = .hom
Instances For
noncomputable def TopologicalSpace.Opens.leSupr {X : TopCat} {ι : Type u_1} (U : ) (i : ι) :
U i iSup U

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

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

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

Equations
• U.botLE = .hom
Instances For
noncomputable def TopologicalSpace.Opens.leTop {X : TopCat} (U : ) :

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

Equations
• U.leTop = .hom
Instances For
theorem TopologicalSpace.Opens.infLELeft_apply {X : TopCat} (U : ) (V : ) (x : { x : X // x U V }) :
(fun (x : { x : X // x U V }) => x, ) x = x,
@[simp]
theorem TopologicalSpace.Opens.infLELeft_apply_mk {X : TopCat} (U : ) (V : ) (x : X) (m : x U V) :
(fun (x : { x : X // x U V }) => x, ) x, m = x,
@[simp]
theorem TopologicalSpace.Opens.leSupr_apply_mk {X : TopCat} {ι : Type u_1} (U : ) (i : ι) (x : X) (m : x U i) :
(fun (x : { x : X // x U i }) => x, ) x, m = x,

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem TopologicalSpace.Opens.toTopCat_map (X : TopCat) {U : } {V : } {f : U V} {x : X} {h : x U} :
(.map f) x, h = x,
@[simp]
theorem TopologicalSpace.Opens.inclusion'_apply {X : TopCat} (U : ) :
U.inclusion' = 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.

Equations
• U.inclusion' = { toFun := Subtype.val, continuous_toFun := }
Instances For
@[simp]
theorem TopologicalSpace.Opens.coe_inclusion' {X : TopCat} {U : } :
U.inclusion' = Subtype.val

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

Equations
• = { hom := .inclusion', inv := { toFun := fun (x : X) => x, trivial, continuous_toFun := }, hom_inv_id := , inv_hom_id := }
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.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
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' := }
@[simp]
theorem TopologicalSpace.Opens.map_homOfLE {X : TopCat} {Y : TopCat} (f : X Y) {U : } {V : } (e : U V) :
@[simp]
@[simp]
theorem TopologicalSpace.Opens.map_id_obj' {X : TopCat} (U : Set X) (p : ) :
{ carrier := U, is_open' := p } = { carrier := U, is_open' := p }
@[simp]
theorem TopologicalSpace.Opens.op_map_id_obj {X : TopCat} (U : ) :
U = U
@[simp]
theorem TopologicalSpace.Opens.map_top {X : TopCat} {Y : TopCat} (f : X Y) :
.obj =
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.

Equations
• = U.leTop
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 : ) :
{ 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 (.obj )
@[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 (.obj U)
@[simp]
theorem TopologicalSpace.Opens.mapId_inv_app (X : TopCat) (U : ) :
.inv.app U =
@[simp]
theorem TopologicalSpace.Opens.mapId_hom_app (X : TopCat) (U : ) :
.hom.app U =

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

Equations
• One or more equations did not get rendered due to their size.
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 =
@[simp]
theorem TopologicalSpace.Opens.mapComp_inv_app {X : TopCat} {Y : TopCat} {Z : TopCat} (f : X Y) (g : Y Z) (U : ) :
.inv.app 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.

Equations
• One or more equations did not get rendered due to their size.
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.

Equations
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 =
@[simp]
theorem TopologicalSpace.Opens.mapIso_inv_app {X : TopCat} {Y : TopCat} (f : X Y) (g : X Y) (h : f = g) (U : ) :
.inv.app U =
@[simp]
theorem TopologicalSpace.Opens.mapMapIso_functor {X : TopCat} {Y : TopCat} (H : X Y) :
.functor =
@[simp]
theorem TopologicalSpace.Opens.mapMapIso_unitIso {X : TopCat} {Y : TopCat} (H : X Y) :
.unitIso = CategoryTheory.NatIso.ofComponents (fun (U : ) => )
@[simp]
theorem TopologicalSpace.Opens.mapMapIso_inverse {X : TopCat} {Y : TopCat} (H : X Y) :
.inverse =
@[simp]
theorem TopologicalSpace.Opens.mapMapIso_counitIso {X : TopCat} {Y : TopCat} (H : X Y) :
.counitIso = CategoryTheory.NatIso.ofComponents (fun (U : ) => )

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

TODO: define OrderIso.equivalence, use it.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem IsOpenMap.functor_obj_coe {X : TopCat} {Y : TopCat} {f : X Y} (hf : ) (U : ) :
(hf.functor.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.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def IsOpenMap.adjunction {X : TopCat} {Y : TopCat} {f : X Y} (hf : ) :
hf.functor

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
instance IsOpenMap.functorFullOfMono {X : TopCat} {Y : TopCat} {f : X Y} (hf : ) [H : ] :
hf.functor.Full
Equations
• =
instance IsOpenMap.functor_faithful {X : TopCat} {Y : TopCat} {f : X Y} (hf : ) :
hf.functor.Faithful
Equations
• =
theorem OpenEmbedding.functor_obj_injective {X : TopCat} {Y : TopCat} {f : X Y} (hf : ) :
Function.Injective .functor.obj
@[simp]
theorem TopologicalSpace.Opens.openEmbedding_obj_top {X : TopCat} (U : ) :
.functor.obj = U
@[simp]
theorem TopologicalSpace.Opens.adjunction_counit_app_self {X : TopCat} (U : ) :