second countable topology question

Stream: Is there code for X?

[Kevin Buzzard]

Is this true? (surely it is but I can't find it; probably something more general is true):

import Mathlib

theorem Topology.IsClosedEmbedding.secondCountableTopology
    {X : Type*} {Y : Type*} [TopologicalSpace X]
    [TopologicalSpace Y] [SecondCountableTopology Y] {f : X → Y}
    (hf : Topology.IsClosedEmbedding f) :
    SecondCountableTopology X := sorry

I want it (or something like it) to prove that the infinite adeles of a number field are second countable; the infinite adeles of a number field are nothing more than $\mathbb{R}^r\times\mathbb{C}^s$ for $r,s$ naturals depending on the arithmetic of the field, so the result I actually want is certainly true, but I was trying to prove it in a mathlib-like way, and the analogue of the plan below is how we prove that they're a locally compact space (see docs#AbsoluteValue.Completion.locallyCompactSpace).

import Mathlib

theorem Topology.IsClosedEmbedding.secondCountableTopology
    {X : Type*} {Y : Type*} [TopologicalSpace X]
    [TopologicalSpace Y] [SecondCountableTopology Y] {f : X → Y}
    (hf : Topology.IsClosedEmbedding f) :
    SecondCountableTopology X := sorry

theorem AbsoluteValue.Completion.secondCountableTopology
    {K : Type*} [Field K] {v : AbsoluteValue K ℝ} {L : Type*}
    [NormedField L] [CompleteSpace L] {f : WithAbs v →+* L}
    [SecondCountableTopology L] (h : Isometry f) :
    SecondCountableTopology v.Completion :=
  h.completion_extension.isClosedEmbedding.secondCountableTopology

instance NumberField.InfinitePlace.Completion.secondCountableTopology
    {K : Type*} [Field K] (v : InfinitePlace K) :
    SecondCountableTopology (v.Completion) :=
  AbsoluteValue.Completion.secondCountableTopology v.isometry_embedding

open NumberField in
instance (K : Type*) [Field K] [NumberField K] :
    SecondCountableTopology (InfiniteAdeleRing K) :=
  inferInstanceAs <| SecondCountableTopology (Π _, _)

[Sébastien Gouëzel]

docs#Topology.IsInducing.secondCountableTopology

[Sébastien Gouëzel]

(This means that in your snippet you just need to remove the theorem Topology.IsClosedEmbedding.secondCountableTopology, and then everything goes through by the magic of dot notation going to subclasses)

[Kevin Buzzard]

Perfect thanks! So one trick when searching is to know the right generality for the statement :-)

[William Coram]

To piggy back this discussion, I also need

instance (K : Type*) [Field K] [NumberField K] (D : Type*) [DivisionRing D]
        [Algebra K D]  [FiniteDimensional K D] :
        SecondCountableTopology (D ⊗[K] InfiniteAdeleRing K) :
    sorry

Is there an easy immediate way to get this from Kevin's instance of SecondCountableTopology (InfiniteAdeleRing K)?

[Kevin Buzzard]

I'm not sure that type even has a topology in mathlib but in FLT it will be the usual trick of picking a basis.

[William Coram]

I was hoping I could've avoided doing explicit basis work (i.e. someone had already done the hard work for me). Maybe I could prove a general result saying something like: tensoring a SecondCountableTopology space with a finite module (unsure what generality this could be - certainly need countable basis on the other side too) gives something second countable.

[Kevin Buzzard]

Right -- I don't think that work has been done though because it won't be in mathlib because the topology isn't in mathlib. You're right about the general statement but it'll have to be an FLT thing in the same file where we make $A\otimes B$ a $B$-module.