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

We now construct as morphisms various inclusions of open sets.

noncomputable def TopologicalSpace.Opens.infLELeft {X : TopCat} (U V : Opens X) :
UV U

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

Equations
noncomputable def TopologicalSpace.Opens.infLERight {X : TopCat} (U V : Opens X) :
UV V

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

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

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

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

Equations
noncomputable def TopologicalSpace.Opens.leTop {X : TopCat} (U : Opens X) :

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

Equations
theorem TopologicalSpace.Opens.infLELeft_apply {X : TopCat} (U V : Opens X) (x : (UV)) :
(U.infLELeft V) x = x,
@[simp]
theorem TopologicalSpace.Opens.infLELeft_apply_mk {X : TopCat} (U V : Opens X) (x : X) (m : x UV) :
(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,

The functor from open sets in X to TopCat, 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 V : Opens X} {f : U V} {x : X} {h : x U} :

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

Equations

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

Equations

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 Y : TopCat} (f : X Y) (U : Opens Y) :
@[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) :
@[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 }
@[simp]
theorem TopologicalSpace.Opens.map_top {X Y : TopCat} (f : X Y) :
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.

Equations
@[simp]
theorem TopologicalSpace.Opens.map_comp_obj {X Y Z : TopCat} (f : X Y) (g : Y Z) (U : Opens Z) :
@[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) :
@[simp]
@[simp]
theorem TopologicalSpace.Opens.op_map_comp_obj {X Y Z : TopCat} (f : X Y) (g : Y Z) (U : (Opens Z)ᵒᵖ) :
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)

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.

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.
@[simp]
theorem TopologicalSpace.Opens.mapComp_inv_app {X Y Z : TopCat} (f : X Y) (g : Y Z) (U : Opens Z) :
@[simp]
theorem TopologicalSpace.Opens.mapComp_hom_app {X Y Z : TopCat} (f : X Y) (g : Y Z) (U : Opens Z) :
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.

Equations
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) :
@[simp]
theorem TopologicalSpace.Opens.mapIso_hom_app {X Y : TopCat} (f g : X Y) (h : f = g) (U : Opens Y) :
@[simp]
theorem TopologicalSpace.Opens.mapIso_inv_app {X Y : TopCat} (f g : X Y) (h : f = g) (U : Opens Y) :
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.

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

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.

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.

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.

Equations

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

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

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

Equations

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

Equations
@[simp]
theorem TopologicalSpace.Opens.functor_map_eq_inf {X : TopCat} (U V : Opens X) :
.functor.obj ((map U.inclusion').obj V) = VU
@[simp]
theorem TopologicalSpace.Opens.map_functor_eq {X : TopCat} {U : Opens X} (V : Opens U) :
(map U.inclusion').obj (.functor.obj V) = V