Changing the reference family of a restricted product

Two families of reference subgroups that agree at all but finitely many indices define the same restricted product up to a coordinatewise-identity isomorphism, which is a homeomorphism for every pair of families. This file records that isomorphism, its coordinate formulas in both directions, its continuity, its coherence laws, its naturality with respect to componentwise maps, and its identification with the componentwise map induced by the identity homomorphisms. It is the case of restrictedProductCongrRight in which every coordinate equivalence is the identity.

The isomorphism identifies the ambient restricted products only; it need not carry the everywhere-integral subgroup of one family onto that of the other, because the coordinate condition can change at the finitely many indices where the families differ. Precisely, it carries the subgroup cut out by any family V to the subgroup cut out by V, so it preserves the everywhere-integral subgroups exactly when the two families agree at every index (map_integralSubgroup_restrictedProductCongr_eq_iff). The witness exists_map_integralSubgroup_ne records an explicit counterexample to the general preservation claim. The resulting transport of double-coset spaces is in TauCeti.Topology.Algebra.RestrictedProduct.Congr.DoubleCoset.

The general statements have additive counterparts, such as addRestrictedProductCongr.

References

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

def TauCeti.restrictedProductCongr {ι : Type u} {G : ι → Type v} [(i : ι) → Group (G i)] (U U' : (i : ι) → Subgroup (G i)) (h : ∀ᶠ (i : ι) in Filter.cofinite, U i = U' i) : RestrictedProduct (fun (i : ι) => G i) (fun (i : ι) => ↑(U i)) Filter.cofinite ≃* RestrictedProduct (fun (i : ι) => G i) (fun (i : ι) => ↑(U' i)) Filter.cofinite

The multiplicative equivalence between the restricted products with respect to two reference families that agree at all but finitely many indices. It is the identity in every coordinate.

def TauCeti.addRestrictedProductCongr {ι : Type u} {G : ι → Type v} [(i : ι) → AddGroup (G i)] (U U' : (i : ι) → AddSubgroup (G i)) (h : ∀ᶠ (i : ι) in Filter.cofinite, U i = U' i) : RestrictedProduct (fun (i : ι) => G i) (fun (i : ι) => ↑(U i)) Filter.cofinite ≃+ RestrictedProduct (fun (i : ι) => G i) (fun (i : ι) => ↑(U' i)) Filter.cofinite

The additive equivalence between the restricted products with respect to two reference families that agree at all but finitely many indices. It is the identity in every coordinate.

@[simp]

theorem TauCeti.restrictedProductCongr_apply {ι : Type u} {G : ι → Type v} [(i : ι) → Group (G i)] (U U' : (i : ι) → Subgroup (G i)) (h : ∀ᶠ (i : ι) in Filter.cofinite, U i = U' i) (x : RestrictedProduct (fun (i : ι) => G i) (fun (i : ι) => ↑(U i)) Filter.cofinite) (i : ι) : ((restrictedProductCongr U U' h) x) i = x i

The change-of-family equivalence is the identity in every coordinate.

@[simp]

theorem TauCeti.addRestrictedProductCongr_apply {ι : Type u} {G : ι → Type v} [(i : ι) → AddGroup (G i)] (U U' : (i : ι) → AddSubgroup (G i)) (h : ∀ᶠ (i : ι) in Filter.cofinite, U i = U' i) (x : RestrictedProduct (fun (i : ι) => G i) (fun (i : ι) => ↑(U i)) Filter.cofinite) (i : ι) : ((addRestrictedProductCongr U U' h) x) i = x i

theorem TauCeti.restrictedProductCongr_symm_apply {ι : Type u} {G : ι → Type v} [(i : ι) → Group (G i)] (U U' : (i : ι) → Subgroup (G i)) (h : ∀ᶠ (i : ι) in Filter.cofinite, U i = U' i) (y : RestrictedProduct (fun (i : ι) => G i) (fun (i : ι) => ↑(U' i)) Filter.cofinite) (i : ι) : ((restrictedProductCongr U U' h).symm y) i = y i

The inverse of the change-of-family equivalence is the identity in every coordinate.

Not a simp lemma: simp proves it from restrictedProductCongr_symm and restrictedProductCongr_apply.

theorem TauCeti.addRestrictedProductCongr_symm_apply {ι : Type u} {G : ι → Type v} [(i : ι) → AddGroup (G i)] (U U' : (i : ι) → AddSubgroup (G i)) (h : ∀ᶠ (i : ι) in Filter.cofinite, U i = U' i) (y : RestrictedProduct (fun (i : ι) => G i) (fun (i : ι) => ↑(U' i)) Filter.cofinite) (i : ι) : ((addRestrictedProductCongr U U' h).symm y) i = y i

theorem TauCeti.continuous_restrictedProductCongr {ι : Type u} {G : ι → Type v} [(i : ι) → Group (G i)] [(i : ι) → TopologicalSpace (G i)] (U U' : (i : ι) → Subgroup (G i)) (h : ∀ᶠ (i : ι) in Filter.cofinite, U i = U' i) : Continuous ⇑(restrictedProductCongr U U' h)

The change-of-family equivalence is continuous, for every pair of reference families.

theorem TauCeti.continuous_addRestrictedProductCongr {ι : Type u} {G : ι → Type v} [(i : ι) → AddGroup (G i)] [(i : ι) → TopologicalSpace (G i)] (U U' : (i : ι) → AddSubgroup (G i)) (h : ∀ᶠ (i : ι) in Filter.cofinite, U i = U' i) : Continuous ⇑(addRestrictedProductCongr U U' h)

theorem TauCeti.continuous_restrictedProductCongr_symm {ι : Type u} {G : ι → Type v} [(i : ι) → Group (G i)] [(i : ι) → TopologicalSpace (G i)] (U U' : (i : ι) → Subgroup (G i)) (h : ∀ᶠ (i : ι) in Filter.cofinite, U i = U' i) : Continuous ⇑(restrictedProductCongr U U' h).symm

The inverse of the change-of-family equivalence is continuous, for every pair of reference families.

theorem TauCeti.continuous_addRestrictedProductCongr_symm {ι : Type u} {G : ι → Type v} [(i : ι) → AddGroup (G i)] [(i : ι) → TopologicalSpace (G i)] (U U' : (i : ι) → AddSubgroup (G i)) (h : ∀ᶠ (i : ι) in Filter.cofinite, U i = U' i) : Continuous ⇑(addRestrictedProductCongr U U' h).symm

@[simp]

theorem TauCeti.restrictedProductCongr_refl {ι : Type u} {G : ι → Type v} [(i : ι) → Group (G i)] (U : (i : ι) → Subgroup (G i)) : restrictedProductCongr U U ⋯ = MulEquiv.refl (RestrictedProduct (fun (i : ι) => G i) (fun (i : ι) => ↑(U i)) Filter.cofinite)

The change-of-family equivalence from a family to itself is the identity.

@[simp]

theorem TauCeti.addRestrictedProductCongr_refl {ι : Type u} {G : ι → Type v} [(i : ι) → AddGroup (G i)] (U : (i : ι) → AddSubgroup (G i)) : addRestrictedProductCongr U U ⋯ = AddEquiv.refl (RestrictedProduct (fun (i : ι) => G i) (fun (i : ι) => ↑(U i)) Filter.cofinite)

@[simp]

theorem TauCeti.restrictedProductCongr_symm {ι : Type u} {G : ι → Type v} [(i : ι) → Group (G i)] (U U' : (i : ι) → Subgroup (G i)) (h : ∀ᶠ (i : ι) in Filter.cofinite, U i = U' i) : (restrictedProductCongr U U' h).symm = restrictedProductCongr U' U ⋯

The inverse of the change-of-family equivalence is the change-of-family equivalence in the opposite direction.

@[simp]

theorem TauCeti.addRestrictedProductCongr_symm {ι : Type u} {G : ι → Type v} [(i : ι) → AddGroup (G i)] (U U' : (i : ι) → AddSubgroup (G i)) (h : ∀ᶠ (i : ι) in Filter.cofinite, U i = U' i) : (addRestrictedProductCongr U U' h).symm = addRestrictedProductCongr U' U ⋯

@[simp]

theorem TauCeti.restrictedProductCongr_trans {ι : Type u} {G : ι → Type v} [(i : ι) → Group (G i)] (U U' U'' : (i : ι) → Subgroup (G i)) (h : ∀ᶠ (i : ι) in Filter.cofinite, U i = U' i) (h' : ∀ᶠ (i : ι) in Filter.cofinite, U' i = U'' i) : (restrictedProductCongr U U' h).trans (restrictedProductCongr U' U'' h') = restrictedProductCongr U U'' ⋯

Two successive changes of family compose to the change of family between the outer two families.

@[simp]

theorem TauCeti.addRestrictedProductCongr_trans {ι : Type u} {G : ι → Type v} [(i : ι) → AddGroup (G i)] (U U' U'' : (i : ι) → AddSubgroup (G i)) (h : ∀ᶠ (i : ι) in Filter.cofinite, U i = U' i) (h' : ∀ᶠ (i : ι) in Filter.cofinite, U' i = U'' i) : (addRestrictedProductCongr U U' h).trans (addRestrictedProductCongr U' U'' h') = addRestrictedProductCongr U U'' ⋯

theorem TauCeti.restrictedProductCongr_naturality {ι : Type u} {G : ι → Type v} [(i : ι) → Group (G i)] {H : ι → Type w} [(i : ι) → Group (H i)] (U U' : (i : ι) → Subgroup (G i)) (V V' : (i : ι) → Subgroup (H i)) (φ : (i : ι) → G i →* H i) (hφ : ∀ᶠ (i : ι) in Filter.cofinite, Set.MapsTo ⇑(φ i) ↑(U i) ↑(V i)) (h : ∀ᶠ (i : ι) in Filter.cofinite, U i = U' i) (h' : ∀ᶠ (i : ι) in Filter.cofinite, V i = V' i) : (↑(restrictedProductCongr V V' h')).comp (restrictedProductMap U V φ hφ) = (restrictedProductMap U' V' φ ⋯).comp ↑(restrictedProductCongr U U' h)

Naturality of the change-of-family equivalence with respect to componentwise maps: changing the family before or after applying a componentwise map gives the same homomorphism.

theorem TauCeti.addRestrictedProductCongr_naturality {ι : Type u} {G : ι → Type v} [(i : ι) → AddGroup (G i)] {H : ι → Type w} [(i : ι) → AddGroup (H i)] (U U' : (i : ι) → AddSubgroup (G i)) (V V' : (i : ι) → AddSubgroup (H i)) (φ : (i : ι) → G i →+ H i) (hφ : ∀ᶠ (i : ι) in Filter.cofinite, Set.MapsTo ⇑(φ i) ↑(U i) ↑(V i)) (h : ∀ᶠ (i : ι) in Filter.cofinite, U i = U' i) (h' : ∀ᶠ (i : ι) in Filter.cofinite, V i = V' i) : (↑(addRestrictedProductCongr V V' h')).comp (addRestrictedProductMap U V φ hφ) = (addRestrictedProductMap U' V' φ ⋯).comp ↑(addRestrictedProductCongr U U' h)

theorem TauCeti.coe_monoidHom_restrictedProductCongr {ι : Type u} {G : ι → Type v} [(i : ι) → Group (G i)] (U U' : (i : ι) → Subgroup (G i)) (h : ∀ᶠ (i : ι) in Filter.cofinite, U i = U' i) : ↑(restrictedProductCongr U U' h) = restrictedProductMap U U' (fun (x : ι) => MonoidHom.id (G x)) ⋯

As a monoid homomorphism, the change-of-family equivalence is the componentwise map induced by the identity homomorphisms.

theorem TauCeti.coe_addMonoidHom_addRestrictedProductCongr {ι : Type u} {G : ι → Type v} [(i : ι) → AddGroup (G i)] (U U' : (i : ι) → AddSubgroup (G i)) (h : ∀ᶠ (i : ι) in Filter.cofinite, U i = U' i) : ↑(addRestrictedProductCongr U U' h) = addRestrictedProductMap U U' (fun (x : ι) => AddMonoidHom.id (G x)) ⋯

@[simp]

theorem TauCeti.map_integralSubgroupOf_restrictedProductCongr {ι : Type u} {G : ι → Type v} [(i : ι) → Group (G i)] (U U' V : (i : ι) → Subgroup (G i)) (h : ∀ᶠ (i : ι) in Filter.cofinite, U i = U' i) : Subgroup.map (↑(restrictedProductCongr U U' h)) (integralSubgroupOf U V) = integralSubgroupOf U' V

The change-of-family equivalence carries the subgroup cut out by a family V in the first restricted product to the subgroup cut out by the same family in the second.

@[simp]

theorem TauCeti.map_integralAddSubgroupOf_addRestrictedProductCongr {ι : Type u} {G : ι → Type v} [(i : ι) → AddGroup (G i)] (U U' V : (i : ι) → AddSubgroup (G i)) (h : ∀ᶠ (i : ι) in Filter.cofinite, U i = U' i) : AddSubgroup.map (↑(addRestrictedProductCongr U U' h)) (integralAddSubgroupOf U V) = integralAddSubgroupOf U' V

@[simp]

theorem TauCeti.map_integralSubgroup_restrictedProductCongr {ι : Type u} {G : ι → Type v} [(i : ι) → Group (G i)] (U U' : (i : ι) → Subgroup (G i)) (h : ∀ᶠ (i : ι) in Filter.cofinite, U i = U' i) : Subgroup.map (↑(restrictedProductCongr U U' h)) (integralSubgroup U) = integralSubgroupOf U' U

The change-of-family equivalence carries the everywhere-integral subgroup of U to the subgroup of the U'-restricted product cut out by U.

@[simp]

theorem TauCeti.map_integralAddSubgroup_addRestrictedProductCongr {ι : Type u} {G : ι → Type v} [(i : ι) → AddGroup (G i)] (U U' : (i : ι) → AddSubgroup (G i)) (h : ∀ᶠ (i : ι) in Filter.cofinite, U i = U' i) : AddSubgroup.map (↑(addRestrictedProductCongr U U' h)) (integralAddSubgroup U) = integralAddSubgroupOf U' U

theorem TauCeti.map_integralSubgroup_restrictedProductCongr_eq_iff {ι : Type u} {G : ι → Type v} [(i : ι) → Group (G i)] (U U' : (i : ι) → Subgroup (G i)) (h : ∀ᶠ (i : ι) in Filter.cofinite, U i = U' i) : Subgroup.map (↑(restrictedProductCongr U U' h)) (integralSubgroup U) = integralSubgroup U' ↔ U = U'

The change-of-family equivalence carries the everywhere-integral subgroup of U onto that of U' exactly when the two reference families agree at every index. Agreement at all but finitely many indices identifies the ambient restricted products, but not their integral subgroups.

theorem TauCeti.map_integralAddSubgroup_addRestrictedProductCongr_eq_iff {ι : Type u} {G : ι → Type v} [(i : ι) → AddGroup (G i)] (U U' : (i : ι) → AddSubgroup (G i)) (h : ∀ᶠ (i : ι) in Filter.cofinite, U i = U' i) : AddSubgroup.map (↑(addRestrictedProductCongr U U' h)) (integralAddSubgroup U) = integralAddSubgroup U' ↔ U = U'

theorem TauCeti.exists_map_integralSubgroup_ne : ∃ (U : ℕ → Subgroup (Multiplicative ℤ)) (U' : ℕ → Subgroup (Multiplicative ℤ)) (h : ∀ᶠ (i : ℕ) in Filter.cofinite, U i = U' i), Subgroup.map (↑(restrictedProductCongr U U' h)) (integralSubgroup U) ≠ integralSubgroup U'

The change-of-family equivalence need not carry the everywhere-integral subgroup onto the everywhere-integral subgroup of the new family. The witness is that of exists_not_map_integralSubgroup_le: copies of Multiplicative ℤ indexed by ℕ, with the first family everywhere ⊤ and the second family equal to ⊥ at zero and ⊤ elsewhere.