Proposition. Enlarging the right subgroup of a double coset [fcap-004Q]

Let \(G\) be a group and let \(\Gamma ,K,K'\) be subgroups of \(G\), with \(K\subseteq K'\). Write \([x]_K\) for the double coset \(\Gamma xK\); throughout, \(\Gamma \) is fixed. There is a surjection \[\begin {aligned} p_{K,K'}:\Gamma \backslash G/K&\longrightarrow \Gamma \backslash G/K',\\ [x]_K&\longmapsto [x]_{K'}. \end {aligned}\] Thus allowing more right transformations can identify classes that were previously distinct.

Injectivity fails even for the group \(C_2=\{1,s\}\), where \(s^2=1\) and \(s\ne 1\). Take \(\Gamma =K=\{1\}\) and \(K'=C_2\). The source classes are exactly \(\{1\}\) and \(\{s\}\): with both witnesses equal to \(1\), two representatives are equivalent only when they are equal. The target has the single class \(C_2\), because \(\Gamma xK'=xC_2=C_2\) for each \(x\). Hence precisely two source classes map to one target class. This is a general-group counterexample, without an asserted adelic realization.

For the finite adelic class sets, fix a nondegenerate quadratic form \(Q\) on a finite-dimensional rational space \(V\) and one compatible compact-open reference tuple \(U\). Apply the proposition separately with \[(G,\Gamma ,K)= \bigl (H_f(U),\delta _f^H(H(V,Q)),K_H\bigr ), \qquad H\in \{O,SO,\operatorname {Spin}\}.\] Here the ambient restricted group is from Definition [fcap-004F], the rational image is from Definition [fcap-004K], and \(K_H\) is the actual product reference subgroup. Any subgroup \(K'_H\) of that same \(H_f(U)\) containing \(K_H\) gives the stated surjection. An enlargement of reference families does not by itself keep the ambient restricted product fixed; the proposition applies only after the ambient group and the rational diagonal have been identified.

The adelic objects have classical context in [conrad2011adelic, Example 2.3, p. 3, and Theorem 3.6, pp. 6-8]. The quotient map and counterexample above are elementary group arguments, not assertions quoted from that source. TauCeti's DoubleCoset.quotientMapOfLERight_surjective formalizes the general surjectivity statement. Its separate adelic specializations are TauCeti.QuadraticMap.OrthogonalCompactOpens.finiteAdelicOrthogonalDoubleCosetMapOfLE_surjective, TauCeti.QuadraticMap.OrthogonalCompactOpens.finiteAdelicSpecialOrthogonalDoubleCosetMapOfLE_surjective and TauCeti.QuadraticMap.OrthogonalCompactOpens.finiteAdelicSpinDoubleCosetMapOfLE_surjective. No finiteness of these quotient sets is needed.