vadd_eq_self_of_preimage_zsmul_eq_self
theorem vadd_eq_self_of_preimage_zsmul_eq_self :
∀ {G : Type u_1} [inst : AddCommGroup G] {n : ℤ} {s : Set G},
(fun x => n • x) ⁻¹' s = s → ∀ {g : G} {j : ℕ}, n ^ j • g = 0 → g +ᵥ s = s
This theorem states that for any integer `n` and subset `s` of an additive commutative group `G` that is invariant under the preimage of the map `x ↦ n • x`, the set `s` is also invariant under the pointwise action of the additive subgroup of elements `g : G` that satisfy `(n^j) • g = 0` for some natural number `j`. This additive subgroup is known as the Prüfer subgroup when `G` is the Additive Circle and `n` is a prime number. Essentially, the theorem provides a condition under which a set in an additive group remains unchanged when acted upon by members of a specific additive subgroup.
More concisely: For any additive commutative group G and invariant subset s under the map x ↦ n • x for some integer n, s is also invariant under the pointwise action of the Prüfer subgroup of G consisting of g such that (n^j) • g = 0 for some natural number j.
|
smul_eq_self_of_preimage_zpow_eq_self
theorem smul_eq_self_of_preimage_zpow_eq_self :
∀ {G : Type u_1} [inst : CommGroup G] {n : ℤ} {s : Set G},
(fun x => x ^ n) ⁻¹' s = s → ∀ {g : G} {j : ℕ}, g ^ n ^ j = 1 → g • s = s
The theorem `smul_eq_self_of_preimage_zpow_eq_self` states that for a given integer `n` and a subset `s` of a commutative group `G` which remains invariant under preimage for the map `x ↦ x^n`, the subset `s` is also invariant under the action of the subgroup of elements `g : G` that satisfy the condition `g^(n^j) = 1` for some natural number `j`. This particular subgroup is referred to as the Prüfer subgroup when `G` is the circle and `n` is a prime number. In other words, if you scale `s` by any element `g` from this subgroup, `s` remains unchanged.
More concisely: If a subset `s` of a commutative group `G` is invariant under the map `x ↦ x^n`, then it is also invariant under the subgroup of elements `g : G` such that `g^(n^j) = 1` for some natural number `j`.
|