Period of a group action

This module defines some helpful lemmas around [MulAction.period] and [AddAction.period]. The period of a point a by a group element g is the smallest m such that g ^ m • a = a (resp. (m • g) +ᵥ a = a) for a given g : G and a : α.

If such an m does not exist, then by convention MulAction.period and AddAction.period return 0.

theorem AddAction.le_period {α : Type v} {M : Type u} [AddMonoid M] [AddAction M α] {m : M} {a : α} {n : ℕ} (period_pos : 0 < AddAction.period m a) (moved : ∀ (k : ℕ), 0 < k → k < n → k • m +ᵥ a ≠ a) : n ≤ AddAction.period m a

If the action is periodic, then a lower bound for its period can be computed.

theorem MulAction.le_period {α : Type v} {M : Type u} [Monoid M] [MulAction M α] {m : M} {a : α} {n : ℕ} (period_pos : 0 < MulAction.period m a) (moved : ∀ (k : ℕ), 0 < k → k < n → m ^ k • a ≠ a) : n ≤ MulAction.period m a

If the action is periodic, then a lower bound for its period can be computed.

theorem AddAction.period_le_of_fixed {α : Type v} {M : Type u} [AddMonoid M] [AddAction M α] {m : M} {a : α} {n : ℕ} (n_pos : 0 < n) (fixed : n • m +ᵥ a = a) : AddAction.period m a ≤ n

If for some n, (n • m) +ᵥ a = a, then period m a ≤ n.

theorem MulAction.period_le_of_fixed {α : Type v} {M : Type u} [Monoid M] [MulAction M α] {m : M} {a : α} {n : ℕ} (n_pos : 0 < n) (fixed : m ^ n • a = a) : MulAction.period m a ≤ n

If for some n, m ^ n • a = a, then period m a ≤ n.

theorem AddAction.period_pos_of_fixed {α : Type v} {M : Type u} [AddMonoid M] [AddAction M α] {m : M} {a : α} {n : ℕ} (n_pos : 0 < n) (fixed : n • m +ᵥ a = a) : 0 < AddAction.period m a

If for some n, (n • m) +ᵥ a = a, then 0 < period m a.

theorem MulAction.period_pos_of_fixed {α : Type v} {M : Type u} [Monoid M] [MulAction M α] {m : M} {a : α} {n : ℕ} (n_pos : 0 < n) (fixed : m ^ n • a = a) : 0 < MulAction.period m a

If for some n, m ^ n • a = a, then 0 < period m a.

theorem AddAction.period_eq_zero_iff {α : Type v} {M : Type u} [AddMonoid M] [AddAction M α] {m : M} {a : α} : AddAction.period m a = 1 ↔ m +ᵥ a = a

theorem MulAction.period_eq_one_iff {α : Type v} {M : Type u} [Monoid M] [MulAction M α] {m : M} {a : α} : MulAction.period m a = 1 ↔ m • a = a

theorem AddAction.nsmul_vadd_ne_of_lt_period {α : Type v} {M : Type u} [AddMonoid M] [AddAction M α] {m : M} {a : α} {n : ℕ} (n_pos : 0 < n) (n_lt_period : n < AddAction.period m a) : n • m +ᵥ a ≠ a

For any non-zero n less than the period of m on a, a is moved by n • m.

theorem MulAction.pow_smul_ne_of_lt_period {α : Type v} {M : Type u} [Monoid M] [MulAction M α] {m : M} {a : α} {n : ℕ} (n_pos : 0 < n) (n_lt_period : n < MulAction.period m a) : m ^ n • a ≠ a

For any non-zero n less than the period of m on a, a is moved by m ^ n.

MulAction.period for common group elements

@[simp]

theorem AddAction.period_zero {α : Type v} (M : Type u) [AddMonoid M] [AddAction M α] (a : α) : AddAction.period 0 a = 1

@[simp]

theorem MulAction.period_one {α : Type v} (M : Type u) [Monoid M] [MulAction M α] (a : α) : MulAction.period 1 a = 1

@[simp]

theorem AddAction.period_neg {α : Type v} {G : Type u} [AddGroup G] [AddAction G α] (g : G) (a : α) : AddAction.period (-g) a = AddAction.period g a

@[simp]

theorem MulAction.period_inv {α : Type v} {G : Type u} [Group G] [MulAction G α] (g : G) (a : α) : MulAction.period g⁻¹ a = MulAction.period g a

MulAction.period and group exponents

The period of a given element m : M can be bounded by the Monoid.exponent M or orderOf m.

theorem AddAction.period_dvd_addOrderOf {α : Type v} {M : Type u} [AddMonoid M] [AddAction M α] (m : M) (a : α) : AddAction.period m a ∣ addOrderOf m

theorem MulAction.period_dvd_orderOf {α : Type v} {M : Type u} [Monoid M] [MulAction M α] (m : M) (a : α) : MulAction.period m a ∣ orderOf m

theorem AddAction.period_pos_of_addOrderOf_pos {α : Type v} {M : Type u} [AddMonoid M] [AddAction M α] {m : M} (order_pos : 0 < addOrderOf m) (a : α) : 0 < AddAction.period m a

theorem MulAction.period_pos_of_orderOf_pos {α : Type v} {M : Type u} [Monoid M] [MulAction M α] {m : M} (order_pos : 0 < orderOf m) (a : α) : 0 < MulAction.period m a

theorem AddAction.period_le_addOrderOf {α : Type v} {M : Type u} [AddMonoid M] [AddAction M α] {m : M} (order_pos : 0 < addOrderOf m) (a : α) : AddAction.period m a ≤ addOrderOf m

theorem MulAction.period_le_orderOf {α : Type v} {M : Type u} [Monoid M] [MulAction M α] {m : M} (order_pos : 0 < orderOf m) (a : α) : MulAction.period m a ≤ orderOf m

theorem AddAction.period_dvd_exponent {α : Type v} {M : Type u} [AddMonoid M] [AddAction M α] (m : M) (a : α) : AddAction.period m a ∣ AddMonoid.exponent M

theorem MulAction.period_dvd_exponent {α : Type v} {M : Type u} [Monoid M] [MulAction M α] (m : M) (a : α) : MulAction.period m a ∣ Monoid.exponent M

theorem AddAction.period_pos_of_exponent_pos {α : Type v} {M : Type u} [AddMonoid M] [AddAction M α] (exp_pos : 0 < AddMonoid.exponent M) (m : M) (a : α) : 0 < AddAction.period m a

theorem MulAction.period_pos_of_exponent_pos {α : Type v} {M : Type u} [Monoid M] [MulAction M α] (exp_pos : 0 < Monoid.exponent M) (m : M) (a : α) : 0 < MulAction.period m a

theorem AddAction.period_le_exponent {α : Type v} {M : Type u} [AddMonoid M] [AddAction M α] (exp_pos : 0 < AddMonoid.exponent M) (m : M) (a : α) : AddAction.period m a ≤ AddMonoid.exponent M

theorem MulAction.period_le_exponent {α : Type v} {M : Type u} [Monoid M] [MulAction M α] (exp_pos : 0 < Monoid.exponent M) (m : M) (a : α) : MulAction.period m a ≤ Monoid.exponent M

theorem AddAction.period_bounded_of_exponent_pos (α : Type v) {M : Type u} [AddMonoid M] [AddAction M α] (exp_pos : 0 < AddMonoid.exponent M) (m : M) : BddAbove (Set.range fun (a : α) => AddAction.period m a)

theorem MulAction.period_bounded_of_exponent_pos (α : Type v) {M : Type u} [Monoid M] [MulAction M α] (exp_pos : 0 < Monoid.exponent M) (m : M) : BddAbove (Set.range fun (a : α) => MulAction.period m a)