The topology on the units of a restricted product

Let R i be topological monoids with submonoids B i. Mathlib's RestrictedProduct.unitsEquiv identifies, as groups, the units of the restricted product Πʳ i, [R i, B i] with the restricted product Πʳ i, [(R i)ˣ, (B i)ˣ] of the unit groups. The two sides carry natural topologies: the units of a topological monoid have the topology induced by x ↦ (x, x⁻¹), while the restricted product of the unit groups has its restricted-product topology, built from the units topologies of the factors. This file shows that these topologies agree for the cofinite filter of indices when every B i is open, so that RestrictedProduct.unitsEquiv is then an isomorphism of topological groups. The inverse comparison map is continuous for every filter of indices, with no openness assumption.

For the finite adele ring of a Dedekind domain this is the statement that the topology of the finite ideles, as units of the finite adeles, is the restricted-product topology of the local unit groups K_vˣ with respect to the local integral units 𝒪_vˣ.

Main results

• RestrictedProduct.continuous_unitsEquiv: for the cofinite filter of indices, the comparison map from the units of the restricted product to the restricted product of the units is continuous when every B i is open.
• RestrictedProduct.continuous_unitsEquiv_symm: its inverse is continuous, for every filter of indices and arbitrary submonoids B i.
• ContinuousMulEquiv.restrictedProductUnits: the resulting isomorphism of topological groups (Πʳ i, [R i, B i])ˣ ≃ₜ* Πʳ i, [(R i)ˣ, (B i)ˣ] (cofinite filter, every B i open).

References

• J. W. S. Cassels and A. Fröhlich, eds., Algebraic Number Theory, Chapter II, §16.
• A. Weil, Basic Number Theory, Chapter IV, §3.

theorem RestrictedProduct.continuous_unitsEquiv_symm {ι : Type u_1} {R : ι → Type u_2} [(i : ι) → Monoid (R i)] [(i : ι) → TopologicalSpace (R i)] {S : ι → Type u_3} [(i : ι) → SetLike (S i) (R i)] [∀ (i : ι), SubmonoidClass (S i) (R i)] {B : (i : ι) → S i} {𝓕 : Filter ι} : Continuous ⇑(unitsEquiv R).symm

The comparison of the units of a restricted product with the restricted product of the unit groups has a continuous inverse, for every filter of indices.

theorem RestrictedProduct.continuous_unitsEquiv {ι : Type u_1} {R : ι → Type u_2} [(i : ι) → Monoid (R i)] [(i : ι) → TopologicalSpace (R i)] {S : ι → Type u_3} [(i : ι) → SetLike (S i) (R i)] [∀ (i : ι), SubmonoidClass (S i) (R i)] {B : (i : ι) → S i} (hB : ∀ (i : ι), IsOpen ↑(B i)) : Continuous ⇑(unitsEquiv R)

The units topology of a restricted product is the restricted-product topology of the unit groups, when every B i is open: the comparison map RestrictedProduct.unitsEquiv from the units of Πʳ i, [R i, B i] to Πʳ i, [(R i)ˣ, (B i)ˣ] is continuous.

noncomputable def ContinuousMulEquiv.restrictedProductUnits {ι : Type u_1} {R : ι → Type u_2} [(i : ι) → Monoid (R i)] [(i : ι) → TopologicalSpace (R i)] {S : ι → Type u_3} [(i : ι) → SetLike (S i) (R i)] [∀ (i : ι), SubmonoidClass (S i) (R i)] {B : (i : ι) → S i} (hB : ∀ (i : ι), IsOpen ↑(B i)) : (RestrictedProduct (fun (i : ι) => R i) (fun (i : ι) => ↑(B i)) Filter.cofinite)ˣ ≃ₜ* RestrictedProduct (fun (i : ι) => (R i)ˣ) (fun (i : ι) => ↑(Submonoid.ofClass (B i)).units) Filter.cofinite

The units of a restricted product are the restricted product of the units, as topological groups: when every B i is open, RestrictedProduct.unitsEquiv is a homeomorphism from the units of Πʳ i, [R i, B i], with the units topology, to Πʳ i, [(R i)ˣ, (B i)ˣ], with the restricted-product topology of the units topologies.

@[simp]

theorem ContinuousMulEquiv.toMulEquiv_restrictedProductUnits {ι : Type u_1} {R : ι → Type u_2} [(i : ι) → Monoid (R i)] [(i : ι) → TopologicalSpace (R i)] {S : ι → Type u_3} [(i : ι) → SetLike (S i) (R i)] [∀ (i : ι), SubmonoidClass (S i) (R i)] {B : (i : ι) → S i} (hB : ∀ (i : ι), IsOpen ↑(B i)) : ↑(restrictedProductUnits hB) = RestrictedProduct.unitsEquiv R

The underlying group isomorphism of ContinuousMulEquiv.restrictedProductUnits is RestrictedProduct.unitsEquiv.

theorem ContinuousMulEquiv.restrictedProductUnits_apply {ι : Type u_1} {R : ι → Type u_2} [(i : ι) → Monoid (R i)] [(i : ι) → TopologicalSpace (R i)] {S : ι → Type u_3} [(i : ι) → SetLike (S i) (R i)] [∀ (i : ι), SubmonoidClass (S i) (R i)] {B : (i : ι) → S i} (hB : ∀ (i : ι), IsOpen ↑(B i)) (x : (RestrictedProduct (fun (i : ι) => R i) (fun (i : ι) => ↑(B i)) Filter.cofinite)ˣ) : (restrictedProductUnits hB) x = (RestrictedProduct.unitsEquiv R) x

ContinuousMulEquiv.restrictedProductUnits is computed by RestrictedProduct.unitsEquiv.

@[simp]

theorem ContinuousMulEquiv.coe_restrictedProductUnits_apply {ι : Type u_1} {R : ι → Type u_2} [(i : ι) → Monoid (R i)] [(i : ι) → TopologicalSpace (R i)] {S : ι → Type u_3} [(i : ι) → SetLike (S i) (R i)] [∀ (i : ι), SubmonoidClass (S i) (R i)] {B : (i : ι) → S i} (hB : ∀ (i : ι), IsOpen ↑(B i)) (x : (RestrictedProduct (fun (i : ι) => R i) (fun (i : ι) => ↑(B i)) Filter.cofinite)ˣ) (i : ι) : ↑(((restrictedProductUnits hB) x) i) = ↑x i

The coordinates of the image of a unit under ContinuousMulEquiv.restrictedProductUnits are the coordinates of that unit.

@[simp]

theorem ContinuousMulEquiv.restrictedProductUnits_symm_apply_apply {ι : Type u_1} {R : ι → Type u_2} [(i : ι) → Monoid (R i)] [(i : ι) → TopologicalSpace (R i)] {S : ι → Type u_3} [(i : ι) → SetLike (S i) (R i)] [∀ (i : ι), SubmonoidClass (S i) (R i)] {B : (i : ι) → S i} (hB : ∀ (i : ι), IsOpen ↑(B i)) (y : RestrictedProduct (fun (i : ι) => (R i)ˣ) (fun (i : ι) => ↑(Submonoid.ofClass (B i)).units) Filter.cofinite) (i : ι) : ↑((restrictedProductUnits hB).symm y) i = ↑(y i)

The coordinates of the unit attached by ContinuousMulEquiv.restrictedProductUnits to a restricted family of units are the given units.