Documentation

Mathlib.GroupTheory.SpecificGroups.Cyclic

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

theorem IsCyclic.exists_generator {α : Type u_1} [Group α] [IsCyclic α] :

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

theorem IsAddCyclic.exists_generator {α : Type u_1} [AddGroup α] [IsAddCyclic α] :

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

theorem isCyclic_iff_exists_zpowers_eq_top {α : Type u_1} [Group α] :

IsCyclic α ↔ ∃ (g : α), Subgroup.zpowers g = ⊤

theorem isAddCyclic_iff_exists_zmultiples_eq_top {α : Type u_1} [AddGroup α] :

IsAddCyclic α ↔ ∃ (g : α), AddSubgroup.zmultiples g = ⊤

theorem Subgroup.isCyclic_iff_exists_zpowers_eq_top {α : Type u_1} [Group α] (H : Subgroup α) :

IsCyclic ↥H ↔ ∃ (g : α), zpowers g = H

theorem AddSubgroup.isAddCyclic_iff_exists_zmultiples_eq_top {α : Type u_1} [AddGroup α] (H : AddSubgroup α) :

IsAddCyclic ↥H ↔ ∃ (g : α), zmultiples g = H

@[instance 100]

instance isCyclic_of_subsingleton {α : Type u_1} [Group α] [Subsingleton α] :

@[instance 100]

instance isAddCyclic_of_subsingleton {α : Type u_1} [AddGroup α] [Subsingleton α] :

@[simp]

theorem isCyclic_multiplicative_iff {α : Type u_1} [SubNegMonoid α] :

IsCyclic (Multiplicative α) ↔ IsAddCyclic α

instance isCyclic_multiplicative {α : Type u_1} [AddGroup α] [IsAddCyclic α] :

IsCyclic (Multiplicative α)

@[simp]

theorem isAddCyclic_additive_iff {α : Type u_1} [DivInvMonoid α] :

IsAddCyclic (Additive α) ↔ IsCyclic α

instance isAddCyclic_additive {α : Type u_1} [Group α] [IsCyclic α] :

IsAddCyclic (Additive α)

instance IsCyclic.commutative {α : Type u_1} [Group α] [IsCyclic α] :

Std.Commutative fun (x1 x2 : α) => x1 * x2

instance IsAddCyclic.commutative {α : Type u_1} [AddGroup α] [IsAddCyclic α] :

Std.Commutative fun (x1 x2 : α) => x1 + x2

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

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

Equations

IsCyclic.commGroup = { toGroup := hg, mul_comm := ⋯ }

def IsAddCyclic.addCommGroup {α : Type u_1} [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 = { toAddGroup := hg, add_comm := ⋯ }

instance instIsMulCommutativeSubtypeMemSubgroupOfIsCyclic {G : Type u_2} [Group G] (H : Subgroup G) [IsCyclic ↥H] :

IsMulCommutative ↥H

theorem Nontrivial.of_not_isCyclic {α : Type u_1} [Group α] (nc : ¬IsCyclic α) :

A non-cyclic multiplicative group is non-trivial.

theorem Nontrivial.of_not_isAddCyclic {α : Type u_1} [AddGroup α] (nc : ¬IsAddCyclic α) :

A non-cyclic additive group is non-trivial.

theorem MonoidHom.map_cyclic {G : Type u_2} [Group G] [h : IsCyclic G] (σ : G →* G) :

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

theorem AddMonoidHom.map_addCyclic {G : Type u_2} [AddGroup G] [h : IsAddCyclic G] (σ : G →+ G) :

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

theorem isCyclic_iff_exists_orderOf_eq_natCard {α : Type u_1} [Group α] [Finite α] :

IsCyclic α ↔ ∃ (g : α), orderOf g = Nat.card α

theorem isAddCyclic_iff_exists_addOrderOf_eq_natCard {α : Type u_1} [AddGroup α] [Finite α] :

IsAddCyclic α ↔ ∃ (g : α), addOrderOf g = Nat.card α

theorem isCyclic_iff_exists_natCard_le_orderOf {α : Type u_1} [Group α] [Finite α] :

IsCyclic α ↔ ∃ (g : α), Nat.card α ≤ orderOf g

theorem isAddCyclic_iff_exists_natCard_le_addOrderOf {α : Type u_1} [AddGroup α] [Finite α] :

IsAddCyclic α ↔ ∃ (g : α), Nat.card α ≤ addOrderOf g

@[deprecated isCyclic_iff_exists_orderOf_eq_natCard (since := "2024-12-20")]

theorem isCyclic_iff_exists_ofOrder_eq_natCard {α : Type u_1} [Group α] [Finite α] :

IsCyclic α ↔ ∃ (g : α), orderOf g = Nat.card α

Alias of isCyclic_iff_exists_orderOf_eq_natCard.

@[deprecated isAddCyclic_iff_exists_addOrderOf_eq_natCard (since := "2024-12-20")]

theorem isAddCyclic_iff_exists_ofOrder_eq_natCard {α : Type u_1} [AddGroup α] [Finite α] :

IsAddCyclic α ↔ ∃ (g : α), addOrderOf g = Nat.card α

Alias of isAddCyclic_iff_exists_addOrderOf_eq_natCard.

@[deprecated isCyclic_iff_exists_orderOf_eq_natCard (since := "2024-12-20")]

theorem IsCyclic.iff_exists_ofOrder_eq_natCard_of_Fintype {α : Type u_1} [Group α] [Finite α] :

IsCyclic α ↔ ∃ (g : α), orderOf g = Nat.card α

Alias of isCyclic_iff_exists_orderOf_eq_natCard.

@[deprecated isAddCyclic_iff_exists_addOrderOf_eq_natCard (since := "2024-12-20")]

theorem IsAddCyclic.iff_exists_ofOrder_eq_natCard_of_Fintype {α : Type u_1} [AddGroup α] [Finite α] :

IsAddCyclic α ↔ ∃ (g : α), addOrderOf g = Nat.card α

Alias of isAddCyclic_iff_exists_addOrderOf_eq_natCard.

theorem isCyclic_of_orderOf_eq_card {α : Type u_1} [Group α] [Finite α] (x : α) (hx : orderOf x = Nat.card α) :

theorem isAddCyclic_of_addOrderOf_eq_card {α : Type u_1} [AddGroup α] [Finite α] (x : α) (hx : addOrderOf x = Nat.card α) :

theorem isCyclic_of_card_le_orderOf {α : Type u_1} [Group α] [Finite α] (x : α) (hx : Nat.card α ≤ orderOf x) :

theorem isAddCyclic_of_card_le_addOrderOf {α : Type u_1} [AddGroup α] [Finite α] (x : α) (hx : Nat.card α ≤ addOrderOf x) :

theorem Subgroup.eq_bot_or_eq_top_of_prime_card {G : Type u_2} [Group G] (H : Subgroup G) [hp : Fact (Nat.Prime (Nat.card G))] :

H = ⊥ ∨ H = ⊤

theorem AddSubgroup.eq_bot_or_eq_top_of_prime_card {G : Type u_2} [AddGroup G] (H : AddSubgroup G) [hp : Fact (Nat.Prime (Nat.card G))] :

H = ⊥ ∨ H = ⊤

theorem zpowers_eq_top_of_prime_card {G : Type u_2} [Group G] {p : ℕ} [hp : Fact (Nat.Prime p)] (h : Nat.card G = p) {g : G} (hg : g ≠ 1) :

Subgroup.zpowers g = ⊤

Any non-identity element of a finite group of prime order generates the group.

theorem zmultiples_eq_top_of_prime_card {G : Type u_2} [AddGroup G] {p : ℕ} [hp : Fact (Nat.Prime p)] (h : Nat.card G = p) {g : G} (hg : g ≠ 0) :

AddSubgroup.zmultiples g = ⊤

Any non-identity element of a finite group of prime order generates the group.

theorem mem_zpowers_of_prime_card {G : Type u_2} [Group G] {p : ℕ} [hp : Fact (Nat.Prime p)] (h : Nat.card G = p) {g g' : G} (hg : g ≠ 1) :

g' ∈ Subgroup.zpowers g

theorem mem_zmultiples_of_prime_card {G : Type u_2} [AddGroup G] {p : ℕ} [hp : Fact (Nat.Prime p)] (h : Nat.card G = p) {g g' : G} (hg : g ≠ 0) :

g' ∈ AddSubgroup.zmultiples g

theorem mem_powers_of_prime_card {G : Type u_2} [Group G] {p : ℕ} [hp : Fact (Nat.Prime p)] (h : Nat.card G = p) {g g' : G} (hg : g ≠ 1) :

g' ∈ Submonoid.powers g

theorem mem_multiples_of_prime_card {G : Type u_2} [AddGroup G] {p : ℕ} [hp : Fact (Nat.Prime p)] (h : Nat.card G = p) {g g' : G} (hg : g ≠ 0) :

g' ∈ AddSubmonoid.multiples g

theorem powers_eq_top_of_prime_card {G : Type u_2} [Group G] {p : ℕ} [hp : Fact (Nat.Prime p)] (h : Nat.card G = p) {g : G} (hg : g ≠ 1) :

Submonoid.powers g = ⊤

theorem multiples_eq_top_of_prime_card {G : Type u_2} [AddGroup G] {p : ℕ} [hp : Fact (Nat.Prime p)] (h : Nat.card G = p) {g : G} (hg : g ≠ 0) :

AddSubmonoid.multiples g = ⊤

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

A finite group of prime order is cyclic.

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

A finite group of prime order is cyclic.

theorem isCyclic_of_card_dvd_prime {α : Type u_1} [Group α] {p : ℕ} [hp : Fact (Nat.Prime p)] (h : Nat.card α ∣ p) :

A finite group of order dividing a prime is cyclic.

theorem isAddCyclic_of_card_dvd_prime {α : Type u_1} [AddGroup α] {p : ℕ} [hp : Fact (Nat.Prime p)] (h : Nat.card α ∣ p) :

A finite group of order dividing a prime is cyclic.

theorem isCyclic_of_surjective {G : Type u_2} {G' : Type u_3} [Group G] [Group G'] {F : Type u_4} [hH : IsCyclic G'] [FunLike F G' G] [MonoidHomClass F G' G] (f : F) (hf : Function.Surjective ⇑f) :

theorem isAddCyclic_of_surjective {G : Type u_2} {G' : Type u_3} [AddGroup G] [AddGroup G'] {F : Type u_4} [hH : IsAddCyclic G'] [FunLike F G' G] [AddMonoidHomClass F G' G] (f : F) (hf : Function.Surjective ⇑f) :

theorem orderOf_eq_card_of_forall_mem_zpowers {α : Type u_1} [Group α] {g : α} (hx : ∀ (x : α), x ∈ Subgroup.zpowers g) :

orderOf g = Nat.card α

theorem addOrderOf_eq_card_of_forall_mem_zmultiples {α : Type u_1} [AddGroup α] {g : α} (hx : ∀ (x : α), x ∈ AddSubgroup.zmultiples g) :

addOrderOf g = Nat.card α

@[deprecated orderOf_eq_card_of_forall_mem_zpowers (since := "2024-11-15")]

theorem orderOf_generator_eq_natCard {α : Type u_1} [Group α] {g : α} (hx : ∀ (x : α), x ∈ Subgroup.zpowers g) :

orderOf g = Nat.card α

Alias of orderOf_eq_card_of_forall_mem_zpowers.

@[deprecated addOrderOf_eq_card_of_forall_mem_zmultiples (since := "2024-11-15")]

theorem addOrderOf_generator_eq_natCard {α : Type u_1} [AddGroup α] {g : α} (hx : ∀ (x : α), x ∈ AddSubgroup.zmultiples g) :

addOrderOf g = Nat.card α

Alias of addOrderOf_eq_card_of_forall_mem_zmultiples.

theorem orderOf_eq_card_of_zpowers_eq_top {G : Type u_2} [Group G] {g : G} (h : Subgroup.zpowers g = ⊤) :

orderOf g = Nat.card G

theorem addOrderOf_eq_card_of_zmultiples_eq_top {G : Type u_2} [AddGroup G] {g : G} (h : AddSubgroup.zmultiples g = ⊤) :

addOrderOf g = Nat.card G

theorem exists_pow_ne_one_of_isCyclic {G : Type u_2} [Group G] [G_cyclic : IsCyclic G] {k : ℕ} (k_pos : k ≠ 0) (k_lt_card_G : k < Nat.card G) :

∃ (a : G), a ^ k ≠ 1

theorem exists_nsmul_ne_zero_of_isAddCyclic {G : Type u_2} [AddGroup G] [G_cyclic : IsAddCyclic G] {k : ℕ} (k_pos : k ≠ 0) (k_lt_card_G : k < Nat.card G) :

∃ (a : G), k • a ≠ 0

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

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

addOrderOf g = 0

instance Bot.isCyclic {α : Type u_1} [Group α] :

IsCyclic ↥⊥

instance Bot.isAddCyclic {α : Type u_1} [AddGroup α] :

IsAddCyclic ↥⊥

instance Subgroup.isCyclic {α : Type u_1} [Group α] [IsCyclic α] (H : Subgroup α) :

instance AddSubgroup.isAddCyclic {α : Type u_1} [AddGroup α] [IsAddCyclic α] (H : AddSubgroup α) :

IsAddCyclic ↥H

theorem isCyclic_of_injective {G : Type u_2} {G' : Type u_3} [Group G] [Group G'] [IsCyclic G'] (f : G →* G') (hf : Function.Injective ⇑f) :

theorem isAddCyclic_of_injective {G : Type u_2} {G' : Type u_3} [AddGroup G] [AddGroup G'] [IsAddCyclic G'] (f : G →+ G') (hf : Function.Injective ⇑f) :

theorem Subgroup.isCyclic_of_le {G : Type u_2} [Group G] {H H' : Subgroup G} (h : H ≤ H') [IsCyclic ↥H'] :

theorem AddSubgroup.isAddCyclic_of_le {G : Type u_2} [AddGroup G] {H H' : AddSubgroup G} (h : H ≤ H') [IsAddCyclic ↥H'] :

IsAddCyclic ↥H

theorem IsCyclic.card_pow_eq_one_le {α : Type u_1} [Group α] [DecidableEq α] [Fintype α] [IsCyclic α] {n : ℕ} (hn0 : 0 < n) :

{a : α | a ^ n = 1}.card ≤ n

theorem IsAddCyclic.card_nsmul_eq_zero_le {α : Type u_1} [AddGroup α] [DecidableEq α] [Fintype α] [IsAddCyclic α] {n : ℕ} (hn0 : 0 < n) :

{a : α | n • a = 0}.card ≤ n

theorem IsCyclic.exists_monoid_generator {α : Type u_1} [Group α] [Finite α] [IsCyclic α] :

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

theorem IsAddCyclic.exists_addMonoid_generator {α : Type u_1} [AddGroup α] [Finite α] [IsAddCyclic α] :

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

theorem IsCyclic.exists_ofOrder_eq_natCard {α : Type u_1} [Group α] [h : IsCyclic α] :

∃ (g : α), orderOf g = Nat.card α

theorem IsAddCyclic.exists_ofOrder_eq_natCard {α : Type u_1} [AddGroup α] [h : IsAddCyclic α] :

∃ (g : α), addOrderOf g = Nat.card α

noncomputable def MulDistribMulAction.toMonoidHomZModOfIsCyclic (G : Type u_2) [Group G] (M : Type u_4) [Monoid M] [IsCyclic G] [MulDistribMulAction M G] {n : ℕ} (hn : Nat.card G = n) :

A distributive action of a monoid on a finite cyclic group of order n factors through an action on ZMod n.

Equations

MulDistribMulAction.toMonoidHomZModOfIsCyclic G M hn = { toFun := fun (m : M) => ↑⋯.choose, map_one' := ⋯, map_mul' := ⋯ }

theorem MulDistribMulAction.toMonoidHomZModOfIsCyclic_apply {G : Type u_2} [Group G] {M : Type u_4} [Monoid M] [IsCyclic G] [MulDistribMulAction M G] {n : ℕ} (hn : Nat.card G = n) (m : M) (g : G) (k : ℤ) (h : (toMonoidHomZModOfIsCyclic G M hn) m = ↑k) :

m • g = g ^ k

theorem IsCyclic.unique_zpow_zmod {α : Type u_1} {a : α} [Group α] [Fintype α] (ha : ∀ (x : α), x ∈ Subgroup.zpowers a) (x : α) :

∃! n : ZMod (Fintype.card α), x = a ^ n.val

theorem IsAddCyclic.unique_zsmul_zmod {α : Type u_1} {a : α} [AddGroup α] [Fintype α] (ha : ∀ (x : α), x ∈ AddSubgroup.zmultiples a) (x : α) :

∃! n : ZMod (Fintype.card α), x = n.val • a

theorem IsCyclic.image_range_orderOf {α : Type u_1} {a : α} [Group α] [Fintype α] [DecidableEq α] (ha : ∀ (x : α), x ∈ Subgroup.zpowers a) :

Finset.image (fun (i : ℕ) => a ^ i) (Finset.range (orderOf a)) = Finset.univ

theorem IsAddCyclic.image_range_addOrderOf {α : Type u_1} {a : α} [AddGroup α] [Fintype α] [DecidableEq α] (ha : ∀ (x : α), x ∈ AddSubgroup.zmultiples a) :

Finset.image (fun (i : ℕ) => i • a) (Finset.range (addOrderOf a)) = Finset.univ

theorem IsCyclic.image_range_card {α : Type u_1} {a : α} [Group α] [Fintype α] [DecidableEq α] (ha : ∀ (x : α), x ∈ Subgroup.zpowers a) :

Finset.image (fun (i : ℕ) => a ^ i) (Finset.range (Nat.card α)) = Finset.univ

theorem IsAddCyclic.image_range_card {α : Type u_1} {a : α} [AddGroup α] [Fintype α] [DecidableEq α] (ha : ∀ (x : α), x ∈ AddSubgroup.zmultiples a) :

Finset.image (fun (i : ℕ) => i • a) (Finset.range (Nat.card α)) = Finset.univ

theorem IsCyclic.ext {G : Type u_2} [Group G] [Finite G] [IsCyclic G] {d : ℕ} {a b : ZMod d} (hGcard : Nat.card G = d) (h : ∀ (t : G), t ^ a.val = t ^ b.val) :

a = b

theorem IsAddCyclic.ext {G : Type u_2} [AddGroup G] [Finite G] [IsAddCyclic G] {d : ℕ} {a b : ZMod d} (hGcard : Nat.card G = d) (h : ∀ (t : G), a.val • t = b.val • t) :

a = b

theorem card_orderOf_eq_totient_aux₂ {α : Type u_1} [Group α] [DecidableEq α] [Fintype α] (hn : ∀ (n : ℕ), 0 < n → {a : α | a ^ n = 1}.card ≤ n) {d : ℕ} (hd : d ∣ Fintype.card α) :

{a : α | orderOf a = d}.card = d.totient

theorem card_addOrderOf_eq_totient_aux₂ {α : Type u_1} [AddGroup α] [DecidableEq α] [Fintype α] (hn : ∀ (n : ℕ), 0 < n → {a : α | n • a = 0}.card ≤ n) {d : ℕ} (hd : d ∣ Fintype.card α) :

{a : α | addOrderOf a = d}.card = d.totient

theorem isCyclic_of_card_pow_eq_one_le {α : Type u_1} [Group α] [DecidableEq α] [Fintype α] (hn : ∀ (n : ℕ), 0 < n → {a : α | a ^ n = 1}.card ≤ n) :

Stacks Tag 09HX (This theorem is stronger than 09HX. It removes the abelian condition, and requires only ≤ instead of =.)

theorem isAddCyclic_of_card_nsmul_eq_zero_le {α : Type u_1} [AddGroup α] [DecidableEq α] [Fintype α] (hn : ∀ (n : ℕ), 0 < n → {a : α | n • a = 0}.card ≤ n) :

theorem IsCyclic.card_orderOf_eq_totient {α : Type u_1} [Group α] [IsCyclic α] [Fintype α] {d : ℕ} (hd : d ∣ Fintype.card α) :

{a : α | orderOf a = d}.card = d.totient

theorem IsAddCyclic.card_addOrderOf_eq_totient {α : Type u_1} [AddGroup α] [IsAddCyclic α] [Fintype α] {d : ℕ} (hd : d ∣ Fintype.card α) :

{a : α | addOrderOf a = d}.card = d.totient

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

IsSimpleGroup α

A finite group of prime order is simple.

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

IsSimpleAddGroup α

A finite group of prime order is simple.

theorem commutative_of_cyclic_center_quotient {G : Type u_2} {G' : Type u_3} [Group G] [Group G'] [IsCyclic G'] (f : G →* G') (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 commGroupOfCyclicCenterQuotient for the CommGroup instance.

theorem commutative_of_addCyclic_center_quotient {G : Type u_2} {G' : Type u_3} [AddGroup G] [AddGroup G'] [IsAddCyclic G'] (f : G →+ G') (hf : f.ker ≤ AddSubgroup.center G) (a b : G) :

a + b = b + a

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

def commGroupOfCyclicCenterQuotient {G : Type u_2} {G' : Type u_3} [Group G] [Group G'] [IsCyclic G'] (f : G →* G') (hf : f.ker ≤ Subgroup.center G) :

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

Equations

commGroupOfCyclicCenterQuotient f hf = { toGroup := let_fun this := inferInstance; this, mul_comm := ⋯ }

def addCommGroupOfAddCyclicCenterQuotient {G : Type u_2} {G' : Type u_3} [AddGroup G] [AddGroup G'] [IsAddCyclic G'] (f : G →+ G') (hf : f.ker ≤ AddSubgroup.center G) :

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

Equations

addCommGroupOfAddCyclicCenterQuotient f hf = { toAddGroup := let_fun this := inferInstance; this, add_comm := ⋯ }

@[instance 100]

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

@[instance 100]

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

theorem IsSimpleGroup.prime_card {α : Type u_1} [CommGroup α] [IsSimpleGroup α] [Finite α] :

Nat.Prime (Nat.card α)

theorem IsSimpleAddGroup.prime_card {α : Type u_1} [AddCommGroup α] [IsSimpleAddGroup α] [Finite α] :

Nat.Prime (Nat.card α)

theorem CommGroup.is_simple_iff_isCyclic_and_prime_card {α : Type u_1} [Finite α] [CommGroup α] :

IsSimpleGroup α ↔ IsCyclic α ∧ Nat.Prime (Nat.card α)

theorem AddCommGroup.is_simple_iff_isAddCyclic_and_prime_card {α : Type u_1} [Finite α] [AddCommGroup α] :

IsSimpleAddGroup α ↔ IsAddCyclic α ∧ Nat.Prime (Nat.card α)

instance instIsAddCyclicInt :

IsAddCyclic ℤ

instance ZMod.instIsAddCyclic (n : ℕ) :

IsAddCyclic (ZMod n)

instance ZMod.instIsSimpleAddGroup {p : ℕ} [Fact (Nat.Prime p)] :

IsSimpleAddGroup (ZMod p)

theorem IsCyclic.exponent_eq_card {α : Type u_1} [Group α] [IsCyclic α] :

Monoid.exponent α = Nat.card α

theorem IsAddCyclic.exponent_eq_card {α : Type u_1} [AddGroup α] [IsAddCyclic α] :

AddMonoid.exponent α = Nat.card α

theorem IsCyclic.of_exponent_eq_card {α : Type u_1} [CommGroup α] [Finite α] (h : Monoid.exponent α = Nat.card α) :

theorem IsAddCyclic.of_exponent_eq_card {α : Type u_1} [AddCommGroup α] [Finite α] (h : AddMonoid.exponent α = Nat.card α) :

theorem IsCyclic.iff_exponent_eq_card {α : Type u_1} [CommGroup α] [Finite α] :

IsCyclic α ↔ Monoid.exponent α = Nat.card α

theorem IsAddCyclic.iff_exponent_eq_card {α : Type u_1} [AddCommGroup α] [Finite α] :

IsAddCyclic α ↔ AddMonoid.exponent α = Nat.card α

theorem IsCyclic.exponent_eq_zero_of_infinite {α : Type u_1} [Group α] [IsCyclic α] [Infinite α] :

Monoid.exponent α = 0

theorem IsAddCyclic.exponent_eq_zero_of_infinite {α : Type u_1} [AddGroup α] [IsAddCyclic α] [Infinite α] :

AddMonoid.exponent α = 0

@[simp]

theorem ZMod.exponent (n : ℕ) :

AddMonoid.exponent (ZMod n) = n

theorem not_isCyclic_iff_exponent_eq_prime {α : Type u_1} [Group α] {p : ℕ} (hp : Nat.Prime p) (hα : Nat.card α = p ^ 2) :

¬IsCyclic α ↔ Monoid.exponent α = p

A group of order p ^ 2 is not cyclic if and only if its exponent is p.

theorem not_isAddCyclic_iff_exponent_eq_prime {α : Type u_1} [AddGroup α] {p : ℕ} (hp : Nat.Prime p) (hα : Nat.card α = p ^ 2) :

¬IsAddCyclic α ↔ AddMonoid.exponent α = p

theorem zmultiplesHom_ker_eq {G : Type u_2} [AddGroup G] (g : G) :

((zmultiplesHom G) g).ker = AddSubgroup.zmultiples ↑(addOrderOf g)

The kernel of zmultiplesHom G g is equal to the additive subgroup generated by addOrderOf g.

theorem zpowersHom_ker_eq {G : Type u_2} [Group G] (g : G) :

((zpowersHom G) g).ker = Subgroup.zpowers (Multiplicative.ofAdd ↑(orderOf g))

The kernel of zpowersHom G g is equal to the subgroup generated by orderOf g.

noncomputable def zmodAddCyclicAddEquiv {G : Type u_2} [AddGroup G] (h : IsAddCyclic G) :

ZMod (Nat.card G) ≃+ G

The isomorphism from ZMod n to any cyclic additive group of Nat.card equal to n.

Equations

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

noncomputable def zmodCyclicMulEquiv {G : Type u_2} [Group G] (h : IsCyclic G) :

Multiplicative (ZMod (Nat.card G)) ≃* G

The isomorphism from Multiplicative (ZMod n) to any cyclic group of Nat.card equal to n.

Equations

zmodCyclicMulEquiv h = AddEquiv.toMultiplicative (zmodAddCyclicAddEquiv ⋯)

noncomputable def addEquivOfAddCyclicCardEq {G : Type u_2} {G' : Type u_3} [AddGroup G] [AddGroup G'] [hG : IsAddCyclic G] [hH : IsAddCyclic G'] (hcard : Nat.card G = Nat.card G') :

G ≃+ G'

Two cyclic additive groups of the same cardinality are isomorphic.

Equations

addEquivOfAddCyclicCardEq hcard = (hcard ▸ zmodAddCyclicAddEquiv hG).symm.trans (zmodAddCyclicAddEquiv hH)

noncomputable def mulEquivOfCyclicCardEq {G : Type u_2} {G' : Type u_3} [Group G] [Group G'] [hG : IsCyclic G] [hH : IsCyclic G'] (hcard : Nat.card G = Nat.card G') :

G ≃* G'

Two cyclic groups of the same cardinality are isomorphic.

Equations

mulEquivOfCyclicCardEq hcard = (hcard ▸ zmodCyclicMulEquiv hG).symm.trans (zmodCyclicMulEquiv hH)

noncomputable def mulEquivOfPrimeCardEq {G : Type u_2} {G' : Type u_3} {p : ℕ} [Group G] [Group G'] [Fact (Nat.Prime p)] (hG : Nat.card G = p) (hH : Nat.card G' = p) :

G ≃* G'

Two groups of the same prime cardinality are isomorphic.

Equations

mulEquivOfPrimeCardEq hG hH = mulEquivOfCyclicCardEq ⋯

noncomputable def addEquivOfPrimeCardEq {G : Type u_2} {G' : Type u_3} {p : ℕ} [AddGroup G] [AddGroup G'] [Fact (Nat.Prime p)] (hG : Nat.card G = p) (hH : Nat.card G' = p) :

G ≃+ G'

Two additive groups of the same prime cardinality are isomorphic.

Equations

addEquivOfPrimeCardEq hG hH = addEquivOfAddCyclicCardEq ⋯

noncomputable def IsCyclic.mulAutMulEquiv (G : Type u_2) [Group G] [h : IsCyclic G] :

MulAut G ≃* (ZMod (Nat.card G))ˣ

The automorphism group of a cyclic group is isomorphic to the multiplicative group of ZMod.

Equations

IsCyclic.mulAutMulEquiv G = ((MulAut.congr (zmodCyclicMulEquiv h)).symm.trans (MulAutMultiplicative (ZMod (Nat.card G)))).trans (ZMod.AddAutEquivUnits (Nat.card G))

@[simp]

theorem IsCyclic.mulAutMulEquiv_symm_apply_symm_apply (G : Type u_2) [Group G] [h : IsCyclic G] (a✝ : (ZMod (Nat.card G))ˣ) (a✝¹ : G) :

(MulEquiv.symm ((mulAutMulEquiv G).symm a✝)) a✝¹ = (zmodCyclicMulEquiv h) (Multiplicative.ofAdd (a✝⁻¹ • Multiplicative.toAdd ((zmodCyclicMulEquiv h).symm a✝¹)))

@[simp]

theorem IsCyclic.mulAutMulEquiv_symm_apply_apply (G : Type u_2) [Group G] [h : IsCyclic G] (a✝ : (ZMod (Nat.card G))ˣ) (a✝¹ : G) :

((mulAutMulEquiv G).symm a✝) a✝¹ = (zmodCyclicMulEquiv h) (Multiplicative.ofAdd (a✝ • Multiplicative.toAdd ((zmodCyclicMulEquiv h).symm a✝¹)))

@[simp]

theorem IsCyclic.val_mulAutMulEquiv_apply (G : Type u_2) [Group G] [h : IsCyclic G] (a✝ : MulAut G) :

↑((mulAutMulEquiv G) a✝) = Multiplicative.toAdd ((zmodCyclicMulEquiv h).symm (a✝ ((zmodCyclicMulEquiv h) (Multiplicative.ofAdd 1))))

@[simp]

theorem IsCyclic.val_inv_mulAutMulEquiv_apply (G : Type u_2) [Group G] [h : IsCyclic G] (a✝ : MulAut G) :

↑((mulAutMulEquiv G) a✝)⁻¹ = Multiplicative.toAdd ((zmodCyclicMulEquiv h).symm ((MulEquiv.symm a✝) ((zmodCyclicMulEquiv h) (Multiplicative.ofAdd 1))))

theorem IsCyclic.card_mulAut (G : Type u_2) [Group G] [Finite G] [h : IsCyclic G] :

Nat.card (MulAut G) = (Nat.card G).totient

theorem IsCyclic.card_powMonoidHom_range (G : Type u_2) [CommGroup G] [hG : IsCyclic G] [Finite G] (d : ℕ) :

Nat.card ↥(powMonoidHom d).range = Nat.card G / (Nat.card G).gcd d

theorem IsAddCyclic.card_nsmulAddMonoidHom_range (G : Type u_2) [AddCommGroup G] [hG : IsAddCyclic G] [Finite G] (d : ℕ) :

Nat.card ↥(nsmulAddMonoidHom d).range = Nat.card G / (Nat.card G).gcd d

theorem IsCyclic.index_powMonoidHom_ker (G : Type u_2) [CommGroup G] [IsCyclic G] [Finite G] (d : ℕ) :

(powMonoidHom d).ker.index = Nat.card G / (Nat.card G).gcd d

theorem IsAddCyclic.index_nsmulAddMonoidHom_ker (G : Type u_2) [AddCommGroup G] [IsAddCyclic G] [Finite G] (d : ℕ) :

(nsmulAddMonoidHom d).ker.index = Nat.card G / (Nat.card G).gcd d

theorem IsCyclic.card_powMonoidHom_ker (G : Type u_2) [CommGroup G] [IsCyclic G] [Finite G] (d : ℕ) :

Nat.card ↥(powMonoidHom d).ker = (Nat.card G).gcd d

theorem IsAddCyclic.card_nsmulAddMonoidHom_ker (G : Type u_2) [AddCommGroup G] [IsAddCyclic G] [Finite G] (d : ℕ) :

Nat.card ↥(nsmulAddMonoidHom d).ker = (Nat.card G).gcd d

theorem IsCyclic.index_powMonoidHom_range (G : Type u_2) [CommGroup G] [IsCyclic G] [Finite G] (d : ℕ) :

(powMonoidHom d).range.index = (Nat.card G).gcd d

theorem IsAddCyclic.index_nsmulAddMonoidHom_range (G : Type u_2) [AddCommGroup G] [IsAddCyclic G] [Finite G] (d : ℕ) :

(nsmulAddMonoidHom d).range.index = (Nat.card G).gcd d

Groups with a given generator #

We state some results in terms of an explicitly given generator. The generating property is given as in IsCyclic.exists_generator.

The main statements are about the existence and uniqueness of homomorphisms and isomorphisms specified by the image of the given generator.

noncomputable def monoidHomOfForallMemZpowers {G : Type u_2} {G' : Type u_3} [Group G] [Group G'] {g : G} (hg : ∀ (x : G), x ∈ Subgroup.zpowers g) {g' : G'} (hg' : orderOf g' ∣ orderOf g) :

G →* G'

If g generates the group G and g' is an element of another group G' whose order divides that of g, then there is a homomorphism G →* G' mapping g to g'.

Equations

monoidHomOfForallMemZpowers hg hg' = { toFun := fun (x : G) => g' ^ Classical.choose ⋯, map_one' := ⋯, map_mul' := ⋯ }

noncomputable def addMonoidHomOfForallMemZmultiples {G : Type u_2} {G' : Type u_3} [AddGroup G] [AddGroup G'] {g : G} (hg : ∀ (x : G), x ∈ AddSubgroup.zmultiples g) {g' : G'} (hg' : addOrderOf g' ∣ addOrderOf g) :

G →+ G'

If g generates the additive group G and g' is an element of another additive group G' whose order divides that of g, then there is a homomorphism G →+ G' mapping g to g'.

Equations

addMonoidHomOfForallMemZmultiples hg hg' = { toFun := fun (x : G) => Classical.choose ⋯ • g', map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem monoidHomOfForallMemZpowers_apply_gen {G : Type u_2} {G' : Type u_3} [Group G] [Group G'] {g : G} (hg : ∀ (x : G), x ∈ Subgroup.zpowers g) {g' : G'} (hg' : orderOf g' ∣ orderOf g) :

(monoidHomOfForallMemZpowers hg hg') g = g'

@[simp]

theorem addMonoidHomOfForallMemZmultiples_apply_gen {G : Type u_2} {G' : Type u_3} [AddGroup G] [AddGroup G'] {g : G} (hg : ∀ (x : G), x ∈ AddSubgroup.zmultiples g) {g' : G'} (hg' : addOrderOf g' ∣ addOrderOf g) :

(addMonoidHomOfForallMemZmultiples hg hg') g = g'

theorem MonoidHom.eq_iff_eq_on_generator {G : Type u_2} {G' : Type u_3} [Group G] [Group G'] {g : G} (hg : ∀ (x : G), x ∈ Subgroup.zpowers g) (f₁ f₂ : G →* G') :

f₁ = f₂ ↔ f₁ g = f₂ g

Two group homomorphisms G →* G' are equal if and only if they agree on a generator of G.

theorem AddMonoidHom.eq_iff_eq_on_generator {G : Type u_2} {G' : Type u_3} [AddGroup G] [AddGroup G'] {g : G} (hg : ∀ (x : G), x ∈ AddSubgroup.zmultiples g) (f₁ f₂ : G →+ G') :

f₁ = f₂ ↔ f₁ g = f₂ g

Two homomorphisms G →+ G' of additive groups are equal if and only if they agree on a generator of G.

theorem MulEquiv.eq_iff_eq_on_generator {G : Type u_2} {G' : Type u_3} [Group G] [Group G'] {g : G} (hg : ∀ (x : G), x ∈ Subgroup.zpowers g) (f₁ f₂ : G ≃* G') :

f₁ = f₂ ↔ f₁ g = f₂ g

Two group isomorphisms G ≃* G' are equal if and only if they agree on a generator of G.

theorem AddEquiv.eq_iff_eq_on_generator {G : Type u_2} {G' : Type u_3} [AddGroup G] [AddGroup G'] {g : G} (hg : ∀ (x : G), x ∈ AddSubgroup.zmultiples g) (f₁ f₂ : G ≃+ G') :

f₁ = f₂ ↔ f₁ g = f₂ g

Two isomorphisms G ≃+ G' of additive groups are equal if and only if they agree on a generator of G.

noncomputable def mulEquivOfOrderOfEq {G : Type u_2} {G' : Type u_3} [Group G] [Group G'] {g : G} (hg : ∀ (x : G), x ∈ Subgroup.zpowers g) {g' : G'} (hg' : ∀ (x : G'), x ∈ Subgroup.zpowers g') (h : orderOf g = orderOf g') :

G ≃* G'

Given two groups that are generated by elements g and g' of the same order, we obtain an isomorphism sending g to g'.

Equations

mulEquivOfOrderOfEq hg hg' h = (monoidHomOfForallMemZpowers hg ⋯).toMulEquiv (monoidHomOfForallMemZpowers hg' ⋯) ⋯ ⋯

noncomputable def addEquivOfAddOrderOfEq {G : Type u_2} {G' : Type u_3} [AddGroup G] [AddGroup G'] {g : G} (hg : ∀ (x : G), x ∈ AddSubgroup.zmultiples g) {g' : G'} (hg' : ∀ (x : G'), x ∈ AddSubgroup.zmultiples g') (h : addOrderOf g = addOrderOf g') :

G ≃+ G'

Given two additive groups that are generated by elements g and g' of the same order, we obtain an isomorphism sending g to g'.

Equations

addEquivOfAddOrderOfEq hg hg' h = (addMonoidHomOfForallMemZmultiples hg ⋯).toAddEquiv (addMonoidHomOfForallMemZmultiples hg' ⋯) ⋯ ⋯

@[simp]

theorem mulEquivOfOrderOfEq_apply_gen {G : Type u_2} {G' : Type u_3} [Group G] [Group G'] {g : G} (hg : ∀ (x : G), x ∈ Subgroup.zpowers g) {g' : G'} (hg' : ∀ (x : G'), x ∈ Subgroup.zpowers g') (h : orderOf g = orderOf g') :

(mulEquivOfOrderOfEq hg hg' h) g = g'

@[simp]

theorem addEquivOfAddOrderOfEq_apply_gen {G : Type u_2} {G' : Type u_3} [AddGroup G] [AddGroup G'] {g : G} (hg : ∀ (x : G), x ∈ AddSubgroup.zmultiples g) {g' : G'} (hg' : ∀ (x : G'), x ∈ AddSubgroup.zmultiples g') (h : addOrderOf g = addOrderOf g') :

(addEquivOfAddOrderOfEq hg hg' h) g = g'

@[simp]

theorem mulEquivOfOrderOfEq_symm {G : Type u_2} {G' : Type u_3} [Group G] [Group G'] {g : G} (hg : ∀ (x : G), x ∈ Subgroup.zpowers g) {g' : G'} (hg' : ∀ (x : G'), x ∈ Subgroup.zpowers g') (h : orderOf g = orderOf g') :

(mulEquivOfOrderOfEq hg hg' h).symm = mulEquivOfOrderOfEq hg' hg ⋯

@[simp]

theorem addEquivOfAddOrderOfEq_symm {G : Type u_2} {G' : Type u_3} [AddGroup G] [AddGroup G'] {g : G} (hg : ∀ (x : G), x ∈ AddSubgroup.zmultiples g) {g' : G'} (hg' : ∀ (x : G'), x ∈ AddSubgroup.zmultiples g') (h : addOrderOf g = addOrderOf g') :

(addEquivOfAddOrderOfEq hg hg' h).symm = addEquivOfAddOrderOfEq hg' hg ⋯

theorem mulEquivOfOrderOfEq_symm_apply_gen {G : Type u_2} {G' : Type u_3} [Group G] [Group G'] {g : G} (hg : ∀ (x : G), x ∈ Subgroup.zpowers g) {g' : G'} (hg' : ∀ (x : G'), x ∈ Subgroup.zpowers g') (h : orderOf g = orderOf g') :

(mulEquivOfOrderOfEq hg hg' h).symm g' = g

theorem addEquivOfAddOrderOfEq_symm_apply_gen {G : Type u_2} {G' : Type u_3} [AddGroup G] [AddGroup G'] {g : G} (hg : ∀ (x : G), x ∈ AddSubgroup.zmultiples g) {g' : G'} (hg' : ∀ (x : G'), x ∈ AddSubgroup.zmultiples g') (h : addOrderOf g = addOrderOf g') :

(addEquivOfAddOrderOfEq hg hg' h).symm g' = g