mathlib3 documentation

group_theory.specific_groups.cyclic

Cyclic groups #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

A group G is called cyclic if there exists an element g : G such that every element of G is of the form g ^ n for some n : ℕ. This file only deals with the predicate on a group to be cyclic. For the concrete cyclic group of order n, see data.zmod.basic.

Main definitions #

is_cyclic is a predicate on a group stating that the group is cyclic.

Main statements #

is_cyclic_of_prime_card proves that a finite group of prime order is cyclic.
is_simple_group_of_prime_card, is_simple_group.is_cyclic, and is_simple_group.prime_card classify finite simple abelian groups.
is_cyclic.exponent_eq_card: For a finite cyclic group G, the exponent is equal to the group's cardinality.
is_cyclic.exponent_eq_zero_of_infinite: Infinite cyclic groups have exponent zero.
is_cyclic.iff_exponent_eq_card: A finite commutative group is cyclic iff its exponent is equal to its cardinality.

Tags #

cyclic group

@[class]

structure is_add_cyclic (α : Type u) [add_group α] :

Prop

exists_generator : ∃ (g : α), ∀ (x : α), x ∈ add_subgroup.zmultiples g

A group is called cyclic if it is generated by a single element.

Instances of this typeclass

@[class]

structure is_cyclic (α : Type u) [group α] :

Prop

exists_generator : ∃ (g : α), ∀ (x : α), x ∈ subgroup.zpowers g

A group is called cyclic if it is generated by a single element.

Instances of this typeclass

@[protected, instance]

def is_cyclic_of_subsingleton {α : Type u} [group α] [subsingleton α] :

@[protected, instance]

def is_add_cyclic_of_subsingleton {α : Type u} [add_group α] [subsingleton α] :

is_add_cyclic α

def is_add_cyclic.add_comm_group {α : Type u} [hg : add_group α] [is_add_cyclic α] :

add_comm_group α

A cyclic group is always commutative. This is not an instance because often we have a better proof of add_comm_group.

Equations

is_add_cyclic.add_comm_group = {add := add_group.add hg, add_assoc := _, zero := add_group.zero hg, zero_add := _, add_zero := _, nsmul := add_group.nsmul hg, nsmul_zero' := _, nsmul_succ' := _, neg := add_group.neg hg, sub := add_group.sub hg, sub_eq_add_neg := _, zsmul := add_group.zsmul hg, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _}

def is_cyclic.comm_group {α : Type u} [hg : group α] [is_cyclic α] :

A cyclic group is always commutative. This is not an instance because often we have a better proof of comm_group.

Equations

is_cyclic.comm_group = {mul := group.mul hg, mul_assoc := _, one := group.one hg, one_mul := _, mul_one := _, npow := group.npow hg, npow_zero' := _, npow_succ' := _, inv := group.inv hg, div := group.div hg, div_eq_mul_inv := _, zpow := group.zpow hg, zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, mul_left_inv := _, mul_comm := _}

theorem monoid_add_hom.map_add_cyclic {G : Type u_1} [add_group G] [h : is_add_cyclic G] (σ : G →+ G) :

∃ (m : ℤ), ∀ (g : G), ⇑σ g = m • g

theorem monoid_hom.map_cyclic {G : Type u_1} [group G] [h : is_cyclic G] (σ : G →* G) :

∃ (m : ℤ), ∀ (g : G), ⇑σ g = g ^ m

theorem is_add_cyclic_of_order_of_eq_card {α : Type u} [add_group α] [fintype α] (x : α) (hx : add_order_of x = fintype.card α) :

is_add_cyclic α

theorem is_cyclic_of_order_of_eq_card {α : Type u} [group α] [fintype α] (x : α) (hx : order_of x = fintype.card α) :

theorem is_cyclic_of_prime_card {α : Type u} [group α] [fintype α] {p : ℕ} [hp : fact (nat.prime p)] (h : fintype.card α = p) :

A finite group of prime order is cyclic.

theorem is_add_cyclic_of_prime_card {α : Type u} [add_group α] [fintype α] {p : ℕ} [hp : fact (nat.prime p)] (h : fintype.card α = p) :

is_add_cyclic α

A finite group of prime order is cyclic.

theorem add_order_of_eq_card_of_forall_mem_zmultiples {α : Type u} [add_group α] [fintype α] {g : α} (hx : ∀ (x : α), x ∈ add_subgroup.zmultiples g) :

add_order_of g = fintype.card α

theorem order_of_eq_card_of_forall_mem_zpowers {α : Type u} [group α] [fintype α] {g : α} (hx : ∀ (x : α), x ∈ subgroup.zpowers g) :

order_of g = fintype.card α

theorem infinite.order_of_eq_zero_of_forall_mem_zpowers {α : Type u} [group α] [infinite α] {g : α} (h : ∀ (x : α), x ∈ subgroup.zpowers g) :

theorem infinite.add_order_of_eq_zero_of_forall_mem_zmultiples {α : Type u} [add_group α] [infinite α] {g : α} (h : ∀ (x : α), x ∈ add_subgroup.zmultiples g) :

add_order_of g = 0

@[protected, instance]

def bot.is_add_cyclic {α : Type u} [add_group α] :

is_add_cyclic ↥⊥

@[protected, instance]

def bot.is_cyclic {α : Type u} [group α] :

is_cyclic ↥⊥

@[protected, instance]

def subgroup.is_cyclic {α : Type u} [group α] [is_cyclic α] (H : subgroup α) :

@[protected, instance]

def add_subgroup.is_add_cyclic {α : Type u} [add_group α] [is_add_cyclic α] (H : add_subgroup α) :

is_add_cyclic ↥H

theorem is_add_cyclic.card_pow_eq_one_le {α : Type u} [add_group α] [decidable_eq α] [fintype α] [is_add_cyclic α] {n : ℕ} (hn0 : 0 < n) :

(finset.filter (λ (a : α), n • a = 0) finset.univ).card ≤ n

theorem is_cyclic.card_pow_eq_one_le {α : Type u} [group α] [decidable_eq α] [fintype α] [is_cyclic α] {n : ℕ} (hn0 : 0 < n) :

(finset.filter (λ (a : α), a ^ n = 1) finset.univ).card ≤ n

theorem is_add_cyclic.exists_add_monoid_generator {α : Type u} [add_group α] [finite α] [is_add_cyclic α] :

∃ (x : α), ∀ (y : α), y ∈ add_submonoid.multiples x

theorem is_cyclic.exists_monoid_generator {α : Type u} [group α] [finite α] [is_cyclic α] :

∃ (x : α), ∀ (y : α), y ∈ submonoid.powers x

theorem is_add_cyclic.image_range_order_of {α : Type u} {a : α} [add_group α] [decidable_eq α] [fintype α] (ha : ∀ (x : α), x ∈ add_subgroup.zmultiples a) :

finset.image (λ (i : ℕ), i • a) (finset.range (add_order_of a)) = finset.univ

theorem is_cyclic.image_range_order_of {α : Type u} {a : α} [group α] [decidable_eq α] [fintype α] (ha : ∀ (x : α), x ∈ subgroup.zpowers a) :

finset.image (λ (i : ℕ), a ^ i) (finset.range (order_of a)) = finset.univ

theorem is_cyclic.image_range_card {α : Type u} {a : α} [group α] [decidable_eq α] [fintype α] (ha : ∀ (x : α), x ∈ subgroup.zpowers a) :

finset.image (λ (i : ℕ), a ^ i) (finset.range (fintype.card α)) = finset.univ

theorem is_add_cyclic.image_range_card {α : Type u} {a : α} [add_group α] [decidable_eq α] [fintype α] (ha : ∀ (x : α), x ∈ add_subgroup.zmultiples a) :

finset.image (λ (i : ℕ), i • a) (finset.range (fintype.card α)) = finset.univ

theorem card_order_of_eq_totient_aux₂ {α : Type u} [group α] [decidable_eq α] [fintype α] (hn : ∀ (n : ℕ), 0 < n → (finset.filter (λ (a : α), a ^ n = 1) finset.univ).card ≤ n) {d : ℕ} (hd : d ∣ fintype.card α) :

(finset.filter (λ (a : α), order_of a = d) finset.univ).card = d.totient

theorem is_cyclic_of_card_pow_eq_one_le {α : Type u} [group α] [decidable_eq α] [fintype α] (hn : ∀ (n : ℕ), 0 < n → (finset.filter (λ (a : α), a ^ n = 1) finset.univ).card ≤ n) :

theorem is_add_cyclic_of_card_pow_eq_one_le {α : Type u_1} [add_group α] [decidable_eq α] [fintype α] (hn : ∀ (n : ℕ), 0 < n → (finset.filter (λ (a : α), n • a = 0) finset.univ).card ≤ n) :

is_add_cyclic α

theorem is_cyclic.card_order_of_eq_totient {α : Type u} [group α] [is_cyclic α] [fintype α] {d : ℕ} (hd : d ∣ fintype.card α) :

(finset.filter (λ (a : α), order_of a = d) finset.univ).card = d.totient

theorem is_add_cyclic.card_order_of_eq_totient {α : Type u_1} [add_group α] [is_add_cyclic α] [fintype α] {d : ℕ} (hd : d ∣ fintype.card α) :

(finset.filter (λ (a : α), add_order_of a = d) finset.univ).card = d.totient

theorem is_simple_add_group_of_prime_card {α : Type u} [add_group α] [fintype α] {p : ℕ} [hp : fact (nat.prime p)] (h : fintype.card α = p) :

is_simple_add_group α

A finite group of prime order is simple.

theorem is_simple_group_of_prime_card {α : Type u} [group α] [fintype α] {p : ℕ} [hp : fact (nat.prime p)] (h : fintype.card α = p) :

is_simple_group α

A finite group of prime order is simple.

theorem commutative_of_add_cyclic_center_quotient {G : Type u_1} {H : Type u_2} [add_group G] [add_group H] [is_add_cyclic H] (f : G →+ H) (hf : f.ker ≤ add_subgroup.center G) (a b : G) :

a + b = b + a

A group is commutative if the quotient by the center is cyclic. Also see add_comm_group_of_cycle_center_quotient for the add_comm_group instance.

theorem commutative_of_cyclic_center_quotient {G : Type u_1} {H : Type u_2} [group G] [group H] [is_cyclic H] (f : G →* H) (hf : f.ker ≤ subgroup.center G) (a b : G) :

a * b = b * a

A group is commutative if the quotient by the center is cyclic. Also see comm_group_of_cycle_center_quotient for the comm_group instance.

def comm_group_of_cycle_center_quotient {G : Type u_1} {H : Type u_2} [group G] [group H] [is_cyclic H] (f : G →* H) (hf : f.ker ≤ subgroup.center G) :

A group is commutative if the quotient by the center is cyclic.

Equations

comm_group_of_cycle_center_quotient f hf = {mul := group.mul (show group G, from _inst_1), mul_assoc := _, one := group.one (show group G, from _inst_1), one_mul := _, mul_one := _, npow := group.npow (show group G, from _inst_1), npow_zero' := _, npow_succ' := _, inv := group.inv (show group G, from _inst_1), div := group.div (show group G, from _inst_1), div_eq_mul_inv := _, zpow := group.zpow (show group G, from _inst_1), zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, mul_left_inv := _, mul_comm := _}

def commutative_of_add_cycle_center_quotient {G : Type u_1} {H : Type u_2} [add_group G] [add_group H] [is_add_cyclic H] (f : G →+ H) (hf : f.ker ≤ add_subgroup.center G) :

add_comm_group G

A group is commutative if the quotient by the center is cyclic.

Equations

commutative_of_add_cycle_center_quotient f hf = {add := add_group.add (show add_group G, from _inst_1), add_assoc := _, zero := add_group.zero (show add_group G, from _inst_1), zero_add := _, add_zero := _, nsmul := add_group.nsmul (show add_group G, from _inst_1), nsmul_zero' := _, nsmul_succ' := _, neg := add_group.neg (show add_group G, from _inst_1), sub := add_group.sub (show add_group G, from _inst_1), sub_eq_add_neg := _, zsmul := add_group.zsmul (show add_group G, from _inst_1), zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _}

@[protected, instance]

def is_simple_add_group.is_add_cyclic {α : Type u} [add_comm_group α] [is_simple_add_group α] :

is_add_cyclic α

@[protected, instance]

def is_simple_group.is_cyclic {α : Type u} [comm_group α] [is_simple_group α] :

theorem is_simple_add_group.prime_card {α : Type u} [add_comm_group α] [is_simple_add_group α] [fintype α] :

nat.prime (fintype.card α)

theorem is_simple_group.prime_card {α : Type u} [comm_group α] [is_simple_group α] [fintype α] :

nat.prime (fintype.card α)

theorem comm_group.is_simple_iff_is_cyclic_and_prime_card {α : Type u} [fintype α] [comm_group α] :

is_simple_group α ↔ is_cyclic α ∧ nat.prime (fintype.card α)

theorem add_comm_group.is_simple_iff_is_add_cyclic_and_prime_card {α : Type u} [fintype α] [add_comm_group α] :

is_simple_add_group α ↔ is_add_cyclic α ∧ nat.prime (fintype.card α)

theorem is_add_cyclic.exponent_eq_card {α : Type u} [add_group α] [is_add_cyclic α] [fintype α] :

add_monoid.exponent α = fintype.card α

theorem is_cyclic.exponent_eq_card {α : Type u} [group α] [is_cyclic α] [fintype α] :

monoid.exponent α = fintype.card α

theorem is_cyclic.of_exponent_eq_card {α : Type u} [comm_group α] [fintype α] (h : monoid.exponent α = fintype.card α) :

theorem is_add_cyclic.of_exponent_eq_card {α : Type u} [add_comm_group α] [fintype α] (h : add_monoid.exponent α = fintype.card α) :

is_add_cyclic α

theorem is_cyclic.iff_exponent_eq_card {α : Type u} [comm_group α] [fintype α] :

is_cyclic α ↔ monoid.exponent α = fintype.card α

theorem is_add_cyclic.iff_exponent_eq_card {α : Type u} [add_comm_group α] [fintype α] :

is_add_cyclic α ↔ add_monoid.exponent α = fintype.card α

theorem is_cyclic.exponent_eq_zero_of_infinite {α : Type u} [group α] [is_cyclic α] [infinite α] :

monoid.exponent α = 0

theorem is_add_cyclic.exponent_eq_zero_of_infinite {α : Type u} [add_group α] [is_add_cyclic α] [infinite α] :

add_monoid.exponent α = 0