feat(topology/bases): Topological basis of a product. (#7753)

Given a family of topological spaces `X_i` with topological bases `T_i`, this constructs the associated basis of the product topology. 

This also includes a construction of the tautological topological basis consisting of all open sets.

This generalizes a lemma from LTE.

src/topology/bases.lean

@@ -5,6 +5,7 @@ Authors: Johannes Hölzl, Mario Carneiro
 -/
 
 import topology.continuous_on
+import topology.constructions
 
 /-!
 # Bases of topologies. Countability axioms.
@@ -166,6 +167,9 @@ begin
   exact ⟨λ h o hb ⟨a, ha⟩, h a o hb ha, λ h a o hb ha, h o hb ⟨a, ha⟩⟩
 end
 
+protected lemma is_topological_basis.univ : is_topological_basis { U : set α | is_open U } :=
+is_topological_basis_of_open_of_nhds (by tauto) (by tauto)
+
 protected lemma is_topological_basis.prod {β} [topological_space β] {B₁ : set (set α)}
   {B₂ : set (set β)} (h₁ : is_topological_basis B₁) (h₂ : is_topological_basis B₂) :
   is_topological_basis (image2 set.prod B₁ B₂) :=
@@ -179,6 +183,22 @@ begin
     exact ⟨s.prod t, mem_image2_of_mem hs ht, ⟨ha, hb⟩, hu⟩ }
 end
 
+protected lemma is_topological_basis.inducing {β} [topological_space β]
+  {f : α → β} {T : set (set β)} (hf : inducing f) (h : is_topological_basis T) :
+  is_topological_basis {U : set α | ∃ (V : set β), V ∈ T ∧ f ⁻¹' V  = U } :=
+begin
+  refine is_topological_basis_of_open_of_nhds _ _,
+  { rintros _ ⟨V, hV, rfl⟩,
+    rwa hf.is_open_iff,
+    refine ⟨V, h.is_open hV, rfl⟩ },
+  { intros a U ha hU,
+    rw hf.is_open_iff at hU,
+    obtain ⟨V, hV, rfl⟩ := hU,
+    obtain ⟨S, hS, rfl⟩ := h.open_eq_sUnion hV,
+    obtain ⟨W, hW, ha⟩ := ha,
+    refine ⟨f ⁻¹' W, ⟨_, hS hW, rfl⟩, ha, set.preimage_mono $ set.subset_sUnion_of_mem hW⟩ }
+end
+
 lemma is_topological_basis_of_cover {ι} {U  : ι → set α} (Uo : ∀ i, is_open (U i))
   (Uc : (⋃ i, U i) = univ) {b : Π i, set (set (U i))} (hb : ∀ i, is_topological_basis (b i)) :
   is_topological_basis (⋃ i : ι, image (coe : U i → α) '' (b i)) :=
@@ -240,6 +260,82 @@ end topological_space
 
 open topological_space
 
+protected lemma is_topological_basis.pi {ι : Type*} {X : ι → Type*}
+  [∀ i, topological_space (X i)] {T : Π i, set (set (X i))}
+  (cond : ∀ i, is_topological_basis (T i)) :
+  is_topological_basis {S : set (Π i, X i) | ∃ (U : Π i, set (X i)) (F : finset ι),
+    (∀ i, i ∈ F → (U i) ∈ T i) ∧ S = (F : set ι).pi U } :=
+begin
+  classical,
+  refine is_topological_basis_of_open_of_nhds _ _,
+  { rintro _ ⟨U, F, h1, rfl⟩,
+    apply is_open_set_pi F.finite_to_set,
+    intros i hi,
+    exact is_topological_basis.is_open (cond i) (h1 i hi) },
+  { intros a U ha hU,
+    have : U ∈ nhds a := is_open.mem_nhds hU ha,
+    rw [nhds_pi, filter.mem_infi_iff] at this,
+    obtain ⟨F, hF, V, hV1, hV2⟩ := this,
+    choose U' hU' using hV1,
+    obtain ⟨hU1, hU2⟩ := ⟨λ i, (hU' i).1, λ i, (hU' i).2⟩,
+    have : ∀ j : F, ∃ (T' : set (X j)) (hT : T' ∈ T j), a j ∈ T' ∧ T' ⊆ U' j,
+    { intros i,
+      specialize hU1 i,
+      rwa (cond i).mem_nhds_iff at hU1 },
+    choose U'' hU'' using this,
+    let U : Π (i : ι), set (X i) := λ i,
+      if hi : i ∈ F then U'' ⟨i, hi⟩ else set.univ,
+    refine ⟨F.pi U, ⟨U, hF.to_finset, λ i hi, _, by simp⟩, _, _⟩,
+    { dsimp only [U],
+      rw [dif_pos],
+      swap, { simpa using hi },
+      exact (hU'' _).1 },
+    { rw set.mem_pi,
+      intros i hi,
+      dsimp only [U],
+      rw dif_pos hi,
+      exact (hU'' _).2.1 },
+    { intros x hx,
+      apply hV2,
+      rintros - ⟨i, rfl⟩,
+      refine hU2 i ((hU'' i).2.2 _),
+      convert hx i i.2,
+      rcases i with ⟨i, p⟩,
+      dsimp [U],
+      rw dif_pos p, } },
+end
+
+protected lemma is_topological_basis.infi {β : Type*} {ι : Type*} {X : ι → Type*}
+  [t : ∀ i, topological_space (X i)] {T : Π i, set (set (X i))}
+  (cond : ∀ i, is_topological_basis (T i)) (f : Π i, β → X i) :
+  @is_topological_basis β (⨅ i, induced (f i) (t i))
+  { S | ∃ (U : Π i, set (X i)) (F : finset ι),
+    (∀ i, i ∈ F → U i ∈ T i) ∧ S = ⋂ i (hi : i ∈ F), (f i) ⁻¹' (U i) } :=
+begin
+  convert is_topological_basis.inducing
+    (inducing_infi_to_pi _) (is_topological_basis.pi cond),
+  ext V,
+  split,
+  { rintros ⟨U, F, h1, h2⟩,
+    have : (F : set ι).pi U = (⋂ (i : ι) (hi : i ∈ F),
+        (λ (z : Π j, X j), z i) ⁻¹' (U i)), by { ext, simp },
+    refine ⟨(F : set ι).pi U, ⟨U, F, h1, rfl⟩, _⟩,
+    rw [this, h2, set.preimage_Inter],
+    congr' 1,
+    ext1,
+    rw set.preimage_Inter,
+    refl },
+  { rintros ⟨U, ⟨U, F, h1, rfl⟩, h⟩,
+    refine ⟨U, F, h1, _⟩,
+    have : (F : set ι).pi U = (⋂ (i : ι) (hi : i ∈ F),
+        (λ (z : Π j, X j), z i) ⁻¹' (U i)), by { ext, simp },
+    rw [← h, this, set.preimage_Inter],
+    congr' 1,
+    ext1,
+    rw set.preimage_Inter,
+    refl }
+end
+
 /-- If `α` is a separable space and `f : α → β` is a continuous map with dense range, then `β` is
 a separable space as well. E.g., the completion of a separable uniform space is separable. -/
 protected lemma dense_range.separable_space {α β : Type*} [topological_space α] [separable_space α]

src/topology/constructions.lean

@@ -765,6 +765,21 @@ begin
       simpa [pi_if, hf] } }
 end
 
+/-- Suppose `π i` is a family of topological spaces indexed by `i : ι`, and `X` is a type
+endowed with a family of maps `f i : X → π i` for every `i : ι`, hence inducing a
+map `g : X → Π i, π i`. This lemma shows that infimum of the topologies on `X` induced by
+the `f i` as `i : ι` varies is simply the topology on `X` induced by `g : X → Π i, π i`
+where `Π i, π i` is endowed with the usual product topology. -/
+lemma inducing_infi_to_pi {X : Type*} [∀ i, topological_space (π i)] (f : Π i, X → π i) :
+  @inducing X (Π i, π i) (⨅ i, induced (f i) infer_instance) _ (λ x i, f i x) :=
+begin
+  constructor,
+  erw induced_infi,
+  congr' 1,
+  funext,
+  erw induced_compose,
+end
+
 variables [fintype ι] [∀ i, topological_space (π i)] [∀ i, discrete_topology (π i)]
 
 /-- A finite product of discrete spaces is discrete. -/