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

source
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 := (_ : โ†‘x โˆˆ โ†‘V) } }

We now construct as morphisms various inclusions of open sets.

source
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
Instances For
    source
    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
    Instances For
      source
      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
        source
        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
        Instances For
          source
          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
          Instances For
            source
            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 โˆˆ โ†‘U) }) x = { val := โ†‘x, property := (_ : โ†‘x โˆˆ โ†‘U) }
            source
            @[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 := (_ : โ†‘x โˆˆ โ†‘U) }) { val := x, property := m } = { val := x, property := (_ : x โˆˆ โ†‘U) }
            source
            @[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 := (_ : โ†‘x โˆˆ โ†‘(iSup U)) }) { val := x, property := m } = { val := x, property := (_ : x โˆˆ โ†‘(iSup U)) }
            source
            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.
            Instances For
              source
              @[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).toPrefunctor.map f) { val := x, property := h } = { val := x, property := (_ : x โˆˆ โ†‘V) }
              source
              @[simp]
              theorem TopologicalSpace.Opens.inclusion_apply {X : TopCat} (U : TopologicalSpace.Opens โ†‘X) :
              โ‡‘(TopologicalSpace.Opens.inclusion U) = Subtype.val
              source
              def TopologicalSpace.Opens.inclusion {X : TopCat} (U : TopologicalSpace.Opens โ†‘X) :
              (TopologicalSpace.Opens.toTopCat X).toPrefunctor.obj U โŸถ X

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

              Equations
              Instances For
                source
                @[simp]
                theorem TopologicalSpace.Opens.coe_inclusion {X : TopCat} {U : TopologicalSpace.Opens โ†‘X} :
                โ‡‘(TopologicalSpace.Opens.inclusion U) = Subtype.val
                source
                theorem TopologicalSpace.Opens.openEmbedding {X : TopCat} (U : TopologicalSpace.Opens โ†‘X) :
                OpenEmbedding โ‡‘(TopologicalSpace.Opens.inclusion U)
                source
                def TopologicalSpace.Opens.inclusionTopIso (X : TopCat) :
                (TopologicalSpace.Opens.toTopCat X).toPrefunctor.obj โŠค โ‰… X

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

                Equations
                Instances For
                  source
                  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.
                  Instances For
                    source
                    @[simp]
                    theorem TopologicalSpace.Opens.map_coe {X : TopCat} {Y : TopCat} (f : X โŸถ Y) (U : TopologicalSpace.Opens โ†‘Y) :
                    โ†‘((TopologicalSpace.Opens.map f).toPrefunctor.obj U) = โ‡‘f โปยน' โ†‘U
                    source
                    @[simp]
                    theorem TopologicalSpace.Opens.map_obj {X : TopCat} {Y : TopCat} (f : X โŸถ Y) (U : Set โ†‘Y) (p : IsOpen U) :
                    (TopologicalSpace.Opens.map f).toPrefunctor.obj { carrier := U, is_open' := p } = { carrier := โ‡‘f โปยน' U, is_open' := (_ : IsOpen (โ‡‘f โปยน' U)) }
                    source
                    @[simp]
                    theorem TopologicalSpace.Opens.map_id_obj {X : TopCat} (U : TopologicalSpace.Opens โ†‘X) :
                    (TopologicalSpace.Opens.map (CategoryTheory.CategoryStruct.id X)).toPrefunctor.obj U = U
                    source
                    @[simp]
                    theorem TopologicalSpace.Opens.map_id_obj' {X : TopCat} (U : Set โ†‘X) (p : IsOpen U) :
                    (TopologicalSpace.Opens.map (CategoryTheory.CategoryStruct.id X)).toPrefunctor.obj { carrier := U, is_open' := p } = { carrier := U, is_open' := p }
                    source
                    @[simp]
                    theorem TopologicalSpace.Opens.map_id_obj_unop {X : TopCat} (U : (TopologicalSpace.Opens โ†‘X)แต’แต–) :
                    (TopologicalSpace.Opens.map (CategoryTheory.CategoryStruct.id X)).toPrefunctor.obj U.unop = U.unop
                    source
                    @[simp]
                    theorem TopologicalSpace.Opens.op_map_id_obj {X : TopCat} (U : (TopologicalSpace.Opens โ†‘X)แต’แต–) :
                    (TopologicalSpace.Opens.map (CategoryTheory.CategoryStruct.id X)).op.toPrefunctor.obj U = U
                    source
                    @[simp]
                    theorem TopologicalSpace.Opens.map_top {X : TopCat} {Y : TopCat} (f : X โŸถ Y) :
                    (TopologicalSpace.Opens.map f).toPrefunctor.obj โŠค = โŠค
                    source
                    noncomputable def TopologicalSpace.Opens.leMapTop {X : TopCat} {Y : TopCat} (f : X โŸถ Y) (U : TopologicalSpace.Opens โ†‘X) :
                    U โŸถ (TopologicalSpace.Opens.map f).toPrefunctor.obj โŠค

                    The inclusion U โŸถ (map f).obj โŠค as a morphism in the category of open sets.

                    Equations
                    Instances For
                      source
                      @[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)).toPrefunctor.obj U = (TopologicalSpace.Opens.map f).toPrefunctor.obj ((TopologicalSpace.Opens.map g).toPrefunctor.obj U)
                      source
                      @[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)).toPrefunctor.obj { carrier := U, is_open' := p } = (TopologicalSpace.Opens.map f).toPrefunctor.obj ((TopologicalSpace.Opens.map g).toPrefunctor.obj { carrier := U, is_open' := p })
                      source
                      @[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)).toPrefunctor.map i = (TopologicalSpace.Opens.map f).toPrefunctor.map ((TopologicalSpace.Opens.map g).toPrefunctor.map i)
                      source
                      @[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)).toPrefunctor.obj U.unop = (TopologicalSpace.Opens.map f).toPrefunctor.obj ((TopologicalSpace.Opens.map g).toPrefunctor.obj U.unop)
                      source
                      @[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.toPrefunctor.obj U = (TopologicalSpace.Opens.map f).op.toPrefunctor.obj ((TopologicalSpace.Opens.map g).op.toPrefunctor.obj U)
                      source
                      theorem TopologicalSpace.Opens.map_iSup {X : TopCat} {Y : TopCat} (f : X โŸถ Y) {ฮน : Type u_1} (U : ฮน โ†’ TopologicalSpace.Opens โ†‘Y) :
                      (TopologicalSpace.Opens.map f).toPrefunctor.obj (iSup U) = iSup ((TopologicalSpace.Opens.map f).toPrefunctor.obj โˆ˜ U)
                      source
                      @[simp]
                      theorem TopologicalSpace.Opens.mapId_inv_app (X : TopCat) (U : TopologicalSpace.Opens โ†‘X) :
                      (TopologicalSpace.Opens.mapId X).inv.app U = CategoryTheory.eqToHom (_ : U = (TopologicalSpace.Opens.map (CategoryTheory.CategoryStruct.id X)).toPrefunctor.obj U)
                      source
                      @[simp]
                      theorem TopologicalSpace.Opens.mapId_hom_app (X : TopCat) (U : TopologicalSpace.Opens โ†‘X) :
                      (TopologicalSpace.Opens.mapId X).hom.app U = CategoryTheory.eqToHom (_ : (TopologicalSpace.Opens.map (CategoryTheory.CategoryStruct.id X)).toPrefunctor.obj U = U)
                      source
                      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.
                      Instances For
                        source
                        theorem TopologicalSpace.Opens.map_id_eq (X : TopCat) :
                        TopologicalSpace.Opens.map (CategoryTheory.CategoryStruct.id X) = CategoryTheory.Functor.id (TopologicalSpace.Opens โ†‘X)
                        source
                        @[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 (_ : (TopologicalSpace.Opens.map (CategoryTheory.CategoryStruct.comp f g)).toPrefunctor.obj U = (TopologicalSpace.Opens.map f).toPrefunctor.obj ((TopologicalSpace.Opens.map g).toPrefunctor.obj U))
                        source
                        @[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 (_ : (TopologicalSpace.Opens.map f).toPrefunctor.obj ((TopologicalSpace.Opens.map g).toPrefunctor.obj U) = (TopologicalSpace.Opens.map (CategoryTheory.CategoryStruct.comp f g)).toPrefunctor.obj U)
                        source
                        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.
                        Instances For
                          source
                          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)
                          source
                          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
                          • One or more equations did not get rendered due to their size.
                          Instances For
                            source
                            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
                            source
                            @[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)
                            source
                            @[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 (_ : (TopologicalSpace.Opens.map f).toPrefunctor.obj U = (TopologicalSpace.Opens.map g).toPrefunctor.obj U)
                            source
                            @[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 (_ : (TopologicalSpace.Opens.map g).toPrefunctor.obj U = (TopologicalSpace.Opens.map f).toPrefunctor.obj U)
                            source
                            @[simp]
                            theorem TopologicalSpace.Opens.mapMapIso_inverse {X : TopCat} {Y : TopCat} (H : X โ‰… Y) :
                            (TopologicalSpace.Opens.mapMapIso H).inverse = TopologicalSpace.Opens.map H.inv
                            source
                            @[simp]
                            theorem TopologicalSpace.Opens.mapMapIso_functor {X : TopCat} {Y : TopCat} (H : X โ‰… Y) :
                            (TopologicalSpace.Opens.mapMapIso H).functor = TopologicalSpace.Opens.map H.hom
                            source
                            @[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 (_ : U = { carrier := โ‡‘H.inv โปยน' โ†‘((CategoryTheory.Functor.mk { obj := fun (U : TopologicalSpace.Opens โ†‘Y) => { carrier := โ‡‘H.hom โปยน' โ†‘U, is_open' := (_ : IsOpen (โ‡‘H.hom โปยน' โ†‘U)) }, map := fun {X_1 Y_1 : TopologicalSpace.Opens โ†‘Y} (i : X_1 โŸถ Y_1) => { down := { down := (_ : โˆ€ x โˆˆ โ†‘((fun (U : TopologicalSpace.Opens โ†‘Y) => { carrier := โ‡‘H.hom โปยน' โ†‘U, is_open' := (_ : IsOpen (โ‡‘H.hom โปยน' โ†‘U)) }) X_1), H.hom x โˆˆ โ†‘Y_1) } } }).toPrefunctor.obj U), is_open' := (_ : IsOpen (โ‡‘H.inv โปยน' โ†‘((CategoryTheory.Functor.mk { obj := fun (U : TopologicalSpace.Opens โ†‘Y) => { carrier := โ‡‘H.hom โปยน' โ†‘U, is_open' := (_ : IsOpen (โ‡‘H.hom โปยน' โ†‘U)) }, map := fun {X_1 Y_1 : TopologicalSpace.Opens โ†‘Y} (i : X_1 โŸถ Y_1) => { down := { down := (_ : โˆ€ x โˆˆ โ†‘((fun (U : TopologicalSpace.Opens โ†‘Y) => { carrier := โ‡‘H.hom โปยน' โ†‘U, is_open' := (_ : IsOpen (โ‡‘H.hom โปยน' โ†‘U)) }) X_1), H.hom x โˆˆ โ†‘Y_1) } } }).toPrefunctor.obj U))) })
                            source
                            @[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 (_ : { carrier := โ‡‘H.hom โปยน' โ†‘((CategoryTheory.Functor.mk { obj := fun (U : TopologicalSpace.Opens โ†‘X) => { carrier := โ‡‘H.inv โปยน' โ†‘U, is_open' := (_ : IsOpen (โ‡‘H.inv โปยน' โ†‘U)) }, map := fun {X_1 Y_1 : TopologicalSpace.Opens โ†‘X} (i : X_1 โŸถ Y_1) => { down := { down := (_ : โˆ€ x โˆˆ โ†‘((fun (U : TopologicalSpace.Opens โ†‘X) => { carrier := โ‡‘H.inv โปยน' โ†‘U, is_open' := (_ : IsOpen (โ‡‘H.inv โปยน' โ†‘U)) }) X_1), H.inv x โˆˆ โ†‘Y_1) } } }).toPrefunctor.obj U), is_open' := (_ : IsOpen (โ‡‘H.hom โปยน' โ†‘((CategoryTheory.Functor.mk { obj := fun (U : TopologicalSpace.Opens โ†‘X) => { carrier := โ‡‘H.inv โปยน' โ†‘U, is_open' := (_ : IsOpen (โ‡‘H.inv โปยน' โ†‘U)) }, map := fun {X_1 Y_1 : TopologicalSpace.Opens โ†‘X} (i : X_1 โŸถ Y_1) => { down := { down := (_ : โˆ€ x โˆˆ โ†‘((fun (U : TopologicalSpace.Opens โ†‘X) => { carrier := โ‡‘H.inv โปยน' โ†‘U, is_open' := (_ : IsOpen (โ‡‘H.inv โปยน' โ†‘U)) }) X_1), H.inv x โˆˆ โ†‘Y_1) } } }).toPrefunctor.obj U))) } = U)
                            source
                            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.
                            Instances For
                              source
                              @[simp]
                              theorem IsOpenMap.functor_obj_coe {X : TopCat} {Y : TopCat} {f : X โŸถ Y} (hf : IsOpenMap โ‡‘f) (U : TopologicalSpace.Opens โ†‘X) :
                              โ†‘((IsOpenMap.functor hf).toPrefunctor.obj U) = โ‡‘f '' โ†‘U
                              source
                              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.
                              Instances For
                                source
                                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.
                                Instances For
                                  source
                                  instance IsOpenMap.functorFullOfMono {X : TopCat} {Y : TopCat} {f : X โŸถ Y} (hf : IsOpenMap โ‡‘f) [H : CategoryTheory.Mono f] :
                                  CategoryTheory.Full (IsOpenMap.functor hf)
                                  Equations
                                  • One or more equations did not get rendered due to their size.
                                  source
                                  instance IsOpenMap.functor_faithful {X : TopCat} {Y : TopCat} {f : X โŸถ Y} (hf : IsOpenMap โ‡‘f) :
                                  CategoryTheory.Faithful (IsOpenMap.functor hf)
                                  Equations
                                  source
                                  theorem OpenEmbedding.functor_obj_injective {X : TopCat} {Y : TopCat} {f : X โŸถ Y} (hf : OpenEmbedding โ‡‘f) :
                                  Function.Injective (IsOpenMap.functor (_ : IsOpenMap โ‡‘f)).toPrefunctor.obj
                                  source
                                  @[simp]
                                  theorem TopologicalSpace.Opens.openEmbedding_obj_top {X : TopCat} (U : TopologicalSpace.Opens โ†‘X) :
                                  (IsOpenMap.functor (_ : IsOpenMap โ‡‘(TopologicalSpace.Opens.inclusion U))).toPrefunctor.obj โŠค = U
                                  source
                                  @[simp]
                                  theorem TopologicalSpace.Opens.inclusion_map_eq_top {X : TopCat} (U : TopologicalSpace.Opens โ†‘X) :
                                  (TopologicalSpace.Opens.map (TopologicalSpace.Opens.inclusion U)).toPrefunctor.obj U = โŠค
                                  source
                                  @[simp]
                                  theorem TopologicalSpace.Opens.adjunction_counit_app_self {X : TopCat} (U : TopologicalSpace.Opens โ†‘X) :
                                  (IsOpenMap.adjunction (_ : IsOpenMap โ‡‘(TopologicalSpace.Opens.inclusion U))).counit.app U = CategoryTheory.eqToHom (_ : (IsOpenMap.functor (_ : IsOpenMap โ‡‘(TopologicalSpace.Opens.inclusion U))).toPrefunctor.obj ((TopologicalSpace.Opens.map (TopologicalSpace.Opens.inclusion U)).toPrefunctor.obj U) = U)
                                  source
                                  theorem TopologicalSpace.Opens.inclusion_top_functor (X : TopCat) :
                                  IsOpenMap.functor (_ : IsOpenMap โ‡‘(TopologicalSpace.Opens.inclusion โŠค)) = TopologicalSpace.Opens.map (TopologicalSpace.Opens.inclusionTopIso X).inv
                                  source
                                  theorem TopologicalSpace.Opens.functor_obj_map_obj {X : TopCat} {Y : TopCat} {f : X โŸถ Y} (hf : IsOpenMap โ‡‘f) (U : TopologicalSpace.Opens โ†‘Y) :
                                  (IsOpenMap.functor hf).toPrefunctor.obj ((TopologicalSpace.Opens.map f).toPrefunctor.obj U) = (IsOpenMap.functor hf).toPrefunctor.obj โŠค โŠ“ U
                                  source
                                  theorem TopologicalSpace.Opens.set_range_forget_map_inclusion {X : TopCat} (U : TopologicalSpace.Opens โ†‘X) :
                                  Set.range ((CategoryTheory.forget TopCat).toPrefunctor.map (TopologicalSpace.Opens.inclusion U)) = โ†‘U
                                  source
                                  @[simp]
                                  theorem TopologicalSpace.Opens.functor_map_eq_inf {X : TopCat} (U : TopologicalSpace.Opens โ†‘X) (V : TopologicalSpace.Opens โ†‘X) :
                                  (IsOpenMap.functor (_ : IsOpenMap โ‡‘(TopologicalSpace.Opens.inclusion U))).toPrefunctor.obj ((TopologicalSpace.Opens.map (TopologicalSpace.Opens.inclusion U)).toPrefunctor.obj V) = V โŠ“ U
                                  source
                                  theorem TopologicalSpace.Opens.map_functor_eq' {X : TopCat} {U : TopCat} (f : U โŸถ X) (hf : OpenEmbedding โ‡‘f) (V : TopologicalSpace.Opens โ†‘U) :
                                  (TopologicalSpace.Opens.map f).toPrefunctor.obj ((IsOpenMap.functor (_ : IsOpenMap โ‡‘f)).toPrefunctor.obj V) = V
                                  source
                                  @[simp]
                                  theorem TopologicalSpace.Opens.map_functor_eq {X : TopCat} {U : TopologicalSpace.Opens โ†‘X} (V : TopologicalSpace.Opens โ†ฅU) :
                                  (TopologicalSpace.Opens.map (TopologicalSpace.Opens.inclusion U)).toPrefunctor.obj ((IsOpenMap.functor (_ : IsOpenMap โ‡‘(TopologicalSpace.Opens.inclusion U))).toPrefunctor.obj V) = V
                                  source
                                  @[simp]
                                  theorem TopologicalSpace.Opens.adjunction_counit_map_functor {X : TopCat} {U : TopologicalSpace.Opens โ†‘X} (V : TopologicalSpace.Opens โ†ฅU) :
                                  (IsOpenMap.adjunction (_ : IsOpenMap โ‡‘(TopologicalSpace.Opens.inclusion U))).counit.app ((IsOpenMap.functor (_ : IsOpenMap โ‡‘(TopologicalSpace.Opens.inclusion U))).toPrefunctor.obj V) = CategoryTheory.eqToHom (_ : (CategoryTheory.Functor.comp (TopologicalSpace.Opens.map (TopologicalSpace.Opens.inclusion U)) (IsOpenMap.functor (_ : IsOpenMap โ‡‘(TopologicalSpace.Opens.inclusion U)))).toPrefunctor.obj ((IsOpenMap.functor (_ : IsOpenMap โ‡‘(TopologicalSpace.Opens.inclusion U))).toPrefunctor.obj V) = (CategoryTheory.Functor.id (TopologicalSpace.Opens โ†‘X)).toPrefunctor.obj ((IsOpenMap.functor (_ : IsOpenMap โ‡‘(TopologicalSpace.Opens.inclusion U))).toPrefunctor.obj V))