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 : TopologicalSpace.Opens โ†‘X} {V : TopologicalSpace.Opens โ†‘X} :
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 : TopologicalSpace.Opens โ†‘X) (V : TopologicalSpace.Opens โ†‘X) :

The inclusion U โŠ“ V โŸถ U as a morphism in the category of open sets.

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

    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 : ฮน โ†’ TopologicalSpace.Opens โ†‘X) (i : ฮน) :

      The inclusion U i โŸถ supr U as a morphism in the category of open sets.

      Instances For

        The inclusion โŠฅ โŸถ U as a morphism in the category of open sets.

        Instances For

          The inclusion U โŸถ โŠค as a morphism in the category of open sets.

          Instances For
            theorem TopologicalSpace.Opens.infLELeft_apply {X : TopCat} (U : TopologicalSpace.Opens โ†‘X) (V : TopologicalSpace.Opens โ†‘X) (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 : TopologicalSpace.Opens โ†‘X) (V : TopologicalSpace.Opens โ†‘X) (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 : ฮน โ†’ TopologicalSpace.Opens โ†‘X) (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 : 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 := (_ : x โˆˆ โ†‘V) }

              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

                  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 : 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' := (_ : IsOpen (โ†‘f โปยน' 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 }

                    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 : 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 })
                      theorem TopologicalSpace.Opens.map_iSup {X : TopCat} {Y : TopCat} (f : X โŸถ Y) {ฮน : Type u_1} (U : ฮน โ†’ TopologicalSpace.Opens โ†‘Y) :

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

                      Instances For

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

                        Instances For

                          If two continuous maps f g : X โŸถ Y are equal, then the functors Opens Y โฅค Opens X they induce are isomorphic.

                          Instances For
                            @[simp]
                            theorem TopologicalSpace.Opens.mapMapIso_unitIso {X : TopCat} {Y : TopCat} (H : X โ‰… Y) :
                            (TopologicalSpace.Opens.mapMapIso H).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) :
                            (TopologicalSpace.Opens.mapMapIso H).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)

                            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 : TopologicalSpace.Opens โ†‘X) :
                              โ†‘((IsOpenMap.functor hf).obj U) = โ†‘f '' โ†‘U

                              An open map f : X โŸถ Y induces a functor Opens X โฅค Opens Y.

                              Instances For

                                An open map f : X โŸถ Y induces an adjunction between Opens X and Opens Y.

                                Instances For
                                  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 (_ : IsOpenMap โ†‘f)).obj V) = V