Restricted products of groups away from a set of indices

This file names the restricted product of a family of groups relative to a family of reference subgroups over the indices outside a set S. This is the shape in which restricted products appear when the local groups at a finite set of places are set apart from the rest of an adelic group: the finite adelic points away from a finite set of places.

It then constructs the restriction homomorphism from the restricted product to the restricted product away from S, which forgets the coordinates indexed by S. This is Mathlib's RestrictedProduct.mapAlongMonoidHom along the inclusion {i // i ∉ S} → ι, which carries the cofinite filter to the cofinite filter because it is injective. Its coordinate formula, its continuity for every reference family, and its compatibility with nested index sets are the facts the decomposition awayDecomposition of a restricted product along a finite set of indices needs.

No finiteness of S is assumed anywhere: the away-S restricted product and the restriction to it make sense for every set of indices.

When S is empty, awayEmptyEquiv is the canonical reindexing to the original restricted product, with inverse restrictAway ∅. Both directions are continuous for every reference family; awayEmptyContinuousMulEquiv packages them as an isomorphism of topological groups. Its additive counterpart is addAwayEmptyContinuousAddEquiv.

Everything here is also stated for additive groups (RestrictedProductAddGroupAway, addRestrictAway, …).

References

• N. Bourbaki, General Topology.
• A. Weil, Basic Number Theory.

@[reducible, inline]

abbrev TauCeti.RestrictedProductGroupAway {ι : Type u} {G : ι → Type v} [(i : ι) → Group (G i)] (S : Set ι) (U : (i : ι) → Subgroup (G i)) : Type (max u v)

The restricted product of G relative to U over the indices outside S. This is RestrictedProductGroup at the index type {i // i ∉ S}; no finiteness of S is needed to form it.

@[reducible, inline]

abbrev TauCeti.RestrictedProductAddGroupAway {ι : Type u} {G : ι → Type v} [(i : ι) → AddGroup (G i)] (S : Set ι) (U : (i : ι) → AddSubgroup (G i)) : Type (max u v)

The restricted product of the family of additive groups G relative to U over the indices outside S. This is RestrictedProductAddGroup at the index type {i // i ∉ S}; no finiteness of S is needed to form it.

def TauCeti.restrictAway {ι : Type u} {G : ι → Type v} [(i : ι) → Group (G i)] (S : Set ι) (U : (i : ι) → Subgroup (G i)) : RestrictedProductGroup U →* RestrictedProductGroupAway S U

Restriction of a restricted product to the indices outside S, forgetting the coordinates indexed by S.

def TauCeti.addRestrictAway {ι : Type u} {G : ι → Type v} [(i : ι) → AddGroup (G i)] (S : Set ι) (U : (i : ι) → AddSubgroup (G i)) : RestrictedProductAddGroup U →+ RestrictedProductAddGroupAway S U

Restriction of a restricted product of additive groups to the indices outside S, forgetting the coordinates indexed by S.

@[simp]

theorem TauCeti.restrictAway_apply {ι : Type u} {G : ι → Type v} [(i : ι) → Group (G i)] (S : Set ι) (U : (i : ι) → Subgroup (G i)) (x : RestrictedProductGroup U) (i : { i : ι // i ∉ S }) : ((restrictAway S U) x) i = x ↑i

The restriction away from S keeps the coordinates outside S unchanged.

@[simp]

theorem TauCeti.addRestrictAway_apply {ι : Type u} {G : ι → Type v} [(i : ι) → AddGroup (G i)] (S : Set ι) (U : (i : ι) → AddSubgroup (G i)) (x : RestrictedProductAddGroup U) (i : { i : ι // i ∉ S }) : ((addRestrictAway S U) x) i = x ↑i

The restriction away from S of a restricted product of additive groups keeps the coordinates outside S unchanged.

def TauCeti.awayEmptyEquiv {ι : Type u} {G : ι → Type v} [(i : ι) → Group (G i)] (U : (i : ι) → Subgroup (G i)) : RestrictedProductGroupAway ∅ U ≃* RestrictedProductGroup U

Removing an empty set of indices recovers the original restricted product, by the canonical reindexing which forgets the vacuous proof that an index is outside the empty set.

def TauCeti.addAwayEmptyEquiv {ι : Type u} {G : ι → Type v} [(i : ι) → AddGroup (G i)] (U : (i : ι) → AddSubgroup (G i)) : RestrictedProductAddGroupAway ∅ U ≃+ RestrictedProductAddGroup U

Removing an empty set of indices recovers the original restricted product of additive groups, by the canonical reindexing which forgets the vacuous proof that an index is outside the empty set.

@[simp]

theorem TauCeti.awayEmptyEquiv_apply {ι : Type u} {G : ι → Type v} [(i : ι) → Group (G i)] (U : (i : ι) → Subgroup (G i)) (x : RestrictedProductGroupAway ∅ U) (i : ι) : ((awayEmptyEquiv U) x) i = x ⟨i, ⋯⟩

The empty-away comparison preserves each coordinate.

@[simp]

theorem TauCeti.addAwayEmptyEquiv_apply {ι : Type u} {G : ι → Type v} [(i : ι) → AddGroup (G i)] (U : (i : ι) → AddSubgroup (G i)) (x : RestrictedProductAddGroupAway ∅ U) (i : ι) : ((addAwayEmptyEquiv U) x) i = x ⟨i, ⋯⟩

@[simp]

theorem TauCeti.awayEmptyEquiv_restrictAway {ι : Type u} {G : ι → Type v} [(i : ι) → Group (G i)] (U : (i : ι) → Subgroup (G i)) (x : RestrictedProductGroup U) : (awayEmptyEquiv U) ((restrictAway ∅ U) x) = x

Restriction away from the empty set is the inverse of the canonical comparison.

@[simp]

theorem TauCeti.addAwayEmptyEquiv_restrictAway {ι : Type u} {G : ι → Type v} [(i : ι) → AddGroup (G i)] (U : (i : ι) → AddSubgroup (G i)) (x : RestrictedProductAddGroup U) : (addAwayEmptyEquiv U) ((addRestrictAway ∅ U) x) = x

@[simp]

theorem TauCeti.awayEmptyEquiv_symm_apply {ι : Type u} {G : ι → Type v} [(i : ι) → Group (G i)] (U : (i : ι) → Subgroup (G i)) (x : RestrictedProductGroup U) : (awayEmptyEquiv U).symm x = (restrictAway ∅ U) x

The inverse empty-away comparison is restriction away from the empty set.

@[simp]

theorem TauCeti.addAwayEmptyEquiv_symm_apply {ι : Type u} {G : ι → Type v} [(i : ι) → AddGroup (G i)] (U : (i : ι) → AddSubgroup (G i)) (x : RestrictedProductAddGroup U) : (addAwayEmptyEquiv U).symm x = (addRestrictAway ∅ U) x

theorem TauCeti.continuous_awayEmptyEquiv {ι : Type u} {G : ι → Type v} [(i : ι) → Group (G i)] [(i : ι) → TopologicalSpace (G i)] (U : (i : ι) → Subgroup (G i)) : Continuous ⇑(awayEmptyEquiv U)

The canonical empty-away comparison is continuous for every reference family.

theorem TauCeti.continuous_addAwayEmptyEquiv {ι : Type u} {G : ι → Type v} [(i : ι) → AddGroup (G i)] [(i : ι) → TopologicalSpace (G i)] (U : (i : ι) → AddSubgroup (G i)) : Continuous ⇑(addAwayEmptyEquiv U)

theorem TauCeti.continuous_awayEmptyEquiv_symm {ι : Type u} {G : ι → Type v} [(i : ι) → Group (G i)] [(i : ι) → TopologicalSpace (G i)] (U : (i : ι) → Subgroup (G i)) : Continuous ⇑(awayEmptyEquiv U).symm

The inverse empty-away comparison is continuous for every reference family.

theorem TauCeti.continuous_addAwayEmptyEquiv_symm {ι : Type u} {G : ι → Type v} [(i : ι) → AddGroup (G i)] [(i : ι) → TopologicalSpace (G i)] (U : (i : ι) → AddSubgroup (G i)) : Continuous ⇑(addAwayEmptyEquiv U).symm

def TauCeti.awayEmptyContinuousMulEquiv {ι : Type u} {G : ι → Type v} [(i : ι) → Group (G i)] [(i : ι) → TopologicalSpace (G i)] (U : (i : ι) → Subgroup (G i)) : RestrictedProductGroupAway ∅ U ≃ₜ* RestrictedProductGroup U

The canonical empty-away comparison as an isomorphism of topological groups.

def TauCeti.addAwayEmptyContinuousAddEquiv {ι : Type u} {G : ι → Type v} [(i : ι) → AddGroup (G i)] [(i : ι) → TopologicalSpace (G i)] (U : (i : ι) → AddSubgroup (G i)) : RestrictedProductAddGroupAway ∅ U ≃ₜ+ RestrictedProductAddGroup U

The canonical empty-away comparison as an isomorphism of topological additive groups.

@[simp]

theorem TauCeti.awayEmptyContinuousMulEquiv_apply {ι : Type u} {G : ι → Type v} [(i : ι) → Group (G i)] [(i : ι) → TopologicalSpace (G i)] (U : (i : ι) → Subgroup (G i)) (x : RestrictedProductGroupAway ∅ U) : (awayEmptyContinuousMulEquiv U) x = (awayEmptyEquiv U) x

The topological empty-away comparison has the canonical reindexing as underlying map.

@[simp]

theorem TauCeti.addAwayEmptyContinuousAddEquiv_apply {ι : Type u} {G : ι → Type v} [(i : ι) → AddGroup (G i)] [(i : ι) → TopologicalSpace (G i)] (U : (i : ι) → AddSubgroup (G i)) (x : RestrictedProductAddGroupAway ∅ U) : (addAwayEmptyContinuousAddEquiv U) x = (addAwayEmptyEquiv U) x

@[simp]

theorem TauCeti.awayEmptyContinuousMulEquiv_symm_apply {ι : Type u} {G : ι → Type v} [(i : ι) → Group (G i)] [(i : ι) → TopologicalSpace (G i)] (U : (i : ι) → Subgroup (G i)) (x : RestrictedProductGroup U) : (awayEmptyContinuousMulEquiv U).symm x = (restrictAway ∅ U) x

The inverse topological comparison is restriction away from the empty set.

@[simp]

theorem TauCeti.addAwayEmptyContinuousAddEquiv_symm_apply {ι : Type u} {G : ι → Type v} [(i : ι) → AddGroup (G i)] [(i : ι) → TopologicalSpace (G i)] (U : (i : ι) → AddSubgroup (G i)) (x : RestrictedProductAddGroup U) : (addAwayEmptyContinuousAddEquiv U).symm x = (addRestrictAway ∅ U) x

theorem TauCeti.restrictAway_restrictAway {ι : Type u} {G : ι → Type v} [(i : ι) → Group (G i)] {S T : Set ι} (hST : S ⊆ T) (U : (i : ι) → Subgroup (G i)) (x : RestrictedProductGroup U) (i : { i : ι // i ∉ T }) : ((restrictAway T U) x) i = ((restrictAway S U) x) ⟨↑i, ⋯⟩

Restricting away from a larger set factors through restricting away from a smaller one: the coordinate of restrictAway T U x at i ∉ T is the coordinate of restrictAway S U x at the same index, viewed outside S ⊆ T.

theorem TauCeti.addRestrictAway_addRestrictAway {ι : Type u} {G : ι → Type v} [(i : ι) → AddGroup (G i)] {S T : Set ι} (hST : S ⊆ T) (U : (i : ι) → AddSubgroup (G i)) (x : RestrictedProductAddGroup U) (i : { i : ι // i ∉ T }) : ((addRestrictAway T U) x) i = ((addRestrictAway S U) x) ⟨↑i, ⋯⟩

Restricting a restricted product of additive groups away from a larger set factors through restricting away from a smaller one: the coordinate of addRestrictAway T U x at i ∉ T is the coordinate of addRestrictAway S U x at the same index, viewed outside S ⊆ T.

theorem TauCeti.continuous_restrictAway {ι : Type u} {G : ι → Type v} [(i : ι) → Group (G i)] [(i : ι) → TopologicalSpace (G i)] (S : Set ι) (U : (i : ι) → Subgroup (G i)) : Continuous ⇑(restrictAway S U)

The restriction away from S is continuous for every reference family: it is a map out of a single restricted product whose coordinate maps are identities.

theorem TauCeti.continuous_addRestrictAway {ι : Type u} {G : ι → Type v} [(i : ι) → AddGroup (G i)] [(i : ι) → TopologicalSpace (G i)] (S : Set ι) (U : (i : ι) → AddSubgroup (G i)) : Continuous ⇑(addRestrictAway S U)

The restriction away from S of a restricted product of additive groups is continuous for every reference family: it is a map out of a single restricted product whose coordinate maps are identities.