feature(category_theory/instances/Top/open[_nhds]): category of open …

…sets, and open neighbourhoods of a point (merge #920 first) (#922)

* rearrange Top

* oops, import from the future

* the categories of open sets and of open_nhds

* missing import

* restoring opens, adding headers

* Update src/category_theory/instances/Top/open_nhds.lean

Co-Authored-By: semorrison <scott@tqft.net>

* use full_subcategory_inclusion

src/category_theory/instances/Top/adjunctions.lean

@@ -0,0 +1,33 @@
+-- Copyright (c) 2017 Scott Morrison. All rights reserved.
+-- Released under Apache 2.0 license as described in the file LICENSE.
+-- Authors: Patrick Massot, Mario Carneiro
+
+import category_theory.instances.Top.basic
+import category_theory.adjunction
+
+universe u
+
+open category_theory
+open category_theory.instances
+
+namespace category_theory.instances.Top
+
+def adj₁ : adjunction discrete forget :=
+{ hom_equiv := λ X Y,
+  { to_fun := λ f, f,
+    inv_fun := λ f, ⟨f, continuous_top⟩,
+    left_inv := by tidy,
+    right_inv := by tidy },
+  unit := { app := λ X, id },
+  counit := { app := λ X, ⟨id, continuous_top⟩ } }
+
+def adj₂ : adjunction forget trivial :=
+{ hom_equiv := λ X Y,
+  { to_fun := λ f, ⟨f, continuous_bot⟩,
+    inv_fun := λ f, f,
+    left_inv := by tidy,
+    right_inv := by tidy },
+  unit := { app := λ X, ⟨id, continuous_bot⟩ },
+  counit := { app := λ X, id } }
+
+end category_theory.instances.Top

src/category_theory/instances/Top/basic.lean

@@ -0,0 +1,33 @@
+-- Copyright (c) 2017 Scott Morrison. All rights reserved.
+-- Released under Apache 2.0 license as described in the file LICENSE.
+-- Authors: Patrick Massot, Scott Morrison, Mario Carneiro
+
+import category_theory.concrete_category
+import category_theory.full_subcategory
+import topology.opens
+
+open category_theory
+open topological_space
+
+universe u
+
+namespace category_theory.instances
+
+/-- The category of topological spaces and continuous maps. -/
+@[reducible] def Top : Type (u+1) := bundled topological_space
+
+instance topological_space_unbundled (x : Top) : topological_space x := x.str
+
+namespace Top
+instance concrete_category_continuous : concrete_category @continuous := ⟨@continuous_id, @continuous.comp⟩
+
+def discrete : Type u ⥤ Top.{u} :=
+{ obj := λ X, ⟨X, ⊤⟩,
+  map := λ X Y f, ⟨f, continuous_top⟩ }
+
+def trivial : Type u ⥤ Top.{u} :=
+{ obj := λ X, ⟨X, ⊥⟩,
+  map := λ X Y f, ⟨f, continuous_bot⟩ }
+end Top
+
+end category_theory.instances

src/category_theory/instances/Top/default.lean

@@ -0,0 +1,8 @@
+-- Copyright (c) 2019 Scott Morrison. All rights reserved.
+-- Released under Apache 2.0 license as described in the file LICENSE.
+-- Authors: Scott Morrison
+
+import category_theory.instances.Top.basic
+import category_theory.instances.Top.limits
+import category_theory.instances.Top.adjunctions
+import category_theory.instances.Top.open_nhds

src/category_theory/instances/Top/limits.lean

@@ -0,0 +1,63 @@
+-- Copyright (c) 2017 Scott Morrison. All rights reserved.
+-- Released under Apache 2.0 license as described in the file LICENSE.
+-- Authors: Patrick Massot, Scott Morrison, Mario Carneiro
+
+import category_theory.instances.Top.basic
+import category_theory.limits.types
+import category_theory.limits.preserves
+
+open category_theory
+open category_theory.instances
+open topological_space
+
+universe u
+
+namespace category_theory.instances.Top
+
+open category_theory.limits
+
+variables {J : Type u} [small_category J]
+
+def limit (F : J ⥤ Top.{u}) : cone F :=
+{ X := ⟨limit (F ⋙ forget), ⨆ j, (F.obj j).str.induced (limit.π (F ⋙ forget) j)⟩,
+  π :=
+  { app := λ j, ⟨limit.π (F ⋙ forget) j, continuous_iff_induced_le.mpr (lattice.le_supr _ j)⟩,
+    naturality' := λ j j' f, subtype.eq ((limit.cone (F ⋙ forget)).π.naturality f) } }
+
+def limit_is_limit (F : J ⥤ Top.{u}) : is_limit (limit F) :=
+by refine is_limit.of_faithful forget (limit.is_limit _) (λ s, ⟨_, _⟩) (λ s, rfl);
+   exact continuous_iff_le_coinduced.mpr (lattice.supr_le $ λ j,
+     induced_le_iff_le_coinduced.mpr $ continuous_iff_le_coinduced.mp (s.π.app j).property)
+
+instance Top_has_limits : has_limits.{u} Top.{u} :=
+{ has_limits_of_shape := λ J 𝒥,
+  { has_limit := λ F, by exactI { cone := limit F, is_limit := limit_is_limit F } } }
+
+instance forget_preserves_limits : preserves_limits (forget : Top.{u} ⥤ Type u) :=
+{ preserves_limits_of_shape := λ J 𝒥,
+  { preserves_limit := λ F,
+    by exactI preserves_limit_of_preserves_limit_cone
+      (limit.is_limit F) (limit.is_limit (F ⋙ forget)) } }
+
+def colimit (F : J ⥤ Top.{u}) : cocone F :=
+{ X := ⟨colimit (F ⋙ forget), ⨅ j, (F.obj j).str.coinduced (colimit.ι (F ⋙ forget) j)⟩,
+  ι :=
+  { app := λ j, ⟨colimit.ι (F ⋙ forget) j, continuous_iff_le_coinduced.mpr (lattice.infi_le _ j)⟩,
+    naturality' := λ j j' f, subtype.eq ((colimit.cocone (F ⋙ forget)).ι.naturality f) } }
+
+def colimit_is_colimit (F : J ⥤ Top.{u}) : is_colimit (colimit F) :=
+by refine is_colimit.of_faithful forget (colimit.is_colimit _) (λ s, ⟨_, _⟩) (λ s, rfl);
+   exact continuous_iff_induced_le.mpr (lattice.le_infi $ λ j,
+     induced_le_iff_le_coinduced.mpr $ continuous_iff_le_coinduced.mp (s.ι.app j).property)
+
+instance Top_has_colimits : has_colimits.{u} Top.{u} :=
+{ has_colimits_of_shape := λ J 𝒥,
+  { has_colimit := λ F, by exactI { cocone := colimit F, is_colimit := colimit_is_colimit F } } }
+
+instance forget_preserves_colimits : preserves_colimits (forget : Top.{u} ⥤ Type u) :=
+{ preserves_colimits_of_shape := λ J 𝒥,
+  { preserves_colimit := λ F,
+    by exactI preserves_colimit_of_preserves_colimit_cocone
+      (colimit.is_colimit F) (colimit.is_colimit (F ⋙ forget)) } }
+
+end category_theory.instances.Top

src/category_theory/instances/Top/open_nhds.lean

@@ -0,0 +1,42 @@
+import category_theory.instances.Top.opens
+
+open category_theory
+open category_theory.instances
+open topological_space
+
+universe u
+
+namespace topological_space.open_nhds
+variables {X Y : Top.{u}} (f : X ⟶ Y)
+
+def open_nhds (x : X.α) := { U : opens X // x ∈ U }
+instance open_nhds_category (x : X.α) : category.{u+1} (open_nhds x) := by {unfold open_nhds, apply_instance}
+
+def inclusion (x : X.α) : open_nhds x ⥤ opens X :=
+full_subcategory_inclusion _
+
+@[simp] lemma inclusion_obj (x : X.α) (U) (p) : (inclusion x).obj ⟨U,p⟩ = U := rfl
+
+def map (x : X) : open_nhds (f x) ⥤ open_nhds x :=
+{ obj := λ U, ⟨(opens.map f).obj U.1, by tidy⟩,
+  map := λ U V i, (opens.map f).map i }
+
+@[simp] lemma map_id_obj' (x : X) (U) (p) (q) : (map (𝟙 X) x).obj ⟨⟨U, p⟩, q⟩ = ⟨⟨U, p⟩, q⟩ :=
+rfl
+@[simp] lemma map_id_obj (x : X) (U) : (map (𝟙 X) x).obj U = U :=
+by tidy
+
+@[simp] lemma map_id_obj_unop (x : X) (U : (open_nhds x)ᵒᵖ) : (map (𝟙 X) x).obj (unop U) = unop U :=
+by simp
+@[simp] lemma op_map_id_obj (x : X) (U : (open_nhds x)ᵒᵖ) : (map (𝟙 X) x).op.obj U = U :=
+by simp
+
+def inclusion_map_iso (x : X) : inclusion (f x) ⋙ opens.map f ≅ map f x ⋙ inclusion x :=
+nat_iso.of_components
+  (λ U, begin split, exact 𝟙 _, exact 𝟙 _ end)
+  (by tidy)
+
+@[simp] lemma inclusion_map_iso_hom (x : X) : (inclusion_map_iso f x).hom = 𝟙 _ := rfl
+@[simp] lemma inclusion_map_iso_inv (x : X) : (inclusion_map_iso f x).inv = 𝟙 _ := rfl
+
+end topological_space.open_nhds

src/category_theory/instances/Top/opens.lean

@@ -0,0 +1,83 @@
+import category_theory.instances.Top.basic
+import category_theory.natural_isomorphism
+import category_theory.opposites
+import category_theory.eq_to_hom
+
+open category_theory
+open category_theory.instances
+open topological_space
+
+universe u
+
+open category_theory.instances
+
+namespace topological_space.opens
+
+variables {X Y Z : Top.{u}}
+
+instance opens_category : category.{u+1} (opens X) :=
+{ hom  := λ U V, ulift (plift (U ≤ V)),
+  id   := λ X, ⟨ ⟨ le_refl X ⟩ ⟩,
+  comp := λ X Y Z f g, ⟨ ⟨ le_trans f.down.down g.down.down ⟩ ⟩ }
+
+/-- `opens.map f` gives the functor from open sets in Y to open set in X,
+    given by taking preimages under f. -/
+def map (f : X ⟶ Y) : opens Y ⥤ opens X :=
+{ obj := λ U, ⟨ f.val ⁻¹' U, f.property _ U.property ⟩,
+  map := λ U V i, ⟨ ⟨ λ a b, i.down.down b ⟩ ⟩ }.
+
+@[simp] lemma map_id_obj' (U) (p) : (map (𝟙 X)).obj ⟨U, p⟩ = ⟨U, p⟩ :=
+rfl
+
+@[simp] lemma map_id_obj (U : opens X) : (map (𝟙 X)).obj U = U :=
+by { ext, refl } -- not quite `rfl`, since we don't have eta for records
+
+@[simp] lemma map_id_obj_unop (U : (opens X)ᵒᵖ) : (map (𝟙 X)).obj (unop U) = unop U :=
+by simp
+@[simp] lemma op_map_id_obj (U : (opens X)ᵒᵖ) : (map (𝟙 X)).op.obj U = U :=
+by simp
+
+section
+variable (X)
+def map_id : map (𝟙 X) ≅ functor.id (opens X) :=
+{ hom := { app := λ U, eq_to_hom (map_id_obj U) },
+  inv := { app := λ U, eq_to_hom (map_id_obj U).symm } }
+
+@[simp] lemma map_id_hom_app (U) : (map_id X).hom.app U = eq_to_hom (map_id_obj U) := rfl
+@[simp] lemma map_id_inv_app (U) : (map_id X).inv.app U = eq_to_hom (map_id_obj U).symm := rfl
+end
+
+@[simp] lemma map_comp_obj' (f : X ⟶ Y) (g : Y ⟶ Z) (U) (p) : (map (f ≫ g)).obj ⟨U, p⟩ = (map f).obj ((map g).obj ⟨U, p⟩) :=
+rfl
+
+@[simp] lemma map_comp_obj (f : X ⟶ Y) (g : Y ⟶ Z) (U) : (map (f ≫ g)).obj U = (map f).obj ((map g).obj U) :=
+by { ext, refl } -- not quite `rfl`, since we don't have eta for records
+
+@[simp] lemma map_comp_obj_unop (f : X ⟶ Y) (g : Y ⟶ Z) (U) : (map (f ≫ g)).obj (unop U) = (map f).obj ((map g).obj (unop U)) :=
+by simp
+@[simp] lemma op_map_comp_obj (f : X ⟶ Y) (g : Y ⟶ Z) (U) : (map (f ≫ g)).op.obj U = (map f).op.obj ((map g).op.obj U) :=
+by simp
+
+def map_comp (f : X ⟶ Y) (g : Y ⟶ Z) : map (f ≫ g) ≅ map g ⋙ map f :=
+{ hom := { app := λ U, eq_to_hom (map_comp_obj f g U) },
+  inv := { app := λ U, eq_to_hom (map_comp_obj f g U).symm } }
+
+@[simp] lemma map_comp_hom_app (f : X ⟶ Y) (g : Y ⟶ Z) (U) : (map_comp f g).hom.app U = eq_to_hom (map_comp_obj f g U) := rfl
+@[simp] lemma map_comp_inv_app (f : X ⟶ Y) (g : Y ⟶ Z) (U) : (map_comp f g).inv.app U = eq_to_hom (map_comp_obj f g U).symm := rfl
+
+-- We could make f g implicit here, but it's nice to be able to see when
+-- they are the identity (often!)
+def map_iso (f g : X ⟶ Y) (h : f = g) : map f ≅ map g :=
+nat_iso.of_components (λ U, eq_to_iso (congr_fun (congr_arg functor.obj (congr_arg map h)) U) ) (by obviously)
+
+@[simp] lemma map_iso_refl (f : X ⟶ Y) (h) : map_iso f f h = iso.refl (map _) := rfl
+
+@[simp] lemma map_iso_hom_app (f g : X ⟶ Y) (h : f = g) (U : opens Y) :
+  (map_iso f g h).hom.app U = eq_to_hom (congr_fun (congr_arg functor.obj (congr_arg map h)) U) :=
+rfl
+
+@[simp] lemma map_iso_inv_app (f g : X ⟶ Y) (h : f = g) (U : opens Y) :
+  (map_iso f g h).inv.app U = eq_to_hom (congr_fun (congr_arg functor.obj (congr_arg map h.symm)) U) :=
+rfl
+
+end topological_space.opens

src/category_theory/instances/measurable_space.lean

@@ -5,7 +5,7 @@ Authors: Johannes Hölzl
 Basic setup for measurable spaces.
 -/
 
-import category_theory.instances.topological_spaces
+import category_theory.instances.Top
 import measure_theory.borel_space
 
 open category_theory