Documentation

TauCeti.GroupTheory.ProperPower

Proper powers in groups #

A proper power is a power with a natural exponent at least two. In particular the identity is a proper power; the predicate makes no exception for it, so an element that is not a proper power is nontrivial. Homomorphisms preserve proper powers; in particular conjugation preserves and reflects them.

Conjugation, inversion, and positive powers transport maximal-root decompositions, specified by a nonzero exponent and a root that is not a proper power. An element whose root exponents are bounded has such a decomposition, with a root of greatest exponent (Group.exists_maximalRoot_of_bddAbove).

source
def Group.IsProperPower {G : Type u_1} [Group G] (x : G) :
Prop

An element of a group is a proper power if it has a root with exponent at least two.

Instances For
    source
    theorem Group.isProperPower_iff {G : Type u_1} [Group G] {x : G} :
    IsProperPower x ↔ ∃ (y : G) (n : ℕ), 2 ≤ n ∧ x = y ^ n

    The root-and-exponent characterization of a proper power.

    source
    theorem Group.IsProperPower.map {G : Type u_1} {H : Type u_2} {F : Type u_3} [Group G] [Group H] [FunLike F G H] [MonoidHomClass F G H] (f : F) {x : G} (hx : IsProperPower x) :
    IsProperPower (f x)

    Homomorphisms preserve proper powers.

    source
    @[simp]
    theorem Group.IsProperPower.one {G : Type u_1} [Group G] :
    IsProperPower 1

    The identity is a proper power in every group.

    source
    theorem Group.isProperPower_pow {G : Type u_1} [Group G] (y : G) {n : ℕ} (hn : 2 ≤ n) :
    IsProperPower (y ^ n)

    Every natural power with exponent at least two is a proper power.

    source
    theorem Group.isProperPower_zpow {G : Type u_1} [Group G] (y : G) {n : ℤ} (hn : 2 ≤ n.natAbs) :
    IsProperPower (y ^ n)

    An integer power with absolute exponent at least two is a proper power.

    source
    theorem Group.ne_one_of_not_isProperPower {G : Type u_1} [Group G] {x : G} (hx : ¬IsProperPower x) :
    x ≠ 1

    An element that is not a proper power is not the identity.

    source
    theorem Group.natAbs_eq_one_of_not_isProperPower_zpow {G : Type u_1} [Group G] {y : G} {n : ℤ} (h : ¬IsProperPower (y ^ n)) :
    n.natAbs = 1

    If y ^ n is not a proper power, then n = 1 or n = -1. The exponent 0 is excluded because y ^ 0 = 1 is a proper power.

    source
    @[simp]
    theorem Group.isProperPower_inv {G : Type u_1} [Group G] {x : G} :
    IsProperPower x⁻¹ ↔ IsProperPower x

    An element is a proper power exactly when its inverse is.

    source
    theorem Group.not_isProperPower_ofAdd_one :
    ¬IsProperPower (Multiplicative.ofAdd 1)

    The generator of the additive integers, viewed multiplicatively, is not a proper power.

    source
    @[simp]
    theorem MulEquiv.isProperPower_map_iff {G : Type u_1} {H : Type u_2} [Group G] [Group H] (e : G ≃* H) {x : G} :
    Group.IsProperPower (e x) ↔ Group.IsProperPower x

    A multiplicative equivalence preserves and reflects proper powers.

    source
    @[simp]
    theorem Group.isProperPower_conj_iff {G : Type u_1} [Group G] (g x : G) :
    IsProperPower (g * x * g⁻¹) ↔ IsProperPower x

    Conjugation preserves and reflects proper powers.

    source
    theorem Group.maximalRoot_conj {G : Type u_1} [Group G] {x r : G} {k : ℕ} (g : G) (hk : k ≠ 0) (hx : r ^ k = x) (hr : ¬IsProperPower r) :
    k ≠ 0 ∧ (g * r * g⁻¹) ^ k = g * x * g⁻¹ ∧ ¬IsProperPower (g * r * g⁻¹)

    Conjugation transports a maximal-root decomposition without changing its exponent.

    source
    theorem Group.maximalRoot_inv {G : Type u_1} [Group G] {x r : G} {k : ℕ} (hk : k ≠ 0) (hx : r ^ k = x) (hr : ¬IsProperPower r) :
    k ≠ 0 ∧ r⁻¹ ^ k = x⁻¹ ∧ ¬IsProperPower r⁻¹

    Inversion transports a maximal-root decomposition without changing its exponent.

    source
    theorem Group.maximalRoot_pow {G : Type u_1} [Group G] {x r : G} {k m : ℕ} (hk : k ≠ 0) (hx : r ^ k = x) (hr : ¬IsProperPower r) (hm : m ≠ 0) :
    m * k ≠ 0 ∧ r ^ (m * k) = x ^ m ∧ ¬IsProperPower r

    A positive power transports a maximal-root decomposition by multiplying the exponent.

    source
    theorem Group.exists_maximalRoot_of_bddAbove {G : Type u_1} [Group G] {x : G} (hbdd : BddAbove {n : ℕ | ∃ (y : G), y ^ n = x}) :
    ∃ (r : G) (k : ℕ), k ≠ 0 ∧ r ^ k = x ∧ ¬IsProperPower r ∧ ∀ (y : G) (n : ℕ), y ^ n = x → n ≤ k

    An element x whose root exponents {n | ∃ y, y ^ n = x} are bounded above has a maximal-root decomposition r ^ k = x in which k is the greatest root exponent of x. The root r is not a proper power, since a root of r with exponent m ≥ 2 would be a root of x with exponent m * k > k. The hypothesis forces x ≠ 1, as every natural number is a root exponent of the identity.

    source
    theorem Group.not_isProperPower_of_zpowers_eq_centralizer {G : Type u_1} [Group G] [IsMulTorsionFree G] {x r : G} (hx : x ≠ 1) (hr : Subgroup.zpowers r = Subgroup.centralizer {x}) :
    ¬IsProperPower r

    A generator of the centralizer of a nontrivial element in a torsion-free group is not a proper power.