feat(order/filter/*): filter.pi is countably generated (#15632)

* rename `filter.has_basis_infi` to `filter.has_basis_infi'`, add new `filter.has_basis_infi`;
* move `prod.is_countably_generated`, golf, add `coprod.is_countably_generated`;
* `is_countably_generated_seq` is no longer an instance, `infi.is_countably_generated` is better;
* add `infi.is_countably_generated` and `pi.is_countably_generated`;
* prove `prod.fist_countable_topology` (from the sphere eversion project) and `pi.first_countable_topology`;
* generalize `pi.second_countable_topology` from `encodable` to `countable` so that it automatically applies to finite types.

src/order/filter/bases.lean

@@ -415,24 +415,37 @@ lemma has_basis.inf {ι ι' : Type*} {p : ι → Prop} {s : ι → set α} {p' :
 (hl.inf' hl').to_has_basis (λ i hi, ⟨⟨i.1, i.2⟩, hi, subset.rfl⟩)
   (λ i hi, ⟨⟨i.1, i.2⟩, hi, subset.rfl⟩)
 
-lemma has_basis_infi {ι : Type*} {ι' : ι → Type*} {l : ι → filter α}
+lemma has_basis_infi' {ι : Type*} {ι' : ι → Type*} {l : ι → filter α}
   {p : Π i, ι' i → Prop} {s : Π i, ι' i → set α} (hl : ∀ i, (l i).has_basis (p i) (s i)) :
   (⨅ i, l i).has_basis (λ If : set ι × Π i, ι' i, If.1.finite ∧ ∀ i ∈ If.1, p i (If.2 i))
     (λ If : set ι × Π i, ι' i, ⋂ i ∈ If.1, s i (If.2 i)) :=
 ⟨begin
   intro t,
   split,
   { simp only [mem_infi', (hl _).mem_iff],
-    rintros ⟨I, hI, V, hV, -, hVt, -⟩,
+    rintros ⟨I, hI, V, hV, -, rfl, -⟩,
     choose u hu using hV,
-    refine ⟨⟨I, u⟩, ⟨hI, λ i _, (hu i).1⟩, _⟩,
-    rw hVt,
-    exact Inter_mono (λ i, Inter_mono $ λ hi, (hu i).2) },
+    exact ⟨⟨I, u⟩, ⟨hI, λ i _, (hu i).1⟩, Inter_mono (λ i, Inter_mono $ λ hi, (hu i).2)⟩ },
   { rintros ⟨⟨I, f⟩, ⟨hI₁, hI₂⟩, hsub⟩,
     refine mem_of_superset _ hsub,
     exact (bInter_mem hI₁).mpr (λ i hi, mem_infi_of_mem i $ (hl i).mem_of_mem $ hI₂ _ hi) }
 end⟩
 
+lemma has_basis_infi {ι : Type*} {ι' : ι → Type*} {l : ι → filter α}
+  {p : Π i, ι' i → Prop} {s : Π i, ι' i → set α} (hl : ∀ i, (l i).has_basis (p i) (s i)) :
+  (⨅ i, l i).has_basis (λ If : Σ I : set ι, Π i : I, ι' i, If.1.finite ∧ ∀ i : If.1, p i (If.2 i))
+    (λ If, ⋂ i : If.1, s i (If.2 i)) :=
+begin
+  refine ⟨λ t, ⟨λ ht, _, _⟩⟩,
+  { rcases (has_basis_infi' hl).mem_iff.mp ht with ⟨⟨I, f⟩, ⟨hI, hf⟩, hsub⟩,
+    exact ⟨⟨I, λ i, f i⟩, ⟨hI, subtype.forall.mpr hf⟩,
+      trans_rel_right _ (Inter_subtype _ _) hsub⟩ },
+  { rintro ⟨⟨I, f⟩, ⟨hI, hf⟩, hsub⟩,
+    refine mem_of_superset _ hsub,
+    casesI hI.nonempty_fintype,
+    exact Inter_mem.2 (λ i, mem_infi_of_mem i $ (hl i).mem_of_mem $ hf _) }
+end
+
 lemma has_basis_infi_of_directed' {ι : Type*} {ι' : ι → Sort*}
   [nonempty ι]
   {l : ι → filter α} (s : Π i, (ι' i) → set α) (p : Π i, (ι' i) → Prop)
@@ -932,9 +945,17 @@ begin
     ⟨hs.to_has_basis.sup ht.to_has_basis, set.to_countable _⟩
 end
 
+instance prod.is_countably_generated (la : filter α) (lb : filter β) [is_countably_generated la]
+  [is_countably_generated lb] : is_countably_generated (la ×ᶠ lb) :=
+filter.inf.is_countably_generated _ _
+
+instance coprod.is_countably_generated (la : filter α) (lb : filter β) [is_countably_generated la]
+  [is_countably_generated lb] : is_countably_generated (la.coprod lb) :=
+filter.sup.is_countably_generated _ _
+
 end is_countably_generated
 
-@[instance] lemma is_countably_generated_seq [encodable β] (x : β → set α) :
+lemma is_countably_generated_seq [encodable β] (x : β → set α) :
   is_countably_generated (⨅ i, 𝓟 $ x i) :=
 begin
   use [range x, countable_range x],
@@ -971,14 +992,18 @@ by { rw ← principal_singleton, exact is_countably_generated_principal _, }
 @[instance] lemma is_countably_generated_top : is_countably_generated (⊤ : filter α) :=
 @principal_univ α ▸ is_countably_generated_principal _
 
-instance is_countably_generated.prod {f : filter α} {g : filter β}
-  [hf : f.is_countably_generated] [hg : g.is_countably_generated] :
-  is_countably_generated (f ×ᶠ g) :=
+instance infi.is_countably_generated {ι : Sort*} [countable ι] (f : ι → filter α)
+  [∀ i, is_countably_generated (f i)] : is_countably_generated (⨅ i, f i) :=
 begin
-  simp_rw is_countably_generated_iff_exists_antitone_basis at hf hg ⊢,
-  rcases hf with ⟨s, hs⟩,
-  rcases hg with ⟨t, ht⟩,
-  refine ⟨_, hs.prod ht⟩,
+  choose s hs using λ i, exists_antitone_basis (f i),
+  rw [← plift.down_surjective.infi_comp],
+  refine has_countable_basis.is_countably_generated
+    ⟨has_basis_infi (λ n, (hs _).to_has_basis), _⟩,
+  haveI := encodable.of_countable (plift ι),
+  refine (countable_range $ sigma.map (coe : finset (plift ι) → set (plift ι)) (λ _, id)).mono _,
+  rintro ⟨I, f⟩ ⟨hI, -⟩,
+  lift I to finset (plift ι) using hI,
+  exact ⟨⟨I, f⟩, rfl⟩
 end
 
 end filter

src/order/filter/pi.lean

@@ -31,6 +31,10 @@ section pi
 /-- The product of an indexed family of filters. -/
 def pi (f : Π i, filter (α i)) : filter (Π i, α i) := ⨅ i, comap (eval i) (f i)
 
+instance pi.is_countably_generated [countable ι] [∀ i, is_countably_generated (f i)] :
+  is_countably_generated (pi f) :=
+infi.is_countably_generated _
+
 lemma tendsto_eval_pi (f : Π i, filter (α i)) (i : ι) :
   tendsto (eval i) (pi f) (f i) :=
 tendsto_infi' i tendsto_comap
@@ -91,7 +95,7 @@ lemma has_basis_pi {ι' : ι → Type} {s : Π i, ι' i → set (α i)} {p : Π
   (pi f).has_basis (λ If : set ι × Π i, ι' i, If.1.finite ∧ ∀ i ∈ If.1, p i (If.2 i))
     (λ If : set ι × Π i, ι' i, If.1.pi (λ i, s i $ If.2 i)) :=
 begin
-  have : (pi f).has_basis _ _ := has_basis_infi (λ i, (h i).comap (eval i : (Π j, α j) → α i)),
+  have : (pi f).has_basis _ _ := has_basis_infi' (λ i, (h i).comap (eval i : (Π j, α j) → α i)),
   convert this,
   ext,
   simp

src/topology/algebra/module/locally_convex.lean

@@ -109,7 +109,7 @@ begin
       ((If.2 i) ∈ @nhds _ ↑i x ∧ convex 𝕜 (If.2 i)))
     (λ x, _) (λ x If hif, convex_Inter $ λ i, convex_Inter $ λ hi, (hif.2 i hi).2),
   rw [nhds_Inf, ← infi_subtype''],
-  exact has_basis_infi (λ i : ts, (@locally_convex_space_iff 𝕜 E _ _ _ ↑i).mp (h ↑i i.2) x),
+  exact has_basis_infi' (λ i : ts, (@locally_convex_space_iff 𝕜 E _ _ _ ↑i).mp (h ↑i i.2) x),
 end
 
 lemma locally_convex_space_infi {ts' : ι → topological_space E}

src/topology/bases.lean

@@ -530,6 +530,20 @@ end first_countable_topology
 
 variables {α}
 
+instance {β} [topological_space β] [first_countable_topology α] [first_countable_topology β] :
+  first_countable_topology (α × β) :=
+⟨λ ⟨x, y⟩, by { rw nhds_prod_eq, apply_instance }⟩
+
+section pi
+
+omit t
+
+instance {ι : Type*} {π : ι → Type*} [countable ι] [Π i, topological_space (π i)]
+  [∀ i, first_countable_topology (π i)] : first_countable_topology (Π i, π i) :=
+⟨λ f, by { rw nhds_pi, apply_instance }⟩
+
+end pi
+
 instance is_countably_generated_nhds_within (x : α) [is_countably_generated (𝓝 x)] (s : set α) :
   is_countably_generated (𝓝[s] x) :=
 inf.is_countably_generated _ _
@@ -622,10 +636,11 @@ instance {β : Type*} [topological_space β]
 ((is_basis_countable_basis α).prod (is_basis_countable_basis β)).second_countable_topology $
   (countable_countable_basis α).image2 (countable_countable_basis β) _
 
-instance second_countable_topology_encodable {ι : Type*} {π : ι → Type*}
-  [encodable ι] [t : ∀a, topological_space (π a)] [∀a, second_countable_topology (π a)] :
+instance {ι : Type*} {π : ι → Type*}
+  [countable ι] [t : ∀a, topological_space (π a)] [∀a, second_countable_topology (π a)] :
   second_countable_topology (∀a, π a) :=
 begin
+  haveI := encodable.of_countable ι,
   have : t = (λa, generate_from (countable_basis (π a))),
     from funext (assume a, (is_basis_countable_basis (π a)).eq_generate_from),
   rw [this, pi_generate_from_eq],
@@ -645,11 +660,6 @@ begin
     exact ⟨s, I, λ i hi, hs ⟨i, hi⟩, set.ext $ λ f, subtype.forall⟩ }
 end
 
-instance second_countable_topology_fintype {ι : Type*} {π : ι → Type*}
-  [fintype ι] [t : ∀a, topological_space (π a)] [∀a, second_countable_topology (π a)] :
-  second_countable_topology (∀a, π a) :=
-by { letI := fintype.to_encodable ι, exact topological_space.second_countable_topology_encodable }
-
 @[priority 100] -- see Note [lower instance priority]
 instance second_countable_topology.to_separable_space
   [second_countable_topology α] : separable_space α :=