The adelic subgroup U_1(S) of (D tensor A_F^infty)^* is compact and open

[kbuzzard]

I have not yet written down a clear path to this and may come back to this issue later on.

The proof is: the rigidification M_2(A_F^f)=D tensor A_F^f is a homeomorphism because it's an isomorphism of finite A_F^-modules with the module topology. So it suffices to prove that the subgroup U_1(S) of GL_2(A_F^f) is compact and open. If we know that the local factors are compact and open this is enough (for openness, use that the local factors are the full subgroup GL_2(O_v) for all but finitely many v). This reduces the claim to the following:

1. GL_2(O_v) is open and compact in GL_2(F_v) if F is a number field and v is a finite place
2. the "local U_1(v)" (i.e. matrices in GL_2(O_v) which are congruent to (a *;0 a) mod v) are open and compact.

Really we should be proving these results for all nonarchimedean local fields, however nonarchimedean local fields are not yet in mathlib.
I want to deduce these results from facts like "units of an open submonoid of a topological monoid are open" and "units of a compact submonoid of a Hausdorff topological monoid are compact" but these are other (much easier) issues.

People are welcome to claim this issue but right now we will need to build a fair amount of infrastructure and perhaps break the problem down into smaller issues.

[bwangpj]

claim