# mathlibdocumentation

topology.category.Top.opens

# The category of open sets in a topological space.

We define to_Top : opens X ⥤ Top and map (f : X ⟶ Y) : opens Y ⥤ opens X, given by taking preimages of open sets.

Unfortunately opens isn't (usefully) a functor Top ⥤ 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 map_id : map (𝟙 X) ≅ 𝟭 (opens X) and map_comp : 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]

Equations

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

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

Equations
def topological_space.opens.le_supr {X : Top} {ι : Type u_1} (U : ι → ) (i : ι) :
U i supr U

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

Equations

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

Equations

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

Equations
@[simp]
theorem topological_space.opens.inf_le_left_apply_mk {X : Top} (U V : topological_space.opens X) (x : X) (m : x has_coe_t_aux.coe (U V)) :
(U.inf_le_left V) x, m⟩ = x, _⟩

@[simp]
theorem topological_space.opens.le_supr_apply_mk {X : Top} {ι : Type u_1} (U : ι → ) (i : ι) (x : X) (m : x has_coe_t_aux.coe (U i)) :
x, m⟩ = x, _⟩

The functor from open sets in X to Top, realising each open set as a topological space itself.

Equations
@[simp]
theorem topological_space.opens.to_Top_map (X : Top) {U V : topological_space.opens X} {f : U V} {x : X} {h : x U.val} :
x, h⟩ = x, _⟩

@[simp]

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

Equations
def topological_space.opens.map {X Y : Top} :
(X Y)

opens.map f gives the functor from open sets in Y to open set in X, given by taking preimages under f.

Equations
@[simp]
theorem topological_space.opens.map_obj {X Y : Top} (f : X Y) (U : set Y) (p : is_open U) :
U, p⟩ = f ⁻¹' U, _⟩

@[simp]
theorem topological_space.opens.map_id_obj' {X : Top} (U : set X) (p : is_open U) :
.obj U, p⟩ = U, p⟩

@[simp]

@[simp]
theorem topological_space.opens.op_map_id_obj {X : Top} (U : ᵒᵖ) :
.op.obj U = U

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

Equations
@[simp]

@[simp]
theorem topological_space.opens.map_comp_obj' {X Y Z : Top} (f : X Y) (g : Y Z) (U : set Z) (p : is_open U) :
(topological_space.opens.map (f g)).obj U, p⟩ = U, p⟩)

@[simp]
theorem topological_space.opens.map_comp_map {X Y Z : Top} (f : X Y) (g : Y Z) {U V : topological_space.opens Z} (i : U V) :

@[simp]
theorem topological_space.opens.map_comp_obj_unop {X Y Z : Top} (f : X Y) (g : Y Z) (U : ᵒᵖ) :

@[simp]
theorem topological_space.opens.op_map_comp_obj {X Y Z : Top} (f : X Y) (g : Y Z) (U : ᵒᵖ) :

The functor opens X ⥤ opens X given by taking preimages under the identity function is naturally isomorphic to the identity functor.

Equations
@[simp]
theorem topological_space.opens.map_comp_hom_app {X Y Z : Top} (f : X Y) (g : Y Z) (U : topological_space.opens Z) :

@[simp]
theorem topological_space.opens.map_comp_inv_app {X Y Z : Top} (f : X Y) (g : Y Z) (U : topological_space.opens Z) :

def topological_space.opens.map_comp {X Y Z : Top} (f : X Y) (g : Y Z) :

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

Equations
def topological_space.opens.map_iso {X Y : Top} (f g : X Y) :

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

Equations
@[simp]
theorem topological_space.opens.map_iso_refl {X Y : Top} (f : X Y) (h : f = f) :

@[simp]
theorem topological_space.opens.map_iso_hom_app {X Y : Top} (f g : X Y) (h : f = g) (U : topological_space.opens Y) :

@[simp]
theorem topological_space.opens.map_iso_inv_app {X Y : Top} (f g : X Y) (h : f = g) (U : topological_space.opens Y) :

@[simp]
theorem is_open_map.functor_obj_val {X Y : Top} {f : X Y} (hf : is_open_map f) (U : topological_space.opens X) :
(hf.functor.obj U).val = f '' U

def is_open_map.functor {X Y : Top} {f : X Y} :

An open map f : X ⟶ Y induces a functor opens X ⥤ opens Y.

Equations
def is_open_map.adjunction {X Y : Top} {f : X Y} (hf : is_open_map f) :

An open map f : X ⟶ Y induces an adjunction between opens X and opens Y.

Equations