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)).
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
The inclusion U i ⟶ supr U as a morphism in the category of open sets.
Equations
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.val), str := infer_instance subtype.topological_space}, map := λ (U V : topological_space.opens ↥X) (i : U ⟶ V), {to_fun := λ (x : ↥{α := ↥(U.val), str := infer_instance subtype.topological_space}), ⟨x.val, _⟩, continuous_to_fun := _}, map_id' := _, map_comp' := _}
opens.map f gives the functor from open sets in Y to open set in X,
given by taking preimages under f.
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' := _}