countable union of open 2nd countable; set v type

Stream: mathlib4

[Kevin Buzzard]

I am looking for design advice. Mathlib has docs#TopologicalSpace.secondCountableTopology_of_countable_cover which says that a countable union of SecondCountableTopology open subsets of a type is second countable. Note that this lemma has the coercion of a set to a type in its statement, as we don't seem to have a predicate on subsets of a top space saying "I am second countable". But I have a top space equipped with a family of open immersions from other second countable topological spaces, so the lemma does not apply directly. What I need in my situation is this variant:

import Mathlib

lemma TopologicalSpace.secondCountableTopology_of_countable_cover' {α : Type*}
    [TopologicalSpace α] {ι : Sort*} [Countable ι] {U : ι → Type*} [∀ i, TopologicalSpace (U i)]
    [∀ (i : ι), SecondCountableTopology (U i)]
    (f : ∀ i, U i → α) (hf : ∀ i, Topology.IsOpenEmbedding (f i))
    (hc : ∀ a, ∃ (i : ι) (u : U i), f i u = a) : SecondCountableTopology α :=
  sorry

It seems to me that there are several ways to proceed. I could try deducing a type version of the lemma (with a family of open immersions instead of a family of open subsets) from the set version, which needs that the image of a second countable top space under an open immersion is second countable; my inept attempt to this is below: I assume there's a much cleaner proof.

import Mathlib

lemma SecondCountableTopology.range {X Y : Type*} [TopologicalSpace X] [TopologicalSpace Y]
    {f : X → Y} (hf : Topology.IsOpenEmbedding f) [SecondCountableTopology X] :
    SecondCountableTopology (Set.range f) := by
  apply Topology.IsQuotientMap.secondCountableTopology (π := Set.rangeFactorization f)
  · constructor
    · exact Set.rangeFactorization_surjective
    · rw [hf.isInducing.1]
      apply le_antisymm
      · intro W ⟨V, hV, h⟩
        rw [Set.ext_iff] at h
        refine ⟨V, hV, ?_⟩
        ext ⟨-, x, rfl⟩
        simpa using h x
      · intro W ⟨V, hV, hVW⟩
        refine ⟨V, hV, ?_⟩
        rw [← hVW]
        grind only
  · intro U hU
    rw [hf.isInducing.1] at hU
    obtain ⟨V, hV, rfl⟩ := hU
    refine ⟨V, hV, ?_⟩
    ext ⟨-, x, rfl⟩
    have := hf.injective
    simp [Set.rangeFactorization]
    grind

Having written such messy code I wondered if instead I should just be proving the result directly, i.e, follow the method of the proof of secondCountableTopology_of_countable_cover rather than trying to reuse the proof itself. But the proof uses docs#TopologicalSpace.isTopologicalBasis_of_cover which itself has some really horrible conclusion involving IsTopologicalBasis (⋃ i, image Subtype.val '' b i)which I'd also have to generalise because my maps aren't Subtype.val.

Can someone who understands the topology part of the library suggest what I should be doing here?

---

To un- #xy : what I actually want is that the adeles are second countable, which I propose to prove via showing that a countable restricted product (wrt cofinite filter) of second countable sets wrt open subsets is second countable . Mathematically the proof is this: a countable product of second countable is second countable, and a restricted product $\prod'_i (X_i,U_i)$ is set-theoretically equal to the union of the open subsets $\prod_{i\in S}X_i\times\prod_{i\not\in S}U_i$ where $S$ runs through finite subsets of the index set. But we do not have these subsets in the restricted product API: they are thought of as distinct types because the products $\prod_{i\in S}X_i\times\prod_{i\not\in S}U_i$ are also restricted products, this time with respect to principal filters, and the inclusions are given by docs#RestrictedProduct.inclusion; the fact that these maps are open embeddings is given by docs#RestrictedProduct.isOpenEmbedding_inclusion_principal .

[Aaron Liu]

here's my version

import Mathlib

lemma TopologicalSpace.secondCountableTopology_of_countable_cover' {α : Type*}
    [TopologicalSpace α] {ι : Sort*} [Countable ι] {U : ι → Type*} [∀ i, TopologicalSpace (U i)]
    [∀ (i : ι), SecondCountableTopology (U i)]
    (f : ∀ i, U i → α) (hf : ∀ i, Topology.IsOpenEmbedding (f i))
    (hc : ∀ a, ∃ (i : ι) (u : U i), f i u = a) : SecondCountableTopology α :=
  let V i := Set.range (f i)
  have (i : ι) : SecondCountableTopology (V i) :=
    (hf i).toHomeomorph.symm.secondCountableTopology
  have Vo (i : ι) : IsOpen (V i) := (hf i).isOpen_range
  have hV : ⋃ i, V i = Set.univ := Set.eq_univ_of_forall fun a =>
    (hc a).elim fun i hi => Set.mem_iUnion_of_mem i (Set.mem_range.2 hi)
  secondCountableTopology_of_countable_cover Vo hV

[Kevin Buzzard]

That looks much better! Thanks!

[Kevin Buzzard]

Aha, it's docs#Topology.IsEmbedding.toHomeomorph which I was missing.

[Anatole Dedecker]

Yes, this is morally the key lemma saying that an open embedding is really an open subset. In a lot of cases we prove the open embedding version of the lemma first, but in the specific case of bases of topology it’s often more natural to start with the version about open subsets

[Kevin Buzzard]

Very pleased with how this has come out:

import Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace

-- Aaron Liu's version -- for mathlib
lemma TopologicalSpace.secondCountableTopology_of_countable_cover' {α : Type*}
    [TopologicalSpace α] {ι : Sort*} [Countable ι] {U : ι → Type*} [∀ i, TopologicalSpace (U i)]
    [∀ (i : ι), SecondCountableTopology (U i)]
    (f : ∀ i, U i → α) (hf : ∀ i, Topology.IsOpenEmbedding (f i))
    (hc : ∀ a, ∃ (i : ι) (u : U i), f i u = a) : SecondCountableTopology α :=
  let V i := Set.range (f i)
  have (i : ι) : SecondCountableTopology (V i) :=
    (hf i).toHomeomorph.symm.secondCountableTopology
  have Vo (i : ι) : IsOpen (V i) := (hf i).isOpen_range
  have hV : ⋃ i, V i = Set.univ := Set.eq_univ_of_forall fun a =>
    (hc a).elim fun i hi => Set.mem_iUnion_of_mem i (Set.mem_range.2 hi)
  secondCountableTopology_of_countable_cover Vo hV

lemma Filter.cofinite.sets.countable (ι : Type*) [Countable ι] :
    (Filter.cofinite : Filter ι).sets.Countable :=
  Set.Countable.mono (fun _ h ↦ h) <|
  Set.Countable.preimage_of_injOn Set.Countable.setOf_finite compl_bijective.1.injOn

instance (ι : Type*) [Countable ι] : Countable (.cofinite : Filter ι).sets := by
  rw [Set.countable_coe_iff]
  exact Filter.cofinite.sets.countable ι

open RestrictedProduct Filter in
instance RestrictedProduct.SecondCountableTopology_of_principal
    {ι : Type*} [Countable ι]
    (X : ι → Type*) [∀ i, TopologicalSpace (X i)]
    (C : (i : ι) → Set (X i))
    [∀ i, SecondCountableTopology (X i)]
    {S : Set ι} :
    SecondCountableTopology (Πʳ i, [X i, C i]_[𝓟 S]) :=
  isEmbedding_coe_of_principal.secondCountableTopology

open Filter RestrictedProduct in
lemma RestrictedProduct.secondCountableTopology {ι : Type*} [Countable ι]
    (X : ι → Type*) [∀ i, TopologicalSpace (X i)]
    (C : (i : ι) → Set (X i)) (hCopen : ∀ (i : ι), IsOpen (C i))
    [∀ i, SecondCountableTopology (X i)] :
    SecondCountableTopology (Πʳ i, [X i, C i]) :=
  TopologicalSpace.secondCountableTopology_of_countable_cover'
    (fun S : (.cofinite : Filter ι).sets ↦ inclusion X C (Filter.le_principal_iff.2 S.2))
    (fun S ↦ RestrictedProduct.isOpenEmbedding_inclusion_principal hCopen
        (Filter.le_principal_iff.2 S.2))
    (fun f ↦ ⟨⟨_, f.2⟩, ⟨f.1, by aesop⟩, rfl⟩)

So in FLT we also have that adeles are locally compact (this boils down to statements in arithmetic) and Hausdorff (this is easy), so now they're Polish (by #FLT > Are the adeles Polish? @ 💬 ) which Anatole is arguing is not the right way to do it but I suspect I'll need second countability in other places too.