Integral subgroups of restricted products

This file packages the everywhere-integral part of a restricted product of groups equipped with topologies. The reference family used to form the restricted product and a second family of subgroups are kept separate, so changing the integral model at finitely many indices is represented without changing the ambient restricted product. The resulting openness and compactness statements are the point-set input for maps and decompositions of restricted products.

It also names the restricted product of a family of groups relative to a family of reference subgroups, and its product with a distinguished factor carrying no integrality condition. These are the shapes in which restricted products appear when a family of local groups is assembled into an adelic one: the finite adelic points, and the full adelic points with the archimedean factor set apart.

Every construction and theorem here is also stated for additive groups (integralAddSubgroup, RestrictedProductAddGroup, CompactOpenAddSubgroups, …).

The eventual comparison results are adapted from the FLT project (ImperialCollegeLondon/FLT, file TopologicalSpace.lean, source commit bc2fe8ff7396469a16c2a6d51d6117f5825d93a0, FLT PR #1088, Apache 2.0), whose source file credits Matthew Jasper, Kevin Buzzard, Bhavik Mehta, Ruben Van de Velde, Bryan Wang Peng Jun, and Pietro Monticone.

References

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

@[simp]

theorem RestrictedProduct.coeMonoidHom_apply {ι : Type u_1} {R : ι → Type u_2} {S : ι → Type u_3} [(i : ι) → SetLike (S i) (R i)] {B : (i : ι) → S i} {𝓕 : Filter ι} [(i : ι) → Monoid (R i)] [∀ (i : ι), SubmonoidClass (S i) (R i)] (x : RestrictedProduct (fun (i : ι) => R i) (fun (i : ι) => ↑(B i)) 𝓕) : coeMonoidHom x = ⇑x

The coercion homomorphism from a restricted product to the full product acts as the coercion.

@[simp]

theorem RestrictedProduct.coeAddMonoidHom_apply {ι : Type u_1} {R : ι → Type u_2} {S : ι → Type u_3} [(i : ι) → SetLike (S i) (R i)] {B : (i : ι) → S i} {𝓕 : Filter ι} [(i : ι) → AddMonoid (R i)] [∀ (i : ι), AddSubmonoidClass (S i) (R i)] (x : RestrictedProduct (fun (i : ι) => R i) (fun (i : ι) => ↑(B i)) 𝓕) : coeAddMonoidHom x = ⇑x

@[reducible, inline]

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

The restricted product of the family G relative to the reference subgroups U: the elements of Π i, G i whose coordinates lie in U i for all but finitely many i.

@[reducible, inline]

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

The restricted product of the family of additive groups G relative to the reference subgroups U: the elements of Π i, G i whose coordinates lie in U i for all but finitely many i.

@[reducible, inline]

abbrev TauCeti.RestrictedProductGroupWithFactor {ι : Type u} {G : ι → Type v} [(i : ι) → Group (G i)] (H : Type w) (U : (i : ι) → Subgroup (G i)) : Type (max w v u)

A restricted product together with a distinguished factor H carrying no integrality condition.

@[reducible, inline]

abbrev TauCeti.RestrictedProductAddGroupWithFactor {ι : Type u} {G : ι → Type v} [(i : ι) → AddGroup (G i)] (H : Type w) (U : (i : ι) → AddSubgroup (G i)) : Type (max w v u)

A restricted product of additive groups together with a distinguished factor H carrying no integrality condition.

def TauCeti.integralSubgroupOf {ι : Type u} {G : ι → Type v} [(i : ι) → Group (G i)] (U V : (i : ι) → Subgroup (G i)) : Subgroup (RestrictedProduct (fun (i : ι) => G i) (fun (i : ι) => ↑(U i)) Filter.cofinite)

The subgroup of a restricted product cut out by a second family of subgroups.

def TauCeti.integralAddSubgroupOf {ι : Type u} {G : ι → Type v} [(i : ι) → AddGroup (G i)] (U V : (i : ι) → AddSubgroup (G i)) : AddSubgroup (RestrictedProduct (fun (i : ι) => G i) (fun (i : ι) => ↑(U i)) Filter.cofinite)

The additive subgroup of a restricted product cut out by a second family of additive subgroups.

@[simp]

theorem TauCeti.mem_integralSubgroupOf {ι : Type u} {G : ι → Type v} [(i : ι) → Group (G i)] (U V : (i : ι) → Subgroup (G i)) (x : RestrictedProduct (fun (i : ι) => G i) (fun (i : ι) => ↑(U i)) Filter.cofinite) : x ∈ integralSubgroupOf U V ↔ ∀ (i : ι), x i ∈ V i

Membership means that every coordinate belongs to the corresponding subgroup V i.

@[simp]

theorem TauCeti.mem_integralAddSubgroupOf {ι : Type u} {G : ι → Type v} [(i : ι) → AddGroup (G i)] (U V : (i : ι) → AddSubgroup (G i)) (x : RestrictedProduct (fun (i : ι) => G i) (fun (i : ι) => ↑(U i)) Filter.cofinite) : x ∈ integralAddSubgroupOf U V ↔ ∀ (i : ι), x i ∈ V i

def TauCeti.integralSubgroup {ι : Type u} {G : ι → Type v} [(i : ι) → Group (G i)] (U : (i : ι) → Subgroup (G i)) : Subgroup (RestrictedProduct (fun (i : ι) => G i) (fun (i : ι) => ↑(U i)) Filter.cofinite)

The subgroup whose coordinates lie in the reference subgroup at every index.

def TauCeti.integralAddSubgroup {ι : Type u} {G : ι → Type v} [(i : ι) → AddGroup (G i)] (U : (i : ι) → AddSubgroup (G i)) : AddSubgroup (RestrictedProduct (fun (i : ι) => G i) (fun (i : ι) => ↑(U i)) Filter.cofinite)

The additive subgroup whose coordinates lie in the reference subgroup at every index.

@[simp]

theorem TauCeti.mem_integralSubgroup {ι : Type u} {G : ι → Type v} [(i : ι) → Group (G i)] (U : (i : ι) → Subgroup (G i)) (x : RestrictedProduct (fun (i : ι) => G i) (fun (i : ι) => ↑(U i)) Filter.cofinite) : x ∈ integralSubgroup U ↔ ∀ (i : ι), x i ∈ U i

Membership means that every coordinate belongs to the reference subgroup U i.

@[simp]

theorem TauCeti.mem_integralAddSubgroup {ι : Type u} {G : ι → Type v} [(i : ι) → AddGroup (G i)] (U : (i : ι) → AddSubgroup (G i)) (x : RestrictedProduct (fun (i : ι) => G i) (fun (i : ι) => ↑(U i)) Filter.cofinite) : x ∈ integralAddSubgroup U ↔ ∀ (i : ι), x i ∈ U i

theorem TauCeti.integralSubgroupOf_self {ι : Type u} {G : ι → Type v} [(i : ι) → Group (G i)] (U : (i : ι) → Subgroup (G i)) : integralSubgroupOf U U = integralSubgroup U

Cutting the reference family out by itself gives the everywhere-integral subgroup. This is the definition of integralSubgroup; it is not a simp lemma, since simp [integralSubgroup] would then loop.

theorem TauCeti.integralAddSubgroupOf_self {ι : Type u} {G : ι → Type v} [(i : ι) → AddGroup (G i)] (U : (i : ι) → AddSubgroup (G i)) : integralAddSubgroupOf U U = integralAddSubgroup U

theorem TauCeti.integralSubgroupOf_le_integralSubgroupOf_iff {ι : Type u} {G : ι → Type v} [(i : ι) → Group (G i)] (U V V' : (i : ι) → Subgroup (G i)) : integralSubgroupOf U V ≤ integralSubgroupOf U V' ↔ ∀ (i : ι), V i ≤ V' i

Inside a fixed restricted product, the subgroup cut out by a family V is contained in the one cut out by V' exactly when V i ≤ V' i at every index: the single-coordinate elements detect every V i.

theorem TauCeti.integralAddSubgroupOf_le_integralAddSubgroupOf_iff {ι : Type u} {G : ι → Type v} [(i : ι) → AddGroup (G i)] (U V V' : (i : ι) → AddSubgroup (G i)) : integralAddSubgroupOf U V ≤ integralAddSubgroupOf U V' ↔ ∀ (i : ι), V i ≤ V' i

theorem TauCeti.integralSubgroupOf_le_integralSubgroup_iff {ι : Type u} {G : ι → Type v} [(i : ι) → Group (G i)] (U V : (i : ι) → Subgroup (G i)) : integralSubgroupOf U V ≤ integralSubgroup U ↔ ∀ (i : ι), V i ≤ U i

The subgroup cut out by a family V lies in the everywhere-integral subgroup exactly when V i ≤ U i at every index.

theorem TauCeti.integralAddSubgroupOf_le_integralAddSubgroup_iff {ι : Type u} {G : ι → Type v} [(i : ι) → AddGroup (G i)] (U V : (i : ι) → AddSubgroup (G i)) : integralAddSubgroupOf U V ≤ integralAddSubgroup U ↔ ∀ (i : ι), V i ≤ U i

theorem TauCeti.isOpen_integralSubgroupOf_of_eventually_le {ι : Type u} {G : ι → Type v} [(i : ι) → Group (G i)] [(i : ι) → TopologicalSpace (G i)] (U V : (i : ι) → Subgroup (G i)) (hV : ∀ (i : ι), IsOpen ↑(V i)) (hUV : ∀ᶠ (i : ι) in Filter.cofinite, U i ≤ V i) : IsOpen ↑(integralSubgroupOf U V)

Openness when every V i is open and the reference subgroup U i lies in V i at all but finitely many indices.

theorem TauCeti.isOpen_integralAddSubgroupOf_of_eventually_le {ι : Type u} {G : ι → Type v} [(i : ι) → AddGroup (G i)] [(i : ι) → TopologicalSpace (G i)] (U V : (i : ι) → AddSubgroup (G i)) (hV : ∀ (i : ι), IsOpen ↑(V i)) (hUV : ∀ᶠ (i : ι) in Filter.cofinite, U i ≤ V i) : IsOpen ↑(integralAddSubgroupOf U V)

theorem TauCeti.isCompact_integralSubgroupOf_of_eventually_le {ι : Type u} {G : ι → Type v} [(i : ι) → Group (G i)] [(i : ι) → TopologicalSpace (G i)] (U V : (i : ι) → Subgroup (G i)) (hV : ∀ (i : ι), IsCompact ↑(V i)) (hVU : ∀ᶠ (i : ι) in Filter.cofinite, V i ≤ U i) : IsCompact ↑(integralSubgroupOf U V)

Compactness when every V i is compact and lies in the reference subgroup U i at all but finitely many indices.

theorem TauCeti.isCompact_integralAddSubgroupOf_of_eventually_le {ι : Type u} {G : ι → Type v} [(i : ι) → AddGroup (G i)] [(i : ι) → TopologicalSpace (G i)] (U V : (i : ι) → AddSubgroup (G i)) (hV : ∀ (i : ι), IsCompact ↑(V i)) (hVU : ∀ᶠ (i : ι) in Filter.cofinite, V i ≤ U i) : IsCompact ↑(integralAddSubgroupOf U V)

theorem TauCeti.isOpen_integralSubgroup {ι : Type u} {G : ι → Type v} [(i : ι) → Group (G i)] [(i : ι) → TopologicalSpace (G i)] (U : (i : ι) → Subgroup (G i)) (hU : ∀ (i : ι), IsOpen ↑(U i)) : IsOpen ↑(integralSubgroup U)

Openness of the everywhere-integral subgroup from coordinatewise openness.

theorem TauCeti.isOpen_integralAddSubgroup {ι : Type u} {G : ι → Type v} [(i : ι) → AddGroup (G i)] [(i : ι) → TopologicalSpace (G i)] (U : (i : ι) → AddSubgroup (G i)) (hU : ∀ (i : ι), IsOpen ↑(U i)) : IsOpen ↑(integralAddSubgroup U)

theorem TauCeti.isCompact_integralSubgroup {ι : Type u} {G : ι → Type v} [(i : ι) → Group (G i)] [(i : ι) → TopologicalSpace (G i)] (U : (i : ι) → Subgroup (G i)) (hK : ∀ (i : ι), IsCompact ↑(U i)) : IsCompact ↑(integralSubgroup U)

Compactness of the everywhere-integral subgroup needs only coordinatewise compactness.

theorem TauCeti.isCompact_integralAddSubgroup {ι : Type u} {G : ι → Type v} [(i : ι) → AddGroup (G i)] [(i : ι) → TopologicalSpace (G i)] (U : (i : ι) → AddSubgroup (G i)) (hK : ∀ (i : ι), IsCompact ↑(U i)) : IsCompact ↑(integralAddSubgroup U)

structure TauCeti.CompactOpenAddSubgroups {ι : Type u} (G : ι → Type v) [(i : ι) → AddGroup (G i)] [(i : ι) → TopologicalSpace (G i)] : Type (max u v)

A family of compact open additive subgroups, one in each factor.

• addSubgroup (i : ι) : OpenAddSubgroup (G i)

  The compact open additive subgroup chosen in each factor.

• isCompact_addSubgroup (i : ι) : IsCompact ↑(self.addSubgroup i)

  Compactness of the chosen additive subgroup in each factor.

structure TauCeti.CompactOpenSubgroups {ι : Type u} (G : ι → Type v) [(i : ι) → Group (G i)] [(i : ι) → TopologicalSpace (G i)] : Type (max u v)

A family of compact open subgroups, one in each factor.

• subgroup (i : ι) : OpenSubgroup (G i)

  The compact open subgroup chosen in each factor.

• isCompact_subgroup (i : ι) : IsCompact ↑(self.subgroup i)

  Compactness of the chosen subgroup in each factor.

theorem TauCeti.CompactOpenSubgroups.ext {ι : Type u} {G : ι → Type v} [(i : ι) → Group (G i)] [(i : ι) → TopologicalSpace (G i)] {K L : CompactOpenSubgroups G} (h : K.subgroup = L.subgroup) : K = L

theorem TauCeti.CompactOpenAddSubgroups.ext {ι : Type u} {G : ι → Type v} [(i : ι) → AddGroup (G i)] [(i : ι) → TopologicalSpace (G i)] {K L : CompactOpenAddSubgroups G} (h : K.addSubgroup = L.addSubgroup) : K = L

theorem TauCeti.CompactOpenAddSubgroups.ext_iff {ι : Type u} {G : ι → Type v} [(i : ι) → AddGroup (G i)] [(i : ι) → TopologicalSpace (G i)] {K L : CompactOpenAddSubgroups G} : K = L ↔ K.addSubgroup = L.addSubgroup

theorem TauCeti.CompactOpenSubgroups.ext_iff {ι : Type u} {G : ι → Type v} [(i : ι) → Group (G i)] [(i : ι) → TopologicalSpace (G i)] {K L : CompactOpenSubgroups G} : K = L ↔ K.subgroup = L.subgroup