Componentwise maps of restricted products

A family of coordinate homomorphisms induces a homomorphism of restricted products when it preserves the reference subgroups at all but finitely many indices. This file records that map, its continuity and functoriality, the criterion for it to be surjective, and the stronger everywhere-preserving specialization that maps the everywhere-integral subgroup into the everywhere-integral subgroup.

The distinction between eventual and everywhere preservation is essential: the final theorems give an explicit family for which the eventual map does not preserve the integral subgroup. The construction is the fixed-index specialization of Mathlib's RestrictedProduct.mapAlongMonoidHom.

The general statements have additive counterparts, such as addRestrictedProductMap.

References

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

def TauCeti.restrictedProductMap {ι : Type u} {G : ι → Type v} [(i : ι) → Group (G i)] {H : ι → Type w} [(i : ι) → Group (H i)] (U : (i : ι) → Subgroup (G i)) (U' : (i : ι) → Subgroup (H i)) (φ : (i : ι) → G i →* H i) (hφ : ∀ᶠ (i : ι) in Filter.cofinite, Set.MapsTo ⇑(φ i) ↑(U i) ↑(U' i)) : RestrictedProduct (fun (i : ι) => G i) (fun (i : ι) => ↑(U i)) Filter.cofinite →* RestrictedProduct (fun (i : ι) => H i) (fun (i : ι) => ↑(U' i)) Filter.cofinite

The componentwise homomorphism of restricted products induced by a family that eventually maps each reference subgroup into the corresponding target subgroup.

def TauCeti.addRestrictedProductMap {ι : Type u} {G : ι → Type v} [(i : ι) → AddGroup (G i)] {H : ι → Type w} [(i : ι) → AddGroup (H i)] (U : (i : ι) → AddSubgroup (G i)) (U' : (i : ι) → AddSubgroup (H i)) (φ : (i : ι) → G i →+ H i) (hφ : ∀ᶠ (i : ι) in Filter.cofinite, Set.MapsTo ⇑(φ i) ↑(U i) ↑(U' i)) : RestrictedProduct (fun (i : ι) => G i) (fun (i : ι) => ↑(U i)) Filter.cofinite →+ RestrictedProduct (fun (i : ι) => H i) (fun (i : ι) => ↑(U' i)) Filter.cofinite

The componentwise additive homomorphism of restricted products induced by a family that eventually maps each reference subgroup into the corresponding target subgroup.

@[simp]

theorem TauCeti.restrictedProductMap_apply {ι : Type u} {G : ι → Type v} [(i : ι) → Group (G i)] {H : ι → Type w} [(i : ι) → Group (H i)] (U : (i : ι) → Subgroup (G i)) (U' : (i : ι) → Subgroup (H i)) (φ : (i : ι) → G i →* H i) (hφ : ∀ᶠ (i : ι) in Filter.cofinite, Set.MapsTo ⇑(φ i) ↑(U i) ↑(U' i)) (x : RestrictedProduct (fun (i : ι) => G i) (fun (i : ι) => ↑(U i)) Filter.cofinite) (i : ι) : ((restrictedProductMap U U' φ hφ) x) i = (φ i) (x i)

Evaluation of a componentwise restricted-product homomorphism at a coordinate.

@[simp]

theorem TauCeti.addRestrictedProductMap_apply {ι : Type u} {G : ι → Type v} [(i : ι) → AddGroup (G i)] {H : ι → Type w} [(i : ι) → AddGroup (H i)] (U : (i : ι) → AddSubgroup (G i)) (U' : (i : ι) → AddSubgroup (H i)) (φ : (i : ι) → G i →+ H i) (hφ : ∀ᶠ (i : ι) in Filter.cofinite, Set.MapsTo ⇑(φ i) ↑(U i) ↑(U' i)) (x : RestrictedProduct (fun (i : ι) => G i) (fun (i : ι) => ↑(U i)) Filter.cofinite) (i : ι) : ((addRestrictedProductMap U U' φ hφ) x) i = (φ i) (x i)

theorem TauCeti.continuous_restrictedProductMap {ι : Type u} {G : ι → Type v} [(i : ι) → Group (G i)] {H : ι → Type w} [(i : ι) → Group (H i)] [(i : ι) → TopologicalSpace (G i)] [(i : ι) → TopologicalSpace (H i)] (U : (i : ι) → Subgroup (G i)) (U' : (i : ι) → Subgroup (H i)) (φ : (i : ι) → G i →* H i) (hφ : ∀ᶠ (i : ι) in Filter.cofinite, Set.MapsTo ⇑(φ i) ↑(U i) ↑(U' i)) (hφcont : ∀ (i : ι), Continuous ⇑(φ i)) : Continuous ⇑(restrictedProductMap U U' φ hφ)

A componentwise restricted-product homomorphism is continuous when all its coordinate maps are continuous.

theorem TauCeti.continuous_addRestrictedProductMap {ι : Type u} {G : ι → Type v} [(i : ι) → AddGroup (G i)] {H : ι → Type w} [(i : ι) → AddGroup (H i)] [(i : ι) → TopologicalSpace (G i)] [(i : ι) → TopologicalSpace (H i)] (U : (i : ι) → AddSubgroup (G i)) (U' : (i : ι) → AddSubgroup (H i)) (φ : (i : ι) → G i →+ H i) (hφ : ∀ᶠ (i : ι) in Filter.cofinite, Set.MapsTo ⇑(φ i) ↑(U i) ↑(U' i)) (hφcont : ∀ (i : ι), Continuous ⇑(φ i)) : Continuous ⇑(addRestrictedProductMap U U' φ hφ)

def TauCeti.restrictedProductMapOfForall {ι : Type u} {G : ι → Type v} [(i : ι) → Group (G i)] {H : ι → Type w} [(i : ι) → Group (H i)] (U : (i : ι) → Subgroup (G i)) (U' : (i : ι) → Subgroup (H i)) (φ : (i : ι) → G i →* H i) (hφ : ∀ (i : ι), Set.MapsTo ⇑(φ i) ↑(U i) ↑(U' i)) : RestrictedProduct (fun (i : ι) => G i) (fun (i : ι) => ↑(U i)) Filter.cofinite →* RestrictedProduct (fun (i : ι) => H i) (fun (i : ι) => ↑(U' i)) Filter.cofinite

The componentwise restricted-product homomorphism when every coordinate map preserves the reference subgroup.

def TauCeti.addRestrictedProductMapOfForall {ι : Type u} {G : ι → Type v} [(i : ι) → AddGroup (G i)] {H : ι → Type w} [(i : ι) → AddGroup (H i)] (U : (i : ι) → AddSubgroup (G i)) (U' : (i : ι) → AddSubgroup (H i)) (φ : (i : ι) → G i →+ H i) (hφ : ∀ (i : ι), Set.MapsTo ⇑(φ i) ↑(U i) ↑(U' i)) : RestrictedProduct (fun (i : ι) => G i) (fun (i : ι) => ↑(U i)) Filter.cofinite →+ RestrictedProduct (fun (i : ι) => H i) (fun (i : ι) => ↑(U' i)) Filter.cofinite

The componentwise additive homomorphism of restricted products when every coordinate map preserves the reference subgroup.

@[simp]

theorem TauCeti.restrictedProductMapOfForall_apply {ι : Type u} {G : ι → Type v} [(i : ι) → Group (G i)] {H : ι → Type w} [(i : ι) → Group (H i)] (U : (i : ι) → Subgroup (G i)) (U' : (i : ι) → Subgroup (H i)) (φ : (i : ι) → G i →* H i) (hφ : ∀ (i : ι), Set.MapsTo ⇑(φ i) ↑(U i) ↑(U' i)) (x : RestrictedProduct (fun (i : ι) => G i) (fun (i : ι) => ↑(U i)) Filter.cofinite) (i : ι) : ((restrictedProductMapOfForall U U' φ hφ) x) i = (φ i) (x i)

Evaluation of the everywhere-preserving componentwise homomorphism at a coordinate.

@[simp]

theorem TauCeti.addRestrictedProductMapOfForall_apply {ι : Type u} {G : ι → Type v} [(i : ι) → AddGroup (G i)] {H : ι → Type w} [(i : ι) → AddGroup (H i)] (U : (i : ι) → AddSubgroup (G i)) (U' : (i : ι) → AddSubgroup (H i)) (φ : (i : ι) → G i →+ H i) (hφ : ∀ (i : ι), Set.MapsTo ⇑(φ i) ↑(U i) ↑(U' i)) (x : RestrictedProduct (fun (i : ι) => G i) (fun (i : ι) => ↑(U i)) Filter.cofinite) (i : ι) : ((addRestrictedProductMapOfForall U U' φ hφ) x) i = (φ i) (x i)

theorem TauCeti.continuous_restrictedProductMapOfForall {ι : Type u} {G : ι → Type v} [(i : ι) → Group (G i)] {H : ι → Type w} [(i : ι) → Group (H i)] [(i : ι) → TopologicalSpace (G i)] [(i : ι) → TopologicalSpace (H i)] (U : (i : ι) → Subgroup (G i)) (U' : (i : ι) → Subgroup (H i)) (φ : (i : ι) → G i →* H i) (hφ : ∀ (i : ι), Set.MapsTo ⇑(φ i) ↑(U i) ↑(U' i)) (hφcont : ∀ (i : ι), Continuous ⇑(φ i)) : Continuous ⇑(restrictedProductMapOfForall U U' φ hφ)

An everywhere-preserving componentwise restricted-product homomorphism is continuous when all its coordinate maps are continuous.

theorem TauCeti.continuous_addRestrictedProductMapOfForall {ι : Type u} {G : ι → Type v} [(i : ι) → AddGroup (G i)] {H : ι → Type w} [(i : ι) → AddGroup (H i)] [(i : ι) → TopologicalSpace (G i)] [(i : ι) → TopologicalSpace (H i)] (U : (i : ι) → AddSubgroup (G i)) (U' : (i : ι) → AddSubgroup (H i)) (φ : (i : ι) → G i →+ H i) (hφ : ∀ (i : ι), Set.MapsTo ⇑(φ i) ↑(U i) ↑(U' i)) (hφcont : ∀ (i : ι), Continuous ⇑(φ i)) : Continuous ⇑(addRestrictedProductMapOfForall U U' φ hφ)

@[simp]

theorem TauCeti.restrictedProductMap_id {ι : Type u} {G : ι → Type v} [(i : ι) → Group (G i)] (U : (i : ι) → Subgroup (G i)) : restrictedProductMap U U (fun (i : ι) => MonoidHom.id (G i)) ⋯ = MonoidHom.id (RestrictedProduct (fun (i : ι) => G i) (fun (i : ι) => ↑(U i)) Filter.cofinite)

The componentwise restricted-product homomorphism induced by identity maps is the identity.

@[simp]

theorem TauCeti.addRestrictedProductMap_id {ι : Type u} {G : ι → Type v} [(i : ι) → AddGroup (G i)] (U : (i : ι) → AddSubgroup (G i)) : addRestrictedProductMap U U (fun (i : ι) => AddMonoidHom.id (G i)) ⋯ = AddMonoidHom.id (RestrictedProduct (fun (i : ι) => G i) (fun (i : ι) => ↑(U i)) Filter.cofinite)

@[simp]

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

Componentwise restricted-product homomorphisms compose coordinatewise.

@[simp]

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

@[simp]

theorem TauCeti.restrictedProductMap_surjective_iff {ι : Type u} {G : ι → Type v} [(i : ι) → Group (G i)] {H : ι → Type w} [(i : ι) → Group (H i)] (U : (i : ι) → Subgroup (G i)) (U' : (i : ι) → Subgroup (H i)) (φ : (i : ι) → G i →* H i) (hφ : ∀ᶠ (i : ι) in Filter.cofinite, Set.MapsTo ⇑(φ i) ↑(U i) ↑(U' i)) : Function.Surjective ⇑(restrictedProductMap U U' φ hφ) ↔ (∀ (i : ι), Function.Surjective ⇑(φ i)) ∧ ∀ᶠ (i : ι) in Filter.cofinite, Set.SurjOn ⇑(φ i) ↑(U i) ↑(U' i)

A componentwise restricted-product homomorphism is surjective exactly when every coordinate map is surjective and, at all but finitely many indices, the coordinate map carries the source reference subgroup onto the target one. Surjectivity of each coordinate map alone is not enough: an element of the target may lie in the target reference subgroups at infinitely many indices where no preimage lies in the source reference subgroup.

@[simp]

theorem TauCeti.addRestrictedProductMap_surjective_iff {ι : Type u} {G : ι → Type v} [(i : ι) → AddGroup (G i)] {H : ι → Type w} [(i : ι) → AddGroup (H i)] (U : (i : ι) → AddSubgroup (G i)) (U' : (i : ι) → AddSubgroup (H i)) (φ : (i : ι) → G i →+ H i) (hφ : ∀ᶠ (i : ι) in Filter.cofinite, Set.MapsTo ⇑(φ i) ↑(U i) ↑(U' i)) : Function.Surjective ⇑(addRestrictedProductMap U U' φ hφ) ↔ (∀ (i : ι), Function.Surjective ⇑(φ i)) ∧ ∀ᶠ (i : ι) in Filter.cofinite, Set.SurjOn ⇑(φ i) ↑(U i) ↑(U' i)

theorem TauCeti.mapsTo_integralSubgroup_of_forall {ι : Type u} {G : ι → Type v} [(i : ι) → Group (G i)] {H : ι → Type w} [(i : ι) → Group (H i)] (U : (i : ι) → Subgroup (G i)) (U' : (i : ι) → Subgroup (H i)) (φ : (i : ι) → G i →* H i) (hφ : ∀ (i : ι), Set.MapsTo ⇑(φ i) ↑(U i) ↑(U' i)) : Subgroup.map (restrictedProductMapOfForall U U' φ hφ) (integralSubgroup U) ≤ integralSubgroup U'

An everywhere-preserving componentwise map sends the integral subgroup into the target integral subgroup.

theorem TauCeti.mapsTo_integralAddSubgroup_of_forall {ι : Type u} {G : ι → Type v} [(i : ι) → AddGroup (G i)] {H : ι → Type w} [(i : ι) → AddGroup (H i)] (U : (i : ι) → AddSubgroup (G i)) (U' : (i : ι) → AddSubgroup (H i)) (φ : (i : ι) → G i →+ H i) (hφ : ∀ (i : ι), Set.MapsTo ⇑(φ i) ↑(U i) ↑(U' i)) : AddSubgroup.map (addRestrictedProductMapOfForall U U' φ hφ) (integralAddSubgroup U) ≤ integralAddSubgroup U'

theorem TauCeti.exists_not_map_integralSubgroup_le : ∃ (U : ℕ → Subgroup (Multiplicative ℤ)) (U' : ℕ → Subgroup (Multiplicative ℤ)) (h : ∀ᶠ (i : ℕ) in Filter.cofinite, U i = U' i), ¬Subgroup.map (restrictedProductMap U U' (fun (x : ℕ) => MonoidHom.id (Multiplicative ℤ)) ⋯) (integralSubgroup U) ≤ integralSubgroup U'

Eventual preservation of reference subgroups does not imply preservation of the integral subgroups: an explicit pair of reference families, agreeing at all but one index, for which the identity componentwise map does not send the integral subgroup into the target integral subgroup. The witness uses copies of Multiplicative ℤ indexed by ℕ, with the source reference family everywhere ⊤ and the target reference family equal to ⊥ at zero and ⊤ elsewhere.

theorem TauCeti.not_forall_mapsTo_integralSubgroup : ¬∀ (U U' : ℕ → Subgroup (Multiplicative ℤ)) (φ : ℕ → Multiplicative ℤ →* Multiplicative ℤ) (hφ : ∀ᶠ (i : ℕ) in Filter.cofinite, Set.MapsTo ⇑(φ i) ↑(U i) ↑(U' i)), Subgroup.map (restrictedProductMap U U' φ hφ) (integralSubgroup U) ≤ integralSubgroup U'

Eventual preservation of reference subgroups does not imply preservation of the integral subgroups; this is the universally quantified form of exists_not_map_integralSubgroup_le.