The category of open sets in a topological space. #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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)).
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.inf_le_left V = _.hom
The inclusion U ⊓ V ⟶ V as a morphism in the category of open sets.
Equations
- U.inf_le_right V = _.hom
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.
The inclusion U ⟶ ⊤ as a morphism in the category of open sets.
The functor from open sets in X to Top,
realising each open set as a topological space itself.
Equations
- topological_space.opens.to_Top X = {obj := λ (U : topological_space.opens ↥X), {α := ↥U, str := infer_instance subtype.topological_space}, map := λ (U V : topological_space.opens ↥X) (i : U ⟶ V), {to_fun := λ (x : ↥{α := ↥U, str := infer_instance subtype.topological_space}), ⟨x.val, _⟩, continuous_to_fun := _}, map_id' := _, map_comp' := _}
The inclusion map from an open subset to the whole space, as a morphism in Top.
Equations
- U.inclusion = {to_fun := coe coe_to_lift, continuous_to_fun := _}
The inclusion of the top open subset (i.e. the whole space) is an isomorphism.
Equations
- topological_space.opens.inclusion_top_iso X = {hom := ⊤.inclusion, inv := {to_fun := λ (x : ↥X), ⟨x, trivial⟩, continuous_to_fun := _}, hom_inv_id' := _, inv_hom_id' := _}
opens.map f gives the functor from open sets in Y to open set in X,
given by taking preimages under f.
The inclusion U ⟶ (map f).obj ⊤ as a morphism in the category of open sets.
Equations
The functor opens X ⥤ opens X given by taking preimages under the identity function
is naturally isomorphic to the identity functor.
Equations
- topological_space.opens.map_id X = {hom := {app := λ (U : topological_space.opens ↥X), category_theory.eq_to_hom _, naturality' := _}, inv := {app := λ (U : topological_space.opens ↥X), category_theory.eq_to_hom _, naturality' := _}, hom_inv_id' := _, inv_hom_id' := _}
The natural isomorphism between taking preimages under f ≫ g, and the composite
of taking preimages under g, then preimages under f.
Equations
- topological_space.opens.map_comp f g = {hom := {app := λ (U : topological_space.opens ↥Z), category_theory.eq_to_hom _, naturality' := _}, inv := {app := λ (U : topological_space.opens ↥Z), category_theory.eq_to_hom _, naturality' := _}, hom_inv_id' := _, inv_hom_id' := _}
If two continuous maps f g : X ⟶ Y are equal,
then the functors opens Y ⥤ opens X they induce are isomorphic.
Equations
A homeomorphism of spaces gives an equivalence of categories of open sets.
TODO: define order_iso.equivalence, use it.
Equations
- topological_space.opens.map_map_iso H = {functor := topological_space.opens.map H.hom, inverse := topological_space.opens.map H.inv, unit_iso := category_theory.nat_iso.of_components (λ (U : topological_space.opens ↥Y), category_theory.eq_to_iso _) _, counit_iso := category_theory.nat_iso.of_components (λ (U : topological_space.opens ↥X), category_theory.eq_to_iso _) _, functor_unit_iso_comp' := _}
An open map f : X ⟶ Y induces a functor opens X ⥤ opens Y.
Equations
Instances for is_open_map.functor
An open map f : X ⟶ Y induces an adjunction between opens X and opens Y.
Equations
- hf.adjunction = category_theory.adjunction.mk_of_unit_counit {unit := {app := λ (U : topological_space.opens ↥X), category_theory.hom_of_le _, naturality' := _}, counit := {app := λ (V : topological_space.opens ↥Y), category_theory.hom_of_le _, naturality' := _}, left_triangle' := _, right_triangle' := _}
Equations
- hf.functor_full_of_mono = {preimage := λ (U V : topological_space.opens ↥X) (i : hf.functor.obj U ⟶ hf.functor.obj V), category_theory.hom_of_le _, witness' := _}