Topological closure of the submonoid closure

In this file we prove several versions of the following statement: if G is a compact topological group and s : Set G, then the topological closures of Submonoid.closure s and Subgroup.closure s are equal.

The proof is based on the following observation, see mapClusterPt_self_zpow_atTop_pow: each x^m, m : ℤ is a limit point (MapClusterPt) of the sequence x^n, n : ℕ, as n → ∞.

theorem mapClusterPt_atTop_zpow_iff_pow {G : Type u_1} [DivInvMonoid G] [TopologicalSpace G] {x y : G} : (MapClusterPt x Filter.atTop fun (x : ℤ) => y ^ x) ↔ MapClusterPt x Filter.atTop fun (x : ℕ) => y ^ x

theorem mapClusterPt_atTop_zsmul_iff_nsmul {G : Type u_1} [SubNegMonoid G] [TopologicalSpace G] {x y : G} : (MapClusterPt x Filter.atTop fun (x : ℤ) => x • y) ↔ MapClusterPt x Filter.atTop fun (x : ℕ) => x • y

theorem mapClusterPt_self_zpow_atTop_pow {G : Type u_1} [Group G] [TopologicalSpace G] [CompactSpace G] [IsTopologicalGroup G] (x : G) (m : ℤ) : MapClusterPt (x ^ m) Filter.atTop fun (x_1 : ℕ) => x ^ x_1

theorem mapClusterPt_self_zsmul_atTop_nsmul {G : Type u_1} [AddGroup G] [TopologicalSpace G] [CompactSpace G] [IsTopologicalAddGroup G] (x : G) (m : ℤ) : MapClusterPt (m • x) Filter.atTop fun (x_1 : ℕ) => x_1 • x

theorem mapClusterPt_one_atTop_pow {G : Type u_1} [Group G] [TopologicalSpace G] [CompactSpace G] [IsTopologicalGroup G] (x : G) : MapClusterPt 1 Filter.atTop fun (x_1 : ℕ) => x ^ x_1

theorem mapClusterPt_zero_atTop_nsmul {G : Type u_1} [AddGroup G] [TopologicalSpace G] [CompactSpace G] [IsTopologicalAddGroup G] (x : G) : MapClusterPt 0 Filter.atTop fun (x_1 : ℕ) => x_1 • x

theorem mapClusterPt_self_atTop_pow {G : Type u_1} [Group G] [TopologicalSpace G] [CompactSpace G] [IsTopologicalGroup G] (x : G) : MapClusterPt x Filter.atTop fun (x_1 : ℕ) => x ^ x_1

theorem mapClusterPt_self_atTop_nsmul {G : Type u_1} [AddGroup G] [TopologicalSpace G] [CompactSpace G] [IsTopologicalAddGroup G] (x : G) : MapClusterPt x Filter.atTop fun (x_1 : ℕ) => x_1 • x

theorem mapClusterPt_atTop_pow_tfae {G : Type u_1} [Group G] [TopologicalSpace G] [CompactSpace G] [IsTopologicalGroup G] (x y : G) : [MapClusterPt x Filter.atTop fun (x : ℕ) => y ^ x, MapClusterPt x Filter.atTop fun (x : ℤ) => y ^ x, x ∈ closure (Set.range fun (x : ℕ) => y ^ x), x ∈ closure (Set.range fun (x : ℤ) => y ^ x)].TFAE

theorem mapClusterPt_atTop_nsmul_tfae {G : Type u_1} [AddGroup G] [TopologicalSpace G] [CompactSpace G] [IsTopologicalAddGroup G] (x y : G) : [MapClusterPt x Filter.atTop fun (x : ℕ) => x • y, MapClusterPt x Filter.atTop fun (x : ℤ) => x • y, x ∈ closure (Set.range fun (x : ℕ) => x • y), x ∈ closure (Set.range fun (x : ℤ) => x • y)].TFAE

theorem mapClusterPt_atTop_pow_iff_mem_topologicalClosure_zpowers {G : Type u_1} [Group G] [TopologicalSpace G] [CompactSpace G] [IsTopologicalGroup G] {x y : G} : (MapClusterPt x Filter.atTop fun (x : ℕ) => y ^ x) ↔ x ∈ (Subgroup.zpowers y).topologicalClosure

theorem mapClusterPt_atTop_nsmul_iff_mem_topologicalClosure_zmultiples {G : Type u_1} [AddGroup G] [TopologicalSpace G] [CompactSpace G] [IsTopologicalAddGroup G] {x y : G} : (MapClusterPt x Filter.atTop fun (x : ℕ) => x • y) ↔ x ∈ (AddSubgroup.zmultiples y).topologicalClosure

@[simp]

theorem mapClusterPt_inv_atTop_pow {G : Type u_1} [Group G] [TopologicalSpace G] [CompactSpace G] [IsTopologicalGroup G] {x y : G} : (MapClusterPt x⁻¹ Filter.atTop fun (x : ℕ) => y ^ x) ↔ MapClusterPt x Filter.atTop fun (x : ℕ) => y ^ x

@[simp]

theorem mapClusterPt_neg_atTop_nsmul {G : Type u_1} [AddGroup G] [TopologicalSpace G] [CompactSpace G] [IsTopologicalAddGroup G] {x y : G} : (MapClusterPt (-x) Filter.atTop fun (x : ℕ) => x • y) ↔ MapClusterPt x Filter.atTop fun (x : ℕ) => x • y

theorem closure_range_zpow_eq_pow {G : Type u_1} [Group G] [TopologicalSpace G] [CompactSpace G] [IsTopologicalGroup G] (x : G) : closure (Set.range fun (x_1 : ℤ) => x ^ x_1) = closure (Set.range fun (x_1 : ℕ) => x ^ x_1)

theorem closure_range_zsmul_eq_nsmul {G : Type u_1} [AddGroup G] [TopologicalSpace G] [CompactSpace G] [IsTopologicalAddGroup G] (x : G) : closure (Set.range fun (x_1 : ℤ) => x_1 • x) = closure (Set.range fun (x_1 : ℕ) => x_1 • x)

theorem denseRange_zpow_iff_pow {G : Type u_1} [Group G] [TopologicalSpace G] [CompactSpace G] [IsTopologicalGroup G] {x : G} : (DenseRange fun (x_1 : ℤ) => x ^ x_1) ↔ DenseRange fun (x_1 : ℕ) => x ^ x_1

theorem denseRange_zsmul_iff_nsmul {G : Type u_1} [AddGroup G] [TopologicalSpace G] [CompactSpace G] [IsTopologicalAddGroup G] {x : G} : (DenseRange fun (x_1 : ℤ) => x_1 • x) ↔ DenseRange fun (x_1 : ℕ) => x_1 • x

theorem topologicalClosure_subgroupClosure_toSubmonoid {G : Type u_1} [Group G] [TopologicalSpace G] [CompactSpace G] [IsTopologicalGroup G] (s : Set G) : (Subgroup.closure s).topologicalClosure = (Submonoid.closure s).topologicalClosure

theorem topologicalClosure_addSubgroupClosure_toAddSubmonoid {G : Type u_1} [AddGroup G] [TopologicalSpace G] [CompactSpace G] [IsTopologicalAddGroup G] (s : Set G) : (AddSubgroup.closure s).topologicalClosure = (AddSubmonoid.closure s).topologicalClosure

theorem closure_submonoidClosure_eq_closure_subgroupClosure {G : Type u_1} [Group G] [TopologicalSpace G] [CompactSpace G] [IsTopologicalGroup G] (s : Set G) : closure ↑(Submonoid.closure s) = closure ↑(Subgroup.closure s)

theorem closure_addSubmonoidClosure_eq_closure_addSubgroupClosure {G : Type u_1} [AddGroup G] [TopologicalSpace G] [CompactSpace G] [IsTopologicalAddGroup G] (s : Set G) : closure ↑(AddSubmonoid.closure s) = closure ↑(AddSubgroup.closure s)

theorem dense_submonoidClosure_iff_subgroupClosure {G : Type u_1} [Group G] [TopologicalSpace G] [CompactSpace G] [IsTopologicalGroup G] {s : Set G} : Dense ↑(Submonoid.closure s) ↔ Dense ↑(Subgroup.closure s)

theorem dense_addSubmonoidClosure_iff_addSubgroupClosure {G : Type u_1} [AddGroup G] [TopologicalSpace G] [CompactSpace G] [IsTopologicalAddGroup G] {s : Set G} : Dense ↑(AddSubmonoid.closure s) ↔ Dense ↑(AddSubgroup.closure s)