Exponents with respect to a generator of a finite cyclic group

For a finite group G generated by g, every x : G is g ^ i for a unique i < orderOf g. This file names that exponent and records how it interacts with powers, products and homomorphisms of cyclic groups.

Main definitions

• TauCeti.cyclicLog g hg x: the unique i < orderOf g with g ^ i = x.

Main results

• TauCeti.pow_cyclicLog, TauCeti.cyclicLog_lt: the defining properties of cyclicLog.
• TauCeti.cyclicLog_pow: the exponent of g ^ i is i % orderOf g.
• TauCeti.cyclicLog_mul: exponents add modulo orderOf g.
• TauCeti.cyclicLog_map: a homomorphism sending g to g' ^ d multiplies exponents by d.

noncomputable def TauCeti.cyclicLog {G : Type u_1} [Group G] [Finite G] (g : G) (hg : ∀ (x : G), x ∈ Subgroup.zpowers g) (x : G) : ℕ

The exponent of x with respect to the generator g of a finite group: the unique i < orderOf g with g ^ i = x.

Equations

• TauCeti.cyclicLog g hg x = ↑((finEquivZPowers ⋯).symm ⟨x, ⋯⟩)

@[simp]

theorem TauCeti.pow_cyclicLog {G : Type u_1} [Group G] [Finite G] (g : G) (hg : ∀ (x : G), x ∈ Subgroup.zpowers g) (x : G) : g ^ cyclicLog g hg x = x

cyclicLog g hg x is an exponent of g giving x.

theorem TauCeti.cyclicLog_lt {G : Type u_1} [Group G] [Finite G] (g : G) (hg : ∀ (x : G), x ∈ Subgroup.zpowers g) (x : G) : cyclicLog g hg x < orderOf g

cyclicLog g hg x is reduced modulo the order of g.

@[simp]

theorem TauCeti.cyclicLog_pow {G : Type u_1} [Group G] [Finite G] (g : G) (hg : ∀ (x : G), x ∈ Subgroup.zpowers g) (i : ℕ) : cyclicLog g hg (g ^ i) = i % orderOf g

The exponent of g ^ i is i reduced modulo the order of g.

theorem TauCeti.cyclicLog_mul {G : Type u_1} [Group G] [Finite G] (g : G) (hg : ∀ (x : G), x ∈ Subgroup.zpowers g) (x y : G) : cyclicLog g hg (x * y) = (cyclicLog g hg x + cyclicLog g hg y) % orderOf g

Exponents with respect to g add modulo the order of g.

theorem TauCeti.cyclicLog_map {G : Type u_1} [Group G] [Finite G] (g : G) (hg : ∀ (x : G), x ∈ Subgroup.zpowers g) {G' : Type u_2} [Group G'] [Finite G'] (f : G →* G') {g' : G'} (hg' : ∀ (x : G'), x ∈ Subgroup.zpowers g') {d : ℕ} (hfg : f g = g' ^ d) (x : G) : cyclicLog g' hg' (f x) = d * cyclicLog g hg x % orderOf g'

A homomorphism of finite cyclic groups sending the generator g to g' ^ d multiplies exponents by d, modulo the order of g'.