Cyclic groups

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

• IsCyclic is a predicate on a group stating that the group is cyclic.

Main statements

• isCyclic_of_prime_card proves that a finite group of prime order is cyclic.
• isSimpleGroup_of_prime_card, IsSimpleGroup.isCyclic, and IsSimpleGroup.prime_card classify finite simple abelian groups.
• IsCyclic.exponent_eq_card: For a finite cyclic group G, the exponent is equal to the group's cardinality.
• IsCyclic.exponent_eq_zero_of_infinite: Infinite cyclic groups have exponent zero.
• IsCyclic.iff_exponent_eq_card: A finite commutative group is cyclic iff its exponent is equal to its cardinality.

Tags

cyclic group

class IsAddCyclic (α : Type u) [AddGroup α] : Prop

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

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

class IsCyclic (α : 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.

theorem isAddCyclic_of_subsingleton.proof_1 {α : Type u_1} [AddGroup α] [Subsingleton α] : IsAddCyclic α

instance isAddCyclic_of_subsingleton {α : Type u} [AddGroup α] [Subsingleton α] : IsAddCyclic α

Equations

• @isAddCyclic_of_subsingleton = @isAddCyclic_of_subsingleton.proof_1

instance isCyclic_of_subsingleton {α : Type u} [Group α] [Subsingleton α] : IsCyclic α

Equations

• @isCyclic_of_subsingleton = @isCyclic_of_subsingleton.proof_1

abbrev IsAddCyclic.addCommGroup.match_1 {α : Type u_1} [hg : AddGroup α] (y : α) : (w : α) → ∀ (motive : y ∈ AddSubgroup.zmultiples w → Prop) (x : y ∈ AddSubgroup.zmultiples w), (∀ (w_1 : ℤ) (hm : (fun x x_1 => x_1 • x) w w_1 = y), motive (_ : ∃ y, (fun x x_1 => x_1 • x) w y = y)) → motive x

Equations

• IsAddCyclic.addCommGroup.match_1 y w motive x h_1 = Exists.casesOn x fun w h => h_1 w h

abbrev IsAddCyclic.addCommGroup.match_2 {α : Type u_1} [hg : AddGroup α] (motive : (∃ g, ∀ (x : α), x ∈ AddSubgroup.zmultiples g) → Prop) : (x : ∃ g, ∀ (x : α), x ∈ AddSubgroup.zmultiples g) → ((w : α) → (hg : ∀ (x : α), x ∈ AddSubgroup.zmultiples w) → motive (_ : ∃ g, ∀ (x : α), x ∈ AddSubgroup.zmultiples g)) → motive x

Equations

• IsAddCyclic.addCommGroup.match_2 motive x h_1 = Exists.casesOn x fun w h => h_1 w h

def IsAddCyclic.addCommGroup {α : Type u} [hg : AddGroup α] [IsAddCyclic α] : AddCommGroup α

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

Equations

• IsAddCyclic.addCommGroup = AddCommGroup.mk (_ : ∀ (x y : α), x + y = y + x)

theorem IsAddCyclic.addCommGroup.proof_1 {α : Type u_1} [hg : AddGroup α] [IsAddCyclic α] (x : α) (y : α) : x + y = y + x

def IsCyclic.commGroup {α : Type u} [hg : Group α] [IsCyclic α] : CommGroup α

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

Equations

• IsCyclic.commGroup = CommGroup.mk (_ : ∀ (x y : α), x * y = y * x)

theorem MonoidAddHom.map_add_cyclic {G : Type u_1} [AddGroup G] [h : IsAddCyclic G] (σ : G →+ G) : ∃ m, ∀ (g : G), ↑σ g = m • g

theorem MonoidHom.map_cyclic {G : Type u_1} [Group G] [h : IsCyclic G] (σ : G →* G) : ∃ m, ∀ (g : G), ↑σ g = g ^ m

theorem isAddCyclic_of_orderOf_eq_card {α : Type u} [AddGroup α] [Fintype α] (x : α) (hx : addOrderOf x = Fintype.card α) : IsAddCyclic α

theorem isCyclic_of_orderOf_eq_card {α : Type u} [Group α] [Fintype α] (x : α) (hx : orderOf x = Fintype.card α) : IsCyclic α

theorem isAddCyclic_of_prime_card {α : Type u} [AddGroup α] [Fintype α] {p : ℕ} [hp : Fact (Nat.Prime p)] (h : Fintype.card α = p) : IsAddCyclic α

A finite group of prime order is cyclic.

theorem isCyclic_of_prime_card {α : Type u} [Group α] [Fintype α] {p : ℕ} [hp : Fact (Nat.Prime p)] (h : Fintype.card α = p) : IsCyclic α

A finite group of prime order is cyclic.

theorem addOrderOf_eq_card_of_forall_mem_zmultiples {α : Type u} [AddGroup α] [Fintype α] {g : α} (hx : ∀ (x : α), x ∈ AddSubgroup.zmultiples g) : addOrderOf g = Fintype.card α

theorem orderOf_eq_card_of_forall_mem_zpowers {α : Type u} [Group α] [Fintype α] {g : α} (hx : ∀ (x : α), x ∈ Subgroup.zpowers g) : orderOf g = Fintype.card α

theorem exists_nsmul_ne_zero_of_isAddCyclic {G : Type u_1} [AddGroup G] [Fintype G] [G_cyclic : IsAddCyclic G] {k : ℕ} (k_pos : k ≠ 0) (k_lt_card_G : k < Fintype.card G) : ∃ a, k • a ≠ 0

theorem exists_pow_ne_one_of_isCyclic {G : Type u_1} [Group G] [Fintype G] [G_cyclic : IsCyclic G] {k : ℕ} (k_pos : k ≠ 0) (k_lt_card_G : k < Fintype.card G) : ∃ a, a ^ k ≠ 1

theorem Infinite.addOrderOf_eq_zero_of_forall_mem_zmultiples {α : Type u} [AddGroup α] [Infinite α] {g : α} (h : ∀ (x : α), x ∈ AddSubgroup.zmultiples g) : addOrderOf g = 0

theorem Infinite.orderOf_eq_zero_of_forall_mem_zpowers {α : Type u} [Group α] [Infinite α] {g : α} (h : ∀ (x : α), x ∈ Subgroup.zpowers g) : orderOf g = 0

theorem Bot.isAddCyclic.proof_1 {α : Type u_1} [AddGroup α] : IsAddCyclic { x // x ∈ ⊥ }

instance Bot.isAddCyclic {α : Type u} [AddGroup α] : IsAddCyclic { x // x ∈ ⊥ }

Equations

• @Bot.isAddCyclic = @Bot.isAddCyclic.proof_1

instance Bot.isCyclic {α : Type u} [Group α] : IsCyclic { x // x ∈ ⊥ }

Equations

• @Bot.isCyclic = @Bot.isCyclic.proof_1

abbrev AddSubgroup.isAddCyclic.match_1 {α : Type u_1} [AddGroup α] (g : α) (x : α) (motive : x ∈ AddSubgroup.zmultiples g → Prop) : (x : x ∈ AddSubgroup.zmultiples g) → ((k : ℤ) → (hk : (fun x x_1 => x_1 • x) g k = x) → motive (_ : ∃ y, (fun x x_1 => x_1 • x) g y = x)) → motive x

Equations

• AddSubgroup.isAddCyclic.match_1 g x motive x h_1 = Exists.casesOn x fun w h => h_1 w h

abbrev AddSubgroup.isAddCyclic.match_3 {α : Type u_1} [AddGroup α] (H : AddSubgroup α) (motive : (∃ x, x ∈ H ∧ x ≠ 0) → Prop) : (hx : ∃ x, x ∈ H ∧ x ≠ 0) → ((x : α) → (hx₁ : x ∈ H) → (hx₂ : x ≠ 0) → motive (_ : ∃ x, x ∈ H ∧ x ≠ 0)) → motive hx

Equations

• AddSubgroup.isAddCyclic.match_3 H motive hx h_1 = Exists.casesOn hx fun w h => And.casesOn h fun left right => h_1 w left right

abbrev AddSubgroup.isAddCyclic.match_2 {α : Type u_1} [AddGroup α] (H : AddSubgroup α) (motive : { x // x ∈ H } → Prop) : (x : { x // x ∈ H }) → ((x : α) → (hx : x ∈ H) → motive { val := x, property := hx }) → motive x

Equations

• AddSubgroup.isAddCyclic.match_2 H motive x h_1 = Subtype.casesOn x fun val property => h_1 val property

theorem AddSubgroup.isAddCyclic.proof_1 {α : Type u_1} [AddGroup α] [IsAddCyclic α] (H : AddSubgroup α) : IsAddCyclic { x // x ∈ H }

instance AddSubgroup.isAddCyclic {α : Type u} [AddGroup α] [IsAddCyclic α] (H : AddSubgroup α) : IsAddCyclic { x // x ∈ H }

Equations

• @AddSubgroup.isAddCyclic = @AddSubgroup.isAddCyclic.proof_1

instance Subgroup.isCyclic {α : Type u} [Group α] [IsCyclic α] (H : Subgroup α) : IsCyclic { x // x ∈ H }

Equations

• @Subgroup.isCyclic = @Subgroup.isCyclic.proof_1

abbrev IsAddCyclic.card_pow_eq_one_le.match_1 {α : Type u_1} [AddGroup α] (g : α) (x : α) (motive : x ∈ AddSubmonoid.multiples g → Prop) : (x : x ∈ AddSubmonoid.multiples g) → ((m : ℕ) → (hm : (fun x x_1 => x_1 • x) g m = x) → motive (_ : ∃ y, (fun x x_1 => x_1 • x) g y = x)) → motive x

Equations

• IsAddCyclic.card_pow_eq_one_le.match_1 g x motive x h_1 = Exists.casesOn x fun w h => h_1 w h

theorem IsAddCyclic.card_pow_eq_one_le {α : Type u} [AddGroup α] [DecidableEq α] [Fintype α] [IsAddCyclic α] {n : ℕ} (hn0 : 0 < n) : Finset.card (Finset.filter (fun a => n • a = 0) Finset.univ) ≤ n

abbrev IsAddCyclic.card_pow_eq_one_le.match_2 {α : Type u_1} [Fintype α] {n : ℕ} (motive : Nat.gcd n (Fintype.card α) ∣ Fintype.card α → Prop) : (x : Nat.gcd n (Fintype.card α) ∣ Fintype.card α) → ((m : ℕ) → (hm : Fintype.card α = Nat.gcd n (Fintype.card α) * m) → motive (_ : ∃ c, Fintype.card α = Nat.gcd n (Fintype.card α) * c)) → motive x

Equations

• IsAddCyclic.card_pow_eq_one_le.match_2 motive x h_1 = Exists.casesOn x fun w h => h_1 w h

theorem IsCyclic.card_pow_eq_one_le {α : Type u} [Group α] [DecidableEq α] [Fintype α] [IsCyclic α] {n : ℕ} (hn0 : 0 < n) : Finset.card (Finset.filter (fun a => a ^ n = 1) Finset.univ) ≤ n

theorem IsAddCyclic.exists_addMonoid_generator {α : Type u} [AddGroup α] [Finite α] [IsAddCyclic α] : ∃ x, ∀ (y : α), y ∈ AddSubmonoid.multiples x

theorem IsCyclic.exists_monoid_generator {α : Type u} [Group α] [Finite α] [IsCyclic α] : ∃ x, ∀ (y : α), y ∈ Submonoid.powers x

theorem IsAddCyclic.image_range_addOrderOf {α : Type u} {a : α} [AddGroup α] [DecidableEq α] [Fintype α] (ha : ∀ (x : α), x ∈ AddSubgroup.zmultiples a) : Finset.image (fun i => i • a) (Finset.range (addOrderOf a)) = Finset.univ

theorem IsCyclic.image_range_orderOf {α : Type u} {a : α} [Group α] [DecidableEq α] [Fintype α] (ha : ∀ (x : α), x ∈ Subgroup.zpowers a) : Finset.image (fun i => a ^ i) (Finset.range (orderOf a)) = Finset.univ

theorem IsAddCyclic.image_range_card {α : Type u} {a : α} [AddGroup α] [DecidableEq α] [Fintype α] (ha : ∀ (x : α), x ∈ AddSubgroup.zmultiples a) : Finset.image (fun i => i • a) (Finset.range (Fintype.card α)) = Finset.univ

theorem IsCyclic.image_range_card {α : Type u} {a : α} [Group α] [DecidableEq α] [Fintype α] (ha : ∀ (x : α), x ∈ Subgroup.zpowers a) : Finset.image (fun i => a ^ i) (Finset.range (Fintype.card α)) = Finset.univ

theorem card_orderOf_eq_totient_aux₂ {α : Type u} [Group α] [DecidableEq α] [Fintype α] (hn : ∀ (n : ℕ), 0 < n → Finset.card (Finset.filter (fun a => a ^ n = 1) Finset.univ) ≤ n) {d : ℕ} (hd : d ∣ Fintype.card α) : Finset.card (Finset.filter (fun a => orderOf a = d) Finset.univ) = Nat.totient d

theorem isCyclic_of_card_pow_eq_one_le {α : Type u} [Group α] [DecidableEq α] [Fintype α] (hn : ∀ (n : ℕ), 0 < n → Finset.card (Finset.filter (fun a => a ^ n = 1) Finset.univ) ≤ n) : IsCyclic α

theorem isAddCyclic_of_card_pow_eq_one_le {α : Type u_1} [AddGroup α] [DecidableEq α] [Fintype α] (hn : ∀ (n : ℕ), 0 < n → Finset.card (Finset.filter (fun a => n • a = 0) Finset.univ) ≤ n) : IsAddCyclic α

theorem IsCyclic.card_orderOf_eq_totient {α : Type u} [Group α] [IsCyclic α] [Fintype α] {d : ℕ} (hd : d ∣ Fintype.card α) : Finset.card (Finset.filter (fun a => orderOf a = d) Finset.univ) = Nat.totient d

theorem IsAddCyclic.card_orderOf_eq_totient {α : Type u_1} [AddGroup α] [IsAddCyclic α] [Fintype α] {d : ℕ} (hd : d ∣ Fintype.card α) : Finset.card (Finset.filter (fun a => addOrderOf a = d) Finset.univ) = Nat.totient d

theorem isSimpleAddGroup_of_prime_card {α : Type u} [AddGroup α] [Fintype α] {p : ℕ} [hp : Fact (Nat.Prime p)] (h : Fintype.card α = p) : IsSimpleAddGroup α

A finite group of prime order is simple.

theorem isSimpleGroup_of_prime_card {α : Type u} [Group α] [Fintype α] {p : ℕ} [hp : Fact (Nat.Prime p)] (h : Fintype.card α = p) : IsSimpleGroup α

A finite group of prime order is simple.

abbrev commutative_of_add_cyclic_center_quotient.match_2 {G : Type u_2} {H : Type u_1} [AddGroup G] [AddGroup H] (f : G →+ H) (motive : (∃ g, ∀ (x : { x // x ∈ AddMonoidHom.range f }), x ∈ AddSubgroup.zmultiples g) → Prop) : (x : ∃ g, ∀ (x : { x // x ∈ AddMonoidHom.range f }), x ∈ AddSubgroup.zmultiples g) → ((x : H) → (y : G) → (hxy : ↑f y = x) → (hx : ∀ (a : { x // x ∈ AddMonoidHom.range f }), a ∈ AddSubgroup.zmultiples { val := x, property := (_ : ∃ y, ↑f y = x) }) → motive (_ : ∃ g, ∀ (x : { x // x ∈ AddMonoidHom.range f }), x ∈ AddSubgroup.zmultiples g)) → motive x

Equations

• One or more equations did not get rendered due to their size.

abbrev commutative_of_add_cyclic_center_quotient.match_1 {G : Type u_2} {H : Type u_1} [AddGroup G] [AddGroup H] (f : G →+ H) (b : G) (x : H) (y : G) (hxy : ↑f y = x) (motive : { val := ↑f b, property := (_ : ∃ y, ↑f y = ↑f b) } ∈ AddSubgroup.zmultiples { val := x, property := (_ : ∃ y, ↑f y = x) } → Prop) : (x : { val := ↑f b, property := (_ : ∃ y, ↑f y = ↑f b) } ∈ AddSubgroup.zmultiples { val := x, property := (_ : ∃ y, ↑f y = x) }) → ((n : ℤ) → (hn : (fun x x_1 => x_1 • x) { val := x, property := (_ : ∃ y, ↑f y = x) } n = { val := ↑f b, property := (_ : ∃ y, ↑f y = ↑f b) }) → motive (_ : ∃ y, (fun x x_1 => x_1 • x) { val := x, property := (_ : ∃ y, ↑f y = x) } y = { val := ↑f b, property := (_ : ∃ y, ↑f y = ↑f b) })) → motive x

Equations

• commutative_of_add_cyclic_center_quotient.match_1 f b x y hxy motive x h_1 = Exists.casesOn x fun w h => h_1 w h

theorem commutative_of_add_cyclic_center_quotient {G : Type u_1} {H : Type u_2} [AddGroup G] [AddGroup H] [IsAddCyclic H] (f : G →+ H) (hf : AddMonoidHom.ker f ≤ AddSubgroup.center G) (a : G) (b : G) : a + b = b + a

A group is commutative if the quotient by the center is cyclic. Also see addCommGroup_of_cycle_center_quotient for the AddCommGroup instance.

theorem commutative_of_cyclic_center_quotient {G : Type u_1} {H : Type u_2} [Group G] [Group H] [IsCyclic H] (f : G →* H) (hf : MonoidHom.ker f ≤ Subgroup.center G) (a : G) (b : G) : a * b = b * a

A group is commutative if the quotient by the center is cyclic. Also see commGroup_of_cycle_center_quotient for the CommGroup instance.

def commutativeOfAddCycleCenterQuotient {G : Type u_1} {H : Type u_2} [AddGroup G] [AddGroup H] [IsAddCyclic H] (f : G →+ H) (hf : AddMonoidHom.ker f ≤ AddSubgroup.center G) : AddCommGroup G

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

Equations

• commutativeOfAddCycleCenterQuotient f hf = let src := let_fun this := inferInstance; this; AddCommGroup.mk (_ : ∀ (a b : G), a + b = b + a)

def commGroupOfCycleCenterQuotient {G : Type u_1} {H : Type u_2} [Group G] [Group H] [IsCyclic H] (f : G →* H) (hf : MonoidHom.ker f ≤ Subgroup.center G) : CommGroup G

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

Equations

• commGroupOfCycleCenterQuotient f hf = let src := let_fun this := inferInstance; this; CommGroup.mk (_ : ∀ (a b : G), a * b = b * a)

instance IsSimpleAddGroup.isAddCyclic {α : Type u} [AddCommGroup α] [IsSimpleAddGroup α] : IsAddCyclic α

Equations

• @IsSimpleAddGroup.isAddCyclic = @IsSimpleAddGroup.isAddCyclic.proof_1

theorem IsSimpleAddGroup.isAddCyclic.proof_1 {α : Type u_1} [AddCommGroup α] [IsSimpleAddGroup α] : IsAddCyclic α

instance IsSimpleGroup.isCyclic {α : Type u} [CommGroup α] [IsSimpleGroup α] : IsCyclic α

Equations

• @IsSimpleGroup.isCyclic = @IsSimpleGroup.isCyclic.proof_1

theorem IsSimpleAddGroup.prime_card {α : Type u} [AddCommGroup α] [IsSimpleAddGroup α] [Fintype α] : Nat.Prime (Fintype.card α)

theorem IsSimpleGroup.prime_card {α : Type u} [CommGroup α] [IsSimpleGroup α] [Fintype α] : Nat.Prime (Fintype.card α)

theorem AddCommGroup.is_simple_iff_isAddCyclic_and_prime_card {α : Type u} [Fintype α] [AddCommGroup α] : IsSimpleAddGroup α ↔ IsAddCyclic α ∧ Nat.Prime (Fintype.card α)

theorem CommGroup.is_simple_iff_isCyclic_and_prime_card {α : Type u} [Fintype α] [CommGroup α] : IsSimpleGroup α ↔ IsCyclic α ∧ Nat.Prime (Fintype.card α)

theorem IsAddCyclic.exponent_eq_card {α : Type u} [AddGroup α] [IsAddCyclic α] [Fintype α] : AddMonoid.exponent α = Fintype.card α

theorem IsCyclic.exponent_eq_card {α : Type u} [Group α] [IsCyclic α] [Fintype α] : Monoid.exponent α = Fintype.card α

theorem IsAddCyclic.of_exponent_eq_card {α : Type u} [AddCommGroup α] [Fintype α] (h : AddMonoid.exponent α = Fintype.card α) : IsAddCyclic α

abbrev IsAddCyclic.of_exponent_eq_card.match_1 {α : Type u_1} [AddCommGroup α] [Fintype α] (motive : (∃ a, a ∈ Finset.univ ∧ addOrderOf a = Finset.max' (Finset.image (fun g => addOrderOf g) Finset.univ) (_ : ∃ x, x ∈ Finset.image addOrderOf Finset.univ)) → Prop) : (x : ∃ a, a ∈ Finset.univ ∧ addOrderOf a = Finset.max' (Finset.image (fun g => addOrderOf g) Finset.univ) (_ : ∃ x, x ∈ Finset.image addOrderOf Finset.univ)) → ((g : α) → (left : g ∈ Finset.univ) → (hg : addOrderOf g = Finset.max' (Finset.image (fun g => addOrderOf g) Finset.univ) (_ : ∃ x, x ∈ Finset.image addOrderOf Finset.univ)) → motive (_ : ∃ a, a ∈ Finset.univ ∧ addOrderOf a = Finset.max' (Finset.image (fun g => addOrderOf g) Finset.univ) (_ : ∃ x, x ∈ Finset.image addOrderOf Finset.univ))) → motive x

Equations

• IsAddCyclic.of_exponent_eq_card.match_1 motive x h_1 = Exists.casesOn x fun w h => And.casesOn h fun left right => h_1 w left right

theorem IsCyclic.of_exponent_eq_card {α : Type u} [CommGroup α] [Fintype α] (h : Monoid.exponent α = Fintype.card α) : IsCyclic α

theorem IsAddCyclic.iff_exponent_eq_card {α : Type u} [AddCommGroup α] [Fintype α] : IsAddCyclic α ↔ AddMonoid.exponent α = Fintype.card α

theorem IsCyclic.iff_exponent_eq_card {α : Type u} [CommGroup α] [Fintype α] : IsCyclic α ↔ Monoid.exponent α = Fintype.card α

theorem IsAddCyclic.exponent_eq_zero_of_infinite {α : Type u} [AddGroup α] [IsAddCyclic α] [Infinite α] : AddMonoid.exponent α = 0

theorem IsCyclic.exponent_eq_zero_of_infinite {α : Type u} [Group α] [IsCyclic α] [Infinite α] : Monoid.exponent α = 0