Proposition. Transporting double cosets by a group isomorphism [fcap-004S]
Proposition. Transporting double cosets by a group isomorphism [fcap-004S]
Let \(G,G'\) be groups, let \(\Gamma ,K\leq G\) and \(\Gamma ',K'\leq G'\), and let \(e:G\to G'\) be a group isomorphism satisfying \(e(\Gamma )=\Gamma '\) and \(e(K)=K'\). Then the double cosets are related by a bijection \[\begin {aligned} \overline e:\Gamma \backslash G/K&\longrightarrow \Gamma '\backslash G'/K',\\ [x]&\longmapsto [e(x)]. \end {aligned}\] Its inverse sends \([y]\) to \([e^{-1}(y)]\). Both subgroup equalities concern their images in the specified ambient groups.
For the finite adelic class sets, let \(Q,Q'\) be nondegenerate forms on finite-dimensional rational spaces \(V,V'\), with compatible compact-open reference tuples \(U,U'\). Fix one \(H\in \{O,SO,\operatorname {Spin}\}\) and suppose that group isomorphisms \[\phi _p:H(Q_p)\longrightarrow H(Q'_p)\] satisfy \(\phi _p(U_p^H)=U_p^{\prime H}\) at every prime. They induce a group isomorphism \[e_H:H_f(U)\longrightarrow H_f(U'),\qquad (x_p)_p\longmapsto (\phi _p(x_p))_p.\] Indeed, membership in a reference subgroup is equivalent at each coordinate, so a tuple and its image have the same finite exceptional set. The coordinatewise inverse is defined for the same reason; multiplication and the inverse identities hold at every coordinate.
Write \(\Gamma _H(U)=\delta _f^H(H(V,Q))\) and \(\Gamma _H(U')=\delta _f^{\prime H}(H(V',Q'))\) for the actual rational diagonal images. Assume additionally \[e_H(\Gamma _H(U))=\Gamma _H(U').\] Everywhere reference preservation gives \(e_H(\prod _pU_p^H)=\prod _pU_p^{\prime H}\): inclusion follows coordinatewise, and the coordinatewise inverse proves the reverse inclusion. The proposition therefore gives \(\mathcal C_H(U)\simeq \mathcal C_H(U')\), with representatives sent by \((x_p)_p\mapsto (\phi _p(x_p))_p\). The rational-image condition is a separate hypothesis; local group isomorphisms alone do not assert it. For SO use the derived reference subgroups \(i_p^{-1}(U_p^O)\) and \((i'_p)^{-1}(U_p^{\prime O})\); for Spin use its own references and actual generated carrier. The argument applies separately to all three groups, without identifying their rational images.
The adelic objects have classical context in
[conrad2011adelic, Example 2.3, p. 3, and Theorem 3.6, pp. 6-8].
The transport and inverse above are direct group arguments, not
claims quoted from that passage. TauCeti's
DoubleCoset.quotientCongr formalizes the general
equivalence. Its three corresponding specializations are
TauCeti.QuadraticMap.OrthogonalCompactOpens.finiteAdelicOrthogonalDoubleCosetCongr,
TauCeti.QuadraticMap.OrthogonalCompactOpens.finiteAdelicSpecialOrthogonalDoubleCosetCongr
and
TauCeti.QuadraticMap.OrthogonalCompactOpens.finiteAdelicSpinDoubleCosetCongr.
These are equivalences of sets; no continuity of the local
isomorphisms or quotient topology is assumed.