Decomposition of a restricted product along a finite set of indices #
For a finite set S of indices, a restricted product Πʳ i, [G i, U i] is the product of the
plain product Π i : S, G i of the factors at S with the restricted product away from S: an
element is determined by its coordinates at S, which carry no integrality condition because
finitely many indices never affect restrictedness, and its restriction away from S. This is the
shape in which an adelic group is split into the local groups at a finite set of places times the
restricted product over the remaining places.
The decomposition awayDecomposition S hS U is the composite of three equivalences that are each
coordinatewise the identity: reindexing along Equiv.sumCompl (· ∈ S)
(restrictedProductReindex), the splitting of a restricted product over a sum of index types
(restrictedProductSum), and the collapse of the restricted product over the finite index type
S to the plain product (restrictedProductOfFinite). It is pinned by its coordinate formulas in
both directions, and its second component is the restriction restrictAway S U.
The decomposition is continuous for every reference family. Its inverse is continuous when the
reference subgroups away from S are open; the reference subgroups at S play no role, as
the finite factor carries no integrality condition. The openness hypothesis cannot be dropped: see
not_continuous_awayDecomposition_symm.
Everything here is also stated for additive groups (addAwayDecomposition, …), the form in which
the adeles of a global field split as the completions at a finite set of places times the adeles
away from it.
References #
- N. Bourbaki, General Topology.
- A. Weil, Basic Number Theory.
For a finite set S of indices, the decomposition of a restricted product as the plain
product of the factors at S times the restricted product away from S, coordinatewise the
identity in both directions: x goes to ((x i)_{i ∈ S}, (x i)_{i ∉ S}), and (y, z) goes to
the element with coordinate y ⟨i, _⟩ at i ∈ S and z ⟨i, _⟩ at i ∉ S.
It is the composite of the reindexing along Equiv.sumCompl (· ∈ S), the splitting over the sum
S ⊕ {i // i ∉ S}, and the collapse of the restricted product over the finite index type S.
Instances For
For a finite set S of indices, the decomposition of a
restricted product of additive groups as the plain product of the factors at S times the
restricted product away from S, coordinatewise the identity in both directions: x goes to
((x i)_{i ∈ S}, (x i)_{i ∉ S}), and (y, z) goes to the element with coordinate y ⟨i, _⟩ at
i ∈ S and z ⟨i, _⟩ at i ∉ S.
It is the composite of the reindexing along Equiv.sumCompl (· ∈ S), the splitting over the sum
S ⊕ {i // i ∉ S}, and the collapse of the restricted product over the finite index type S.
Instances For
The first component of the decomposition records the coordinates at S.
The first component of the additive
away-S decomposition records the coordinates at S.
The second component of the decomposition records the coordinates away from S.
Not a simp lemma: simp proves it from awayDecomposition_snd_eq_restrictAway and
restrictAway_apply.
The second component of the additive away-S
decomposition records the coordinates away from S.
Not a simp lemma: simp proves it from addAwayDecomposition_snd_eq_addRestrictAway and
addRestrictAway_apply.
The second component of the decomposition is the restriction away from S.
The second component of
the additive away-S decomposition is the restriction away from S.
At an index i ∈ S, the inverse of the decomposition reads its coordinate off the plain
product over S.
At an index i ∈ S, the
inverse of the additive away-S decomposition reads its coordinate off the plain product
over S.
At an index i ∉ S, the inverse of the decomposition reads its coordinate off the restricted
product away from S.
At an index i ∉ S, the
inverse of the additive away-S decomposition reads its coordinate off the restricted product away
from S.
The decomposition is continuous for every reference family.
The additive away-S decomposition is continuous
for every reference family.
The inverse of the decomposition is continuous when the reference subgroups away from S are
open; the reference subgroups at S play no role, since the finite factor carries no integrality
condition. Together with continuous_awayDecomposition this makes the decomposition a
homeomorphism for such families.
The inverse of the additive away-S
decomposition is continuous when the reference subgroups away from S are open; the reference
subgroups at S play no role, since the finite factor carries no integrality condition. Together
with continuous_addAwayDecomposition this makes the decomposition a homeomorphism for such
families.