feat(roadmap): add some formal roadmaps in topology (#1914)

* feat(roadmap): add some formal roadmaps in topology

* Update roadmap/topology/paracompact.lean

Co-Authored-By: Johan Commelin <johan@commelin.net>

* Update roadmap/todo.lean

* Update roadmap/topology/shrinking_lemma.lean

Co-Authored-By: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com>

* add `todo` tactic as a wrapper for `exact todo`

* Update roadmap/topology/shrinking_lemma.lean

Co-Authored-By: Johan Commelin <johan@commelin.net>

* copyright notices and module docs

* oops

Co-authored-by: Scott Morrison <scott@tqft.net>
Co-authored-by: Johan Commelin <johan@commelin.net>
Co-authored-by: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com>
Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>

roadmap/todo.lean

@@ -0,0 +1,30 @@
+/-
+Copyright (c) 2020 Reid Barton. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Reid Barton
+-/
+
+/-!
+This file adds an axiom `todo`, and a corresponding tactic,
+which can be used in place of `sorry`.
+It is only intended for use inside the roadmap subdirectory.
+-/
+
+/--
+Axiom used to skip proofs in formal roadmaps.
+(When working on a roadmap, you may prefer to prove new lemmas,
+rather than trying to solve an `exact todo` in-line.
+The tactic `extract_goal` is useful for this.)
+-/
+axiom todo {p : Prop} : p
+
+namespace tactic
+namespace interactive
+
+/--
+An axiomatic alternative to `sorry`, used in formal roadmaps.
+-/
+meta def todo : tactic unit := `[exact todo]
+
+end interactive
+end tactic

roadmap/topology/paracompact.lean

@@ -0,0 +1,82 @@
+/-
+Copyright (c) 2020 Reid Barton. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Reid Barton
+-/
+
+import roadmap.todo
+import topology.subset_properties
+import topology.separation
+import topology.metric_space.basic
+
+/-!
+A formal roadmap for basic properties of paracompact spaces.
+
+It contains the statements that compact spaces and metric spaces are paracompact,
+and that paracompact t2 spaces are normal, as well as partially formalised proofs.
+
+Any contributor should feel welcome to contribute complete proofs. When this happens,
+we should also consider preserving the current file as an exemplar of a formal roadmap.
+-/
+
+open set filter
+
+universe u
+
+class paracompact_space (X : Type u) [topological_space X] : Prop :=
+(locally_finite_refinement :
+  ∀ {α : Type u} (u : α → set X) (uo : ∀ a, is_open (u a)) (uc : Union u = univ),
+  ∃ {β : Type u} (v : β → set X) (vo : ∀ b, is_open (v b)) (vc : Union v = univ),
+  locally_finite v ∧ ∀ b, ∃ a, v b ⊆ u a)
+
+/-- Any open cover of a paracompact space has a locally finite *precise* refinement, that is,
+ one indexed on the same type with each open set contained in the corresponding original one. -/
+lemma paracompact_space.precise_refinement {X : Type u} [topological_space X] [paracompact_space X]
+  {α : Type u} (u : α → set X) (uo : ∀ a, is_open (u a)) (uc : Union u = univ) :
+  ∃ v : α → set X, (∀ a, is_open (v a)) ∧ Union v = univ ∧ locally_finite v ∧ (∀ a, v a ⊆ u a) :=
+begin
+  obtain ⟨β, w, wo, wc, lfw, wr⟩ := paracompact_space.locally_finite_refinement u uo uc,
+  choose f hf using wr,
+  refine ⟨λ a, ⋃₀ {s | ∃ b, f b = a ∧ s = w b}, λ a, _, _, _, λ a, _⟩,
+  { apply is_open_sUnion _,
+    rintros t ⟨b, rfl, rfl⟩,
+    apply wo },
+  { todo },
+  { todo },
+  { apply sUnion_subset,
+    rintros t ⟨b, rfl, rfl⟩,
+    apply hf }
+end
+
+lemma paracompact_of_compact {X : Type u} [topological_space X] [compact_space X] :
+  paracompact_space X :=
+begin
+  refine ⟨λ α u uo uc, _⟩,
+  obtain ⟨s, _, sf, sc⟩ :=
+    compact_univ.elim_finite_subcover_image (λ a _, uo a) (by rwa [univ_subset_iff, bUnion_univ]),
+  refine ⟨s, λ b, u b.val, λ b, uo b.val, _, _, λ b, ⟨b.val, subset.refl _⟩⟩,
+  { todo },
+  { intro x,
+    refine ⟨univ, univ_mem_sets, _⟩,
+    todo },
+end
+
+lemma normal_of_paracompact_t2 {X : Type u} [topological_space X] [t2_space X]
+  [paracompact_space X] : normal_space X :=
+todo
+/-
+Similar to the proof of `generalized_tube_lemma`, but different enough not to merge them.
+Lemma: if `s : set X` is closed and can be separated from any point by open sets,
+then `s` can also be separated from any closed set by open sets. Apply twice.
+
+See
+* Bourbaki, General Topology, Chapter IX, §4.4
+* https://ncatlab.org/nlab/show/paracompact+Hausdorff+spaces+are+normal
+-/
+
+lemma paracompact_of_metric {X : Type u} [metric_space X] : paracompact_space X :=
+todo
+/-
+See Mary Ellen Rudin, A new proof that metric spaces are paracompact.
+https://www.ams.org/journals/proc/1969-020-02/S0002-9939-1969-0236876-3/S0002-9939-1969-0236876-3.pdf
+-/

roadmap/topology/shrinking_lemma.lean

@@ -0,0 +1,45 @@
+/-
+Copyright (c) 2020 Reid Barton. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Reid Barton
+-/
+
+/-!
+A formal roadmap for the shrinking lemma for local finite countable covers.
+
+It contains the statement of the lemma, and an informal sketch of the proof,
+along with references.
+
+Any contributor should feel welcome to contribute a formal proof. When this happens,
+we should also consider preserving the current file as an exemplar of a formal roadmap.
+-/
+
+import roadmap.todo
+import topology.separation
+
+open set
+
+universes u v
+
+/-- A point-finite open cover of a closed subset of a normal space can be "shrunk" to a new open cover
+ so that the closure of each new open set is contained in the corresponding original open set. -/
+lemma shrinking_lemma {X : Type u} [topological_space X] [normal_space X]
+  {s : set X} (hs : is_closed s) {α : Type v} (u : α → set X) (uo : ∀ a, is_open (u a))
+  (uf : ∀ x, finite {a | x ∈ u a}) (su : s ⊆ Union u) :
+  ∃ v : α → set X, s ⊆ Union v ∧ ∀ a, is_open (v a) ∧ closure (v a) ⊆ u a :=
+todo
+/-
+Apply Zorn's lemma to
+ T = Σ (i : set α), {v : α → set X // s ⊆ Union v ∧ (∀ a, is_open (v a)) ∧
+                                      (∀ a ∈ i, closure (v a) ⊆ u a) ∧ (∀ a ∉ i, v a = u a)}
+with the ordering
+ ⟨i, v, _⟩ ≤ ⟨i', v', _⟩ ↔ i ⊆ i' ∧ ∀ a ∈ i, v a = v' a
+The hypothesis that `X` is normal implies that a maximal element must have `i = univ`.
+Point-finiteness of `u` (hypothesis `uf`) implies that
+the least upper bound of a chain in `T` again yields a covering of `s`.
+
+Compare proofs in
+* https://ncatlab.org/nlab/show/shrinking+lemma#ShrinkingLemmaForLocallyFiniteCountableCovers
+* Bourbaki, General Topology, Chapter IX, §4.3
+* Dugundji, Topology, Chapter VII, Theorem 6.1
+-/