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

We now construct as morphisms various inclusions of open sets.

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

Equations
  • U.infLELeft V = .hom
Instances For

    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 : ιTopologicalSpace.Opens X) (i : ι) :
      U i iSup U

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

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

        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 : TopologicalSpace.Opens X) :

          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 : TopologicalSpace.Opens X) (V : TopologicalSpace.Opens X) (x : (U V)) :
            (fun (x : (U V)) => x, ) x = x,
            @[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)) => x, ) x, m = x,
            @[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)) => 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 : TopologicalSpace.Opens X} {V : TopologicalSpace.Opens X} {f : U V} {x : X} {h : x U} :
              ((TopologicalSpace.Opens.toTopCat X).map f) x, h = x,
              @[simp]
              theorem TopologicalSpace.Opens.inclusion_apply {X : TopCat} (U : TopologicalSpace.Opens X) :
              U.inclusion = Subtype.val

              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 : TopologicalSpace.Opens X} :
                U.inclusion = Subtype.val

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

                Equations
                Instances For

                  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 : 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 : Set X) (p : IsOpen U) :
                    (TopologicalSpace.Opens.map (CategoryTheory.CategoryStruct.id X)).obj { carrier := U, is_open' := p } = { carrier := U, is_open' := p }
                    noncomputable def TopologicalSpace.Opens.leMapTop {X : TopCat} {Y : TopCat} (f : X Y) (U : TopologicalSpace.Opens X) :

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

                    Equations
                    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.

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

                        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

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

                          Equations
                          Instances For
                            @[simp]
                            theorem TopologicalSpace.Opens.mapIso_hom_app {X : TopCat} {Y : TopCat} (f : X Y) (g : X Y) (h : f = g) (U : TopologicalSpace.Opens Y) :
                            @[simp]
                            theorem TopologicalSpace.Opens.mapIso_inv_app {X : TopCat} {Y : TopCat} (f : X Y) (g : X Y) (h : f = g) (U : TopologicalSpace.Opens Y) :

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

                              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 : IsOpenMap 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.
                                Instances For
                                  instance IsOpenMap.functorFullOfMono {X : TopCat} {Y : TopCat} {f : X Y} (hf : IsOpenMap f) [H : CategoryTheory.Mono f] :
                                  hf.functor.Full
                                  Equations
                                  • =
                                  instance IsOpenMap.functor_faithful {X : TopCat} {Y : TopCat} {f : X Y} (hf : IsOpenMap f) :
                                  hf.functor.Faithful
                                  Equations
                                  • =
                                  theorem OpenEmbedding.functor_obj_injective {X : TopCat} {Y : TopCat} {f : X Y} (hf : OpenEmbedding f) :
                                  Function.Injective .functor.obj
                                  @[simp]
                                  theorem TopologicalSpace.Opens.functor_obj_map_obj {X : TopCat} {Y : TopCat} {f : X Y} (hf : IsOpenMap f) (U : TopologicalSpace.Opens Y) :
                                  hf.functor.obj ((TopologicalSpace.Opens.map f).obj U) = hf.functor.obj U
                                  @[simp]
                                  theorem TopologicalSpace.Opens.functor_map_eq_inf {X : TopCat} (U : TopologicalSpace.Opens X) (V : TopologicalSpace.Opens X) :
                                  .functor.obj ((TopologicalSpace.Opens.map U.inclusion).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 (.functor.obj V) = V
                                  @[simp]
                                  theorem TopologicalSpace.Opens.map_functor_eq {X : TopCat} {U : TopologicalSpace.Opens X} (V : TopologicalSpace.Opens U) :
                                  (TopologicalSpace.Opens.map U.inclusion).obj (.functor.obj V) = V
                                  @[simp]
                                  theorem TopologicalSpace.Opens.adjunction_counit_map_functor {X : TopCat} {U : TopologicalSpace.Opens X} (V : TopologicalSpace.Opens U) :
                                  .adjunction.counit.app (.functor.obj V) = CategoryTheory.eqToHom