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 : TopologicalSpace.Opens ↑X} {V : TopologicalSpace.Opens ↑X} : CoeFun (U ⟶ V) fun (x : U ⟶ V) => ↥U → ↥V

Equations

• TopologicalSpace.Opens.opensHomHasCoeToFun = { coe := fun (f : U ⟶ V) (x : ↥U) => { val := ↑x, property := ⋯ } }

We now construct as morphisms various inclusions of open sets.

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

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

Equations

• TopologicalSpace.Opens.infLELeft U V = LE.le.hom ⋯

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

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

Equations

• TopologicalSpace.Opens.infLERight U V = LE.le.hom ⋯

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

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

Equations

• TopologicalSpace.Opens.leSupr U i = LE.le.hom ⋯

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

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

Equations

• TopologicalSpace.Opens.botLE U = LE.le.hom ⋯

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

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

Equations

• TopologicalSpace.Opens.leTop U = LE.le.hom ⋯

theorem TopologicalSpace.Opens.infLELeft_apply {X : TopCat} (U : TopologicalSpace.Opens ↑X) (V : TopologicalSpace.Opens ↑X) (x : ↥(U ⊓ V)) : (fun (x : ↥(U ⊓ V)) => { val := ↑x, property := ⋯ }) x = { val := ↑x, property := ⋯ }

@[simp]

theorem TopologicalSpace.Opens.infLELeft_apply_mk {X : TopCat} (U : TopologicalSpace.Opens ↑X) (V : TopologicalSpace.Opens ↑X) (x : ↑X) (m : x ∈ U ⊓ V) : (fun (x : ↥(U ⊓ V)) => { val := ↑x, property := ⋯ }) { val := x, property := m } = { val := x, property := ⋯ }

@[simp]

theorem TopologicalSpace.Opens.leSupr_apply_mk {X : TopCat} {ι : Type u_1} (U : ι → TopologicalSpace.Opens ↑X) (i : ι) (x : ↑X) (m : x ∈ U i) : (fun (x : ↥(U i)) => { val := ↑x, property := ⋯ }) { val := x, property := m } = { val := x, property := ⋯ }

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

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.

@[simp]

theorem TopologicalSpace.Opens.toTopCat_map (X : TopCat) {U : TopologicalSpace.Opens ↑X} {V : TopologicalSpace.Opens ↑X} {f : U ⟶ V} {x : ↑X} {h : x ∈ U} : ((TopologicalSpace.Opens.toTopCat X).map f) { val := x, property := h } = { val := x, property := ⋯ }

@[simp]

theorem TopologicalSpace.Opens.inclusion_apply {X : TopCat} (U : TopologicalSpace.Opens ↑X) : ⇑(TopologicalSpace.Opens.inclusion U) = Subtype.val

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

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

Equations

• TopologicalSpace.Opens.inclusion U = { toFun := Subtype.val, continuous_toFun := ⋯ }

@[simp]

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

theorem TopologicalSpace.Opens.openEmbedding {X : TopCat} (U : TopologicalSpace.Opens ↑X) : OpenEmbedding ⇑(TopologicalSpace.Opens.inclusion U)

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

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

Equations

• One or more equations did not get rendered due to their size.

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

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.

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

Equations

• TopologicalSpace.Opens.leMapTop f U = TopologicalSpace.Opens.leTop U

@[simp]

theorem TopologicalSpace.Opens.map_comp_obj {X : TopCat} {Y : TopCat} {Z : TopCat} (f : X ⟶ Y) (g : Y ⟶ Z) (U : TopologicalSpace.Opens ↑Z) : (TopologicalSpace.Opens.map (CategoryTheory.CategoryStruct.comp f g)).obj U = (TopologicalSpace.Opens.map f).obj ((TopologicalSpace.Opens.map g).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 : IsOpen U) : (TopologicalSpace.Opens.map (CategoryTheory.CategoryStruct.comp f g)).obj { carrier := U, is_open' := p } = (TopologicalSpace.Opens.map f).obj ((TopologicalSpace.Opens.map g).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 : TopologicalSpace.Opens ↑Z} {V : TopologicalSpace.Opens ↑Z} (i : U ⟶ V) : (TopologicalSpace.Opens.map (CategoryTheory.CategoryStruct.comp f g)).map i = (TopologicalSpace.Opens.map f).map ((TopologicalSpace.Opens.map g).map i)

@[simp]

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

@[simp]

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

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

@[simp]

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

@[simp]

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

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

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.

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

@[simp]

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

@[simp]

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

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

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.

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

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

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

Equations

• TopologicalSpace.Opens.mapIso f g h = CategoryTheory.NatIso.ofComponents (fun (U : TopologicalSpace.Opens ↑Y) => CategoryTheory.eqToIso ⋯) ⋯

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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.

@[simp]

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

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

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.

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

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.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• ⋯ = ⋯

theorem OpenEmbedding.functor_obj_injective {X : TopCat} {Y : TopCat} {f : X ⟶ Y} (hf : OpenEmbedding ⇑f) : Function.Injective (IsOpenMap.functor ⋯).obj

@[simp]

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

@[simp]

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

@[simp]

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

theorem TopologicalSpace.Opens.inclusion_top_functor (X : TopCat) : IsOpenMap.functor ⋯ = TopologicalSpace.Opens.map (TopologicalSpace.Opens.inclusionTopIso X).inv

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

theorem TopologicalSpace.Opens.set_range_forget_map_inclusion {X : TopCat} (U : TopologicalSpace.Opens ↑X) : Set.range ((CategoryTheory.forget TopCat).map (TopologicalSpace.Opens.inclusion U)) = ↑U

@[simp]

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

theorem TopologicalSpace.Opens.map_functor_eq' {X : TopCat} {U : TopCat} (f : U ⟶ X) (hf : OpenEmbedding ⇑f) (V : TopologicalSpace.Opens ↑U) : (TopologicalSpace.Opens.map f).obj ((IsOpenMap.functor ⋯).obj V) = V

@[simp]

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

@[simp]

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