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.opensHom.instFunLike {X : TopCat} {U V : Opens ↑X} : FunLike (U ⟶ V) ↥U ↥V

theorem TopologicalSpace.Opens.apply_def {X : TopCat} {U V : Opens ↑X} (f : U ⟶ V) (x : ↥U) : f x = ⟨↑x, ⋯⟩

@[simp]

theorem TopologicalSpace.Opens.apply_mk {X : TopCat} {U V : Opens ↑X} (f : U ⟶ V) (x : ↑X) (hx : x ∈ U) : f ⟨x, hx⟩ = ⟨x, ⋯⟩

@[simp]

theorem TopologicalSpace.Opens.val_apply {X : TopCat} {U V : Opens ↑X} (f : U ⟶ V) (x : ↥U) : ↑(f x) = ↑x

@[simp]

theorem TopologicalSpace.Opens.coe_id {X : TopCat} {U : Opens ↑X} (f : U ⟶ U) : ⇑f = id

theorem TopologicalSpace.Opens.id_apply {X : TopCat} {U : Opens ↑X} (f : U ⟶ U) (x : ↥U) : f x = x

@[simp]

theorem TopologicalSpace.Opens.comp_apply {X : TopCat} {U V W : Opens ↑X} (f : U ⟶ V) (g : V ⟶ W) (x : ↥U) : (CategoryTheory.CategoryStruct.comp f g) x = g (f x)

We now construct as morphisms various inclusions of open sets.

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

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

noncomputable def TopologicalSpace.Opens.infLERight {X : TopCat} (U V : Opens ↑X) : U ⊓ V ⟶ V

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

noncomputable def TopologicalSpace.Opens.leSupr {X : TopCat} {ι : Type u_1} (U : ι → Opens ↑X) (i : ι) : U i ⟶ iSup U

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

noncomputable def TopologicalSpace.Opens.botLE {X : TopCat} (U : Opens ↑X) : ⊥ ⟶ U

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

noncomputable def TopologicalSpace.Opens.leTop {X : TopCat} (U : Opens ↑X) : U ⟶ ⊤

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

theorem TopologicalSpace.Opens.infLELeft_apply {X : TopCat} (U V : Opens ↑X) (x : ↥(U ⊓ V)) : (U.infLELeft V) x = ⟨↑x, ⋯⟩

@[simp]

theorem TopologicalSpace.Opens.infLELeft_apply_mk {X : TopCat} (U V : Opens ↑X) (x : ↑X) (m : x ∈ U ⊓ V) : (U.infLELeft V) ⟨x, m⟩ = ⟨x, ⋯⟩

@[simp]

theorem TopologicalSpace.Opens.leSupr_apply_mk {X : TopCat} {ι : Type u_1} (U : ι → Opens ↑X) (i : ι) (x : ↑X) (m : x ∈ U i) : (leSupr U i) ⟨x, m⟩ = ⟨x, ⋯⟩

def TopologicalSpace.Opens.toTopCat (X : TopCat) : CategoryTheory.Functor (Opens ↑X) TopCat

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

@[simp]

theorem TopologicalSpace.Opens.toTopCat_map (X : TopCat) {U V : Opens ↑X} {f : U ⟶ V} {x : ↑X} {h : x ∈ U} : (CategoryTheory.ConcreteCategory.hom ((toTopCat X).map f)) ⟨x, h⟩ = ⟨x, ⋯⟩

def TopologicalSpace.Opens.inclusion' {X : TopCat} (U : Opens ↑X) : (toTopCat X).obj U ⟶ X

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

@[simp]

theorem TopologicalSpace.Opens.inclusion'_hom_apply {X : TopCat} (U : Opens ↑X) : ⇑(TopCat.Hom.hom U.inclusion') = Subtype.val

@[simp]

theorem TopologicalSpace.Opens.coe_inclusion' {X : TopCat} {U : Opens ↑X} : ⇑(CategoryTheory.ConcreteCategory.hom U.inclusion') = Subtype.val

theorem TopologicalSpace.Opens.isOpenEmbedding {X : TopCat} (U : Opens ↑X) : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom U.inclusion')

def TopologicalSpace.Opens.inclusionTopIso (X : TopCat) : (toTopCat X).obj ⊤ ≅ X

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

def TopologicalSpace.Opens.map {X Y : TopCat} (f : X ⟶ Y) : CategoryTheory.Functor (Opens ↑Y) (Opens ↑X)

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

@[simp]

theorem TopologicalSpace.Opens.map_coe {X Y : TopCat} (f : X ⟶ Y) (U : Opens ↑Y) : ↑((map f).obj U) = ⇑(CategoryTheory.ConcreteCategory.hom f) ⁻¹' ↑U

@[simp]

theorem TopologicalSpace.Opens.map_obj {X Y : TopCat} (f : X ⟶ Y) (U : Set ↑Y) (p : IsOpen U) : (map f).obj { carrier := U, is_open' := p } = { carrier := ⇑(CategoryTheory.ConcreteCategory.hom f) ⁻¹' U, is_open' := ⋯ }

@[simp]

theorem TopologicalSpace.Opens.map_homOfLE {X Y : TopCat} (f : X ⟶ Y) {U V : Opens ↑Y} (e : U ≤ V) : (map f).map (CategoryTheory.homOfLE e) = CategoryTheory.homOfLE ⋯

@[simp]

theorem TopologicalSpace.Opens.map_id_obj {X : TopCat} (U : Opens ↑X) : (map (CategoryTheory.CategoryStruct.id X)).obj U = U

@[simp]

theorem TopologicalSpace.Opens.map_id_obj' {X : TopCat} (U : Set ↑X) (p : IsOpen U) : (map (CategoryTheory.CategoryStruct.id X)).obj { carrier := U, is_open' := p } = { carrier := U, is_open' := p }

theorem TopologicalSpace.Opens.map_id_obj_unop {X : TopCat} (U : (Opens ↑X)ᵒᵖ) : (map (CategoryTheory.CategoryStruct.id X)).obj (Opposite.unop U) = Opposite.unop U

theorem TopologicalSpace.Opens.op_map_id_obj {X : TopCat} (U : (Opens ↑X)ᵒᵖ) : (map (CategoryTheory.CategoryStruct.id X)).op.obj U = U

@[simp]

theorem TopologicalSpace.Opens.map_top {X Y : TopCat} (f : X ⟶ Y) : (map f).obj ⊤ = ⊤

noncomputable def TopologicalSpace.Opens.leMapTop {X Y : TopCat} (f : X ⟶ Y) (U : Opens ↑X) : U ⟶ (map f).obj ⊤

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

@[simp]

theorem TopologicalSpace.Opens.map_comp_obj {X Y Z : TopCat} (f : X ⟶ Y) (g : Y ⟶ Z) (U : Opens ↑Z) : (map (CategoryTheory.CategoryStruct.comp f g)).obj U = (map f).obj ((map g).obj U)

@[simp]

theorem TopologicalSpace.Opens.map_comp_obj' {X Y Z : TopCat} (f : X ⟶ Y) (g : Y ⟶ Z) (U : Set ↑Z) (p : IsOpen U) : (map (CategoryTheory.CategoryStruct.comp f g)).obj { carrier := U, is_open' := p } = (map f).obj ((map g).obj { carrier := U, is_open' := p })

@[simp]

theorem TopologicalSpace.Opens.map_comp_map {X Y Z : TopCat} (f : X ⟶ Y) (g : Y ⟶ Z) {U V : Opens ↑Z} (i : U ⟶ V) : (map (CategoryTheory.CategoryStruct.comp f g)).map i = (map f).map ((map g).map i)

@[simp]

theorem TopologicalSpace.Opens.map_comp_obj_unop {X Y Z : TopCat} (f : X ⟶ Y) (g : Y ⟶ Z) (U : (Opens ↑Z)ᵒᵖ) : (map (CategoryTheory.CategoryStruct.comp f g)).obj (Opposite.unop U) = (map f).obj ((map g).obj (Opposite.unop U))

@[simp]

theorem TopologicalSpace.Opens.op_map_comp_obj {X Y Z : TopCat} (f : X ⟶ Y) (g : Y ⟶ Z) (U : (Opens ↑Z)ᵒᵖ) : (map (CategoryTheory.CategoryStruct.comp f g)).op.obj U = (map f).op.obj ((map g).op.obj U)

theorem TopologicalSpace.Opens.map_iSup {X Y : TopCat} (f : X ⟶ Y) {ι : Type u_1} (U : ι → Opens ↑Y) : (map f).obj (iSup U) = iSup ((map f).obj ∘ U)

def TopologicalSpace.Opens.mapId (X : TopCat) : map (CategoryTheory.CategoryStruct.id X) ≅ CategoryTheory.Functor.id (Opens ↑X)

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

@[simp]

theorem TopologicalSpace.Opens.mapId_inv_app (X : TopCat) (U : Opens ↑X) : (mapId X).inv.app U = CategoryTheory.eqToHom ⋯

@[simp]

theorem TopologicalSpace.Opens.mapId_hom_app (X : TopCat) (U : Opens ↑X) : (mapId X).hom.app U = CategoryTheory.eqToHom ⋯

theorem TopologicalSpace.Opens.map_id_eq (X : TopCat) : map (CategoryTheory.CategoryStruct.id X) = CategoryTheory.Functor.id (Opens ↑X)

def TopologicalSpace.Opens.mapComp {X Y Z : TopCat} (f : X ⟶ Y) (g : Y ⟶ Z) : map (CategoryTheory.CategoryStruct.comp f g) ≅ (map g).comp (map f)

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

@[simp]

theorem TopologicalSpace.Opens.mapComp_inv_app {X Y Z : TopCat} (f : X ⟶ Y) (g : Y ⟶ Z) (U : Opens ↑Z) : (mapComp f g).inv.app U = CategoryTheory.eqToHom ⋯

@[simp]

theorem TopologicalSpace.Opens.mapComp_hom_app {X Y Z : TopCat} (f : X ⟶ Y) (g : Y ⟶ Z) (U : Opens ↑Z) : (mapComp f g).hom.app U = CategoryTheory.eqToHom ⋯

theorem TopologicalSpace.Opens.map_comp_eq {X Y Z : TopCat} (f : X ⟶ Y) (g : Y ⟶ Z) : map (CategoryTheory.CategoryStruct.comp f g) = (map g).comp (map f)

def TopologicalSpace.Opens.mapIso {X Y : TopCat} (f g : X ⟶ Y) (h : f = g) : map f ≅ map g

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

theorem TopologicalSpace.Opens.map_eq {X Y : TopCat} (f g : X ⟶ Y) (h : f = g) : map f = map g

@[simp]

theorem TopologicalSpace.Opens.mapIso_refl {X Y : TopCat} (f : X ⟶ Y) (h : f = f) : mapIso f f h = CategoryTheory.Iso.refl (map f)

@[simp]

theorem TopologicalSpace.Opens.mapIso_hom_app {X Y : TopCat} (f g : X ⟶ Y) (h : f = g) (U : Opens ↑Y) : (mapIso f g h).hom.app U = CategoryTheory.eqToHom ⋯

@[simp]

theorem TopologicalSpace.Opens.mapIso_inv_app {X Y : TopCat} (f g : X ⟶ Y) (h : f = g) (U : Opens ↑Y) : (mapIso f g h).inv.app U = CategoryTheory.eqToHom ⋯

def TopologicalSpace.Opens.mapMapIso {X Y : TopCat} (H : X ≅ Y) : Opens ↑Y ≌ Opens ↑X

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

TODO: define OrderIso.equivalence, use it.

@[simp]

theorem TopologicalSpace.Opens.mapMapIso_unitIso {X Y : TopCat} (H : X ≅ Y) : (mapMapIso H).unitIso = CategoryTheory.NatIso.ofComponents (fun (U : Opens ↑Y) => CategoryTheory.eqToIso ⋯) ⋯

@[simp]

theorem TopologicalSpace.Opens.mapMapIso_counitIso {X Y : TopCat} (H : X ≅ Y) : (mapMapIso H).counitIso = CategoryTheory.NatIso.ofComponents (fun (U : Opens ↑X) => CategoryTheory.eqToIso ⋯) ⋯

@[simp]

theorem TopologicalSpace.Opens.mapMapIso_inverse {X Y : TopCat} (H : X ≅ Y) : (mapMapIso H).inverse = map H.inv

@[simp]

theorem TopologicalSpace.Opens.mapMapIso_functor {X Y : TopCat} (H : X ≅ Y) : (mapMapIso H).functor = map H.hom

def IsOpenMap.functor {X Y : TopCat} {f : X ⟶ Y} (hf : IsOpenMap ⇑(CategoryTheory.ConcreteCategory.hom f)) : CategoryTheory.Functor (TopologicalSpace.Opens ↑X) (TopologicalSpace.Opens ↑Y)

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

@[simp]

theorem IsOpenMap.coe_functor_obj {X Y : TopCat} {f : X ⟶ Y} (hf : IsOpenMap ⇑(CategoryTheory.ConcreteCategory.hom f)) (U : TopologicalSpace.Opens ↑X) : ↑(hf.functor.obj U) = ⇑(CategoryTheory.ConcreteCategory.hom f) '' ↑U

def IsOpenMap.adjunction {X Y : TopCat} {f : X ⟶ Y} (hf : IsOpenMap ⇑(CategoryTheory.ConcreteCategory.hom f)) : hf.functor ⊣ TopologicalSpace.Opens.map f

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

instance IsOpenMap.functorFullOfMono {X Y : TopCat} {f : X ⟶ Y} (hf : IsOpenMap ⇑(CategoryTheory.ConcreteCategory.hom f)) [H : CategoryTheory.Mono f] : hf.functor.Full

instance IsOpenMap.functor_faithful {X Y : TopCat} {f : X ⟶ Y} (hf : IsOpenMap ⇑(CategoryTheory.ConcreteCategory.hom f)) : hf.functor.Faithful

theorem Topology.IsOpenEmbedding.functor_obj_injective {X Y : TopCat} {f : X ⟶ Y} (hf : IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) : Function.Injective ⋯.functor.obj

def Topology.IsInducing.functorObj {X Y : TopCat} {f : X ⟶ Y} : IsInducing ⇑(CategoryTheory.ConcreteCategory.hom f) → (U : TopologicalSpace.Opens ↑X) → TopologicalSpace.Opens ↑Y

Given an inducing map X ⟶ Y and some U : Opens X, this is the union of all open sets whose preimage is U. This is right adjoint to Opens.map.

theorem Topology.IsInducing.map_functorObj {X Y : TopCat} {f : X ⟶ Y} (hf : IsInducing ⇑(CategoryTheory.ConcreteCategory.hom f)) (U : TopologicalSpace.Opens ↑X) : (TopologicalSpace.Opens.map f).obj (hf.functorObj U) = U

theorem Topology.IsInducing.mem_functorObj_iff {X Y : TopCat} {f : X ⟶ Y} (hf : IsInducing ⇑(CategoryTheory.ConcreteCategory.hom f)) (U : TopologicalSpace.Opens ↑X) {x : ↑X} : (CategoryTheory.ConcreteCategory.hom f) x ∈ hf.functorObj U ↔ x ∈ U

theorem Topology.IsInducing.le_functorObj_iff {X Y : TopCat} {f : X ⟶ Y} (hf : IsInducing ⇑(CategoryTheory.ConcreteCategory.hom f)) {U : TopologicalSpace.Opens ↑X} {V : TopologicalSpace.Opens ↑Y} : V ≤ hf.functorObj U ↔ (TopologicalSpace.Opens.map f).obj V ≤ U

def Topology.IsInducing.opensGI {X Y : TopCat} {f : X ⟶ Y} (hf : IsInducing ⇑(CategoryTheory.ConcreteCategory.hom f)) : GaloisInsertion (TopologicalSpace.Opens.map f).obj hf.functorObj

An inducing map f : X ⟶ Y induces a Galois insertion between Opens Y and Opens X.

def Topology.IsInducing.functor {X Y : TopCat} {f : X ⟶ Y} (hf : IsInducing ⇑(CategoryTheory.ConcreteCategory.hom f)) : CategoryTheory.Functor (TopologicalSpace.Opens ↑X) (TopologicalSpace.Opens ↑Y)

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

@[simp]

theorem Topology.IsInducing.functor_map {X Y : TopCat} {f : X ⟶ Y} (hf : IsInducing ⇑(CategoryTheory.ConcreteCategory.hom f)) {U V : TopologicalSpace.Opens ↑X} (h : U ⟶ V) : hf.functor.map h = CategoryTheory.homOfLE ⋯

@[simp]

theorem Topology.IsInducing.functor_obj {X Y : TopCat} {f : X ⟶ Y} (hf : IsInducing ⇑(CategoryTheory.ConcreteCategory.hom f)) (U : TopologicalSpace.Opens ↑X) : hf.functor.obj U = hf.functorObj U

def Topology.IsInducing.adjunction {X Y : TopCat} {f : X ⟶ Y} (hf : IsInducing ⇑(CategoryTheory.ConcreteCategory.hom f)) : TopologicalSpace.Opens.map f ⊣ hf.functor

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

@[simp]

theorem TopologicalSpace.Opens.isOpenEmbedding_obj_top {X : TopCat} (U : Opens ↑X) : ⋯.functor.obj ⊤ = U

@[simp]

theorem TopologicalSpace.Opens.inclusion'_map_eq_top {X : TopCat} (U : Opens ↑X) : (map U.inclusion').obj U = ⊤

@[simp]

theorem TopologicalSpace.Opens.adjunction_counit_app_self {X : TopCat} (U : Opens ↑X) : ⋯.adjunction.counit.app U = CategoryTheory.eqToHom ⋯

theorem TopologicalSpace.Opens.inclusion'_top_functor (X : TopCat) : ⋯.functor = map (inclusionTopIso X).inv

theorem TopologicalSpace.Opens.functor_obj_map_obj {X Y : TopCat} {f : X ⟶ Y} (hf : IsOpenMap ⇑(CategoryTheory.ConcreteCategory.hom f)) (U : Opens ↑Y) : hf.functor.obj ((map f).obj U) = hf.functor.obj ⊤ ⊓ U

theorem TopologicalSpace.Opens.set_range_inclusion' {X : TopCat} (U : Opens ↑X) : Set.range ⇑(CategoryTheory.ConcreteCategory.hom U.inclusion') = ↑U

@[simp]

theorem TopologicalSpace.Opens.functor_map_eq_inf {X : TopCat} (U V : Opens ↑X) : ⋯.functor.obj ((map U.inclusion').obj V) = V ⊓ U

theorem TopologicalSpace.Opens.map_functor_eq' {X U : TopCat} (f : U ⟶ X) (hf : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) (V : Opens ↑U) : (map f).obj (⋯.functor.obj V) = V

@[simp]

theorem TopologicalSpace.Opens.map_functor_eq {X : TopCat} {U : Opens ↑X} (V : Opens ↥U) : (map U.inclusion').obj (⋯.functor.obj V) = V

@[simp]

theorem TopologicalSpace.Opens.adjunction_counit_map_functor {X : TopCat} {U : Opens ↑X} (V : Opens ↥U) : ⋯.adjunction.counit.app (⋯.functor.obj V) = CategoryTheory.eqToHom ⋯