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 #
IsCyclicis a predicate on a group stating that the group is cyclic.
Main statements #
isCyclic_of_prime_cardproves that a finite group of prime order is cyclic.isSimpleGroup_of_prime_card,IsSimpleGroup.isCyclic, andIsSimpleGroup.prime_cardclassify finite simple abelian groups.IsCyclic.exponent_eq_card: For a finite cyclic groupG, 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}
[Group α]
[IsCyclic α]
:
∃ (g : α), ∀ (x : α), x ∈ Subgroup.zpowers g
theorem
IsAddCyclic.exists_generator
{α : Type u}
[AddGroup α]
[IsAddCyclic α]
:
∃ (g : α), ∀ (x : α), x ∈ AddSubgroup.zmultiples g
@[instance 100]
Equations
- ⋯ = ⋯
@[instance 100]
Equations
- ⋯ = ⋯
@[simp]
theorem
isCyclic_multiplicative_iff
{α : Type u}
[AddGroup α]
:
IsCyclic (Multiplicative α) ↔ IsAddCyclic α
Equations
- ⋯ = ⋯
@[simp]
Equations
- ⋯ = ⋯
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 ⋯
Instances For
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 ⋯
Instances For
A non-cyclic multiplicative group is non-trivial.
A non-cyclic additive group is non-trivial.
@[deprecated AddMonoidHom.map_addCyclic]
Alias of AddMonoidHom.map_addCyclic.
theorem
isCyclic_of_orderOf_eq_card
{α : Type u}
[Group α]
[Fintype α]
(x : α)
(hx : orderOf x = Fintype.card α)
:
IsCyclic α
theorem
isAddCyclic_of_addOrderOf_eq_card
{α : Type u}
[AddGroup α]
[Fintype α]
(x : α)
(hx : addOrderOf x = Fintype.card α)
:
@[deprecated isAddCyclic_of_addOrderOf_eq_card]
theorem
isAddCyclic_of_orderOf_eq_card
{α : Type u}
[AddGroup α]
[Fintype α]
(x : α)
(hx : addOrderOf x = Fintype.card α)
:
Alias of isAddCyclic_of_addOrderOf_eq_card.
theorem
AddSubgroup.eq_bot_or_eq_top_of_prime_card
{G : Type u_1}
[AddGroup G]
:
∀ {x : Fintype G} (H : AddSubgroup G) [hp : Fact (Nat.Prime (Fintype.card G))], H = ⊥ ∨ H = ⊤
theorem
zpowers_eq_top_of_prime_card
{G : Type u_1}
[Group G]
:
∀ {x : Fintype G} {p : ℕ} [hp : Fact (Nat.Prime p)], Fintype.card G = p → ∀ {g : G}, 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_1}
[AddGroup G]
:
∀ {x : Fintype G} {p : ℕ} [hp : Fact (Nat.Prime p)],
Fintype.card G = p → ∀ {g : G}, 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_1}
[Group G]
:
∀ {x : Fintype G} {p : ℕ} [hp : Fact (Nat.Prime p)], Fintype.card G = p → ∀ {g g' : G}, g ≠ 1 → g' ∈ Subgroup.zpowers g
theorem
mem_zmultiples_of_prime_card
{G : Type u_1}
[AddGroup G]
:
∀ {x : Fintype G} {p : ℕ} [hp : Fact (Nat.Prime p)],
Fintype.card G = p → ∀ {g g' : G}, g ≠ 0 → g' ∈ AddSubgroup.zmultiples g
theorem
mem_powers_of_prime_card
{G : Type u_1}
[Group G]
:
∀ {x : Fintype G} {p : ℕ} [hp : Fact (Nat.Prime p)], Fintype.card G = p → ∀ {g g' : G}, g ≠ 1 → g' ∈ Submonoid.powers g
theorem
mem_multiples_of_prime_card
{G : Type u_1}
[AddGroup G]
:
∀ {x : Fintype G} {p : ℕ} [hp : Fact (Nat.Prime p)],
Fintype.card G = p → ∀ {g g' : G}, g ≠ 0 → g' ∈ AddSubmonoid.multiples g
theorem
powers_eq_top_of_prime_card
{G : Type u_1}
[Group G]
:
∀ {x : Fintype G} {p : ℕ} [hp : Fact (Nat.Prime p)], Fintype.card G = p → ∀ {g : G}, g ≠ 1 → Submonoid.powers g = ⊤
theorem
multiples_eq_top_of_prime_card
{G : Type u_1}
[AddGroup G]
:
∀ {x : Fintype G} {p : ℕ} [hp : Fact (Nat.Prime p)],
Fintype.card G = p → ∀ {g : G}, g ≠ 0 → AddSubmonoid.multiples g = ⊤
theorem
isAddCyclic_of_prime_card
{α : Type u}
[AddGroup α]
[Fintype α]
{p : ℕ}
[hp : Fact (Nat.Prime p)]
(h : Fintype.card α = p)
:
A finite group of prime order is cyclic.
theorem
isCyclic_of_surjective
{H : Type u_1}
{G : Type u_2}
{F : Type u_3}
[Group H]
[Group G]
[hH : IsCyclic H]
[FunLike F H G]
[MonoidHomClass F H G]
(f : F)
(hf : Function.Surjective ⇑f)
:
IsCyclic G
theorem
isAddCyclic_of_surjective
{H : Type u_1}
{G : Type u_2}
{F : Type u_3}
[AddGroup H]
[AddGroup G]
[hH : IsAddCyclic H]
[FunLike F H G]
[AddMonoidHomClass F H G]
(f : F)
(hf : Function.Surjective ⇑f)
:
theorem
orderOf_eq_card_of_forall_mem_zpowers
{α : Type u}
[Group α]
[Fintype α]
{g : α}
(hx : ∀ (x : α), x ∈ Subgroup.zpowers g)
:
orderOf g = Fintype.card α
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_generator_eq_natCard
{α : Type u}
{a : α}
[Group α]
(h : ∀ (x : α), x ∈ Subgroup.zpowers a)
:
theorem
addOrderOf_generator_eq_natCard
{α : Type u}
{a : α}
[AddGroup α]
(h : ∀ (x : α), x ∈ AddSubgroup.zmultiples a)
:
addOrderOf a = Nat.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)
:
theorem
Infinite.orderOf_eq_zero_of_forall_mem_zpowers
{α : Type u}
[Group α]
[Infinite α]
{g : α}
(h : ∀ (x : α), x ∈ Subgroup.zpowers g)
:
theorem
Infinite.addOrderOf_eq_zero_of_forall_mem_zmultiples
{α : Type u}
[AddGroup α]
[Infinite α]
{g : α}
(h : ∀ (x : α), x ∈ AddSubgroup.zmultiples g)
:
addOrderOf g = 0
instance
AddSubgroup.isAddCyclic
{α : Type u}
[AddGroup α]
[IsAddCyclic α]
(H : AddSubgroup α)
:
IsAddCyclic ↥H
Equations
- ⋯ = ⋯
theorem
IsCyclic.card_pow_eq_one_le
{α : Type u}
[Group α]
[DecidableEq α]
[Fintype α]
[IsCyclic α]
{n : ℕ}
(hn0 : 0 < n)
:
(Finset.filter (fun (a : α) => a ^ n = 1) Finset.univ).card ≤ n
theorem
IsAddCyclic.card_nsmul_eq_zero_le
{α : Type u}
[AddGroup α]
[DecidableEq α]
[Fintype α]
[IsAddCyclic α]
{n : ℕ}
(hn0 : 0 < n)
:
(Finset.filter (fun (a : α) => n • a = 0) Finset.univ).card ≤ n
@[deprecated IsAddCyclic.card_nsmul_eq_zero_le]
theorem
IsAddCyclic.card_pow_eq_one_le
{α : Type u}
[AddGroup α]
[DecidableEq α]
[Fintype α]
[IsAddCyclic α]
{n : ℕ}
(hn0 : 0 < n)
:
(Finset.filter (fun (a : α) => n • a = 0) Finset.univ).card ≤ n
Alias of IsAddCyclic.card_nsmul_eq_zero_le.
theorem
IsCyclic.exists_monoid_generator
{α : Type u}
[Group α]
[Finite α]
[IsCyclic α]
:
∃ (x : α), ∀ (y : α), y ∈ Submonoid.powers x
theorem
IsAddCyclic.exists_addMonoid_generator
{α : Type u}
[AddGroup α]
[Finite α]
[IsAddCyclic α]
:
∃ (x : α), ∀ (y : α), y ∈ AddSubmonoid.multiples x
theorem
IsAddCyclic.exists_ofOrder_eq_natCard
{α : Type u}
[AddGroup α]
[h : IsAddCyclic α]
:
∃ (g : α), addOrderOf g = Nat.card α
theorem
isAddCyclic_iff_exists_ofOrder_eq_natCard
{α : Type u}
[AddGroup α]
[Finite α]
:
IsAddCyclic α ↔ ∃ (g : α), addOrderOf g = Nat.card α
@[deprecated]
theorem
IsAddCyclic.iff_exists_ofOrder_eq_natCard_of_Fintype
{α : Type u}
[AddGroup α]
[Finite α]
:
IsAddCyclic α ↔ ∃ (g : α), addOrderOf g = Nat.card α
theorem
IsCyclic.unique_zpow_zmod
{α : Type u}
{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}
{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}
{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}
{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}
{a : α}
[Group α]
[Fintype α]
[DecidableEq α]
(ha : ∀ (x : α), x ∈ Subgroup.zpowers a)
:
Finset.image (fun (i : ℕ) => a ^ i) (Finset.range (Fintype.card α)) = Finset.univ
theorem
IsAddCyclic.image_range_card
{α : Type u}
{a : α}
[AddGroup α]
[Fintype α]
[DecidableEq α]
(ha : ∀ (x : α), x ∈ AddSubgroup.zmultiples a)
:
Finset.image (fun (i : ℕ) => i • a) (Finset.range (Fintype.card α)) = Finset.univ
theorem
IsAddCyclic.ext
{G : Type u_1}
[AddGroup G]
[Fintype G]
[IsAddCyclic G]
{d : ℕ}
{a : ZMod d}
{b : ZMod d}
(hGcard : Fintype.card G = d)
(h : ∀ (t : G), a.val • t = b.val • t)
:
a = b
theorem
card_orderOf_eq_totient_aux₂
{α : Type u}
[Group α]
[DecidableEq α]
[Fintype α]
(hn : ∀ (n : ℕ), 0 < n → (Finset.filter (fun (a : α) => a ^ n = 1) Finset.univ).card ≤ n)
{d : ℕ}
(hd : d ∣ Fintype.card α)
:
(Finset.filter (fun (a : α) => orderOf a = d) Finset.univ).card = d.totient
theorem
card_addOrderOf_eq_totient_aux₂
{α : Type u}
[AddGroup α]
[DecidableEq α]
[Fintype α]
(hn : ∀ (n : ℕ), 0 < n → (Finset.filter (fun (a : α) => n • a = 0) Finset.univ).card ≤ n)
{d : ℕ}
(hd : d ∣ Fintype.card α)
:
(Finset.filter (fun (a : α) => addOrderOf a = d) Finset.univ).card = d.totient
theorem
isCyclic_of_card_pow_eq_one_le
{α : Type u}
[Group α]
[DecidableEq α]
[Fintype α]
(hn : ∀ (n : ℕ), 0 < n → (Finset.filter (fun (a : α) => a ^ n = 1) Finset.univ).card ≤ n)
:
IsCyclic α
theorem
isAddCyclic_of_card_nsmul_eq_zero_le
{α : Type u}
[AddGroup α]
[DecidableEq α]
[Fintype α]
(hn : ∀ (n : ℕ), 0 < n → (Finset.filter (fun (a : α) => n • a = 0) Finset.univ).card ≤ n)
:
@[deprecated isAddCyclic_of_card_nsmul_eq_zero_le]
theorem
isAddCyclic_of_card_pow_eq_one_le
{α : Type u}
[AddGroup α]
[DecidableEq α]
[Fintype α]
(hn : ∀ (n : ℕ), 0 < n → (Finset.filter (fun (a : α) => n • a = 0) Finset.univ).card ≤ n)
:
Alias of isAddCyclic_of_card_nsmul_eq_zero_le.
theorem
IsCyclic.card_orderOf_eq_totient
{α : Type u}
[Group α]
[IsCyclic α]
[Fintype α]
{d : ℕ}
(hd : d ∣ Fintype.card α)
:
(Finset.filter (fun (a : α) => orderOf a = d) Finset.univ).card = d.totient
theorem
IsAddCyclic.card_addOrderOf_eq_totient
{α : Type u}
[AddGroup α]
[IsAddCyclic α]
[Fintype α]
{d : ℕ}
(hd : d ∣ Fintype.card α)
:
(Finset.filter (fun (a : α) => addOrderOf a = d) Finset.univ).card = d.totient
@[deprecated IsAddCyclic.card_addOrderOf_eq_totient]
theorem
IsAddCyclic.card_orderOf_eq_totient
{α : Type u}
[AddGroup α]
[IsAddCyclic α]
[Fintype α]
{d : ℕ}
(hd : d ∣ Fintype.card α)
:
(Finset.filter (fun (a : α) => addOrderOf a = d) Finset.univ).card = d.totient
Alias of IsAddCyclic.card_addOrderOf_eq_totient.
theorem
isSimpleGroup_of_prime_card
{α : Type u}
[Group α]
[Fintype α]
{p : ℕ}
[hp : Fact (Nat.Prime p)]
(h : Fintype.card α = p)
:
A finite group of prime order is simple.
theorem
isSimpleAddGroup_of_prime_card
{α : Type u}
[AddGroup α]
[Fintype α]
{p : ℕ}
[hp : Fact (Nat.Prime p)]
(h : Fintype.card α = p)
:
A finite group of prime order is simple.
theorem
commutative_of_cyclic_center_quotient
{G : Type u_1}
{H : Type u_2}
[Group G]
[Group H]
[IsCyclic H]
(f : G →* H)
(hf : f.ker ≤ Subgroup.center G)
(a : G)
(b : G)
:
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_1}
{H : Type u_2}
[AddGroup G]
[AddGroup H]
[IsAddCyclic H]
(f : G →+ H)
(hf : f.ker ≤ AddSubgroup.center G)
(a : G)
(b : G)
:
A group is commutative if the quotient by the center is cyclic.
Also see addCommGroupOfCyclicCenterQuotient for the AddCommGroup instance.
@[deprecated commutative_of_addCyclic_center_quotient]
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 : f.ker ≤ AddSubgroup.center G)
(a : G)
(b : G)
:
Alias of commutative_of_addCyclic_center_quotient.
A group is commutative if the quotient by the center is cyclic.
Also see addCommGroupOfCyclicCenterQuotient for the AddCommGroup instance.
def
commGroupOfCyclicCenterQuotient
{G : Type u_1}
{H : Type u_2}
[Group G]
[Group H]
[IsCyclic H]
(f : G →* H)
(hf : f.ker ≤ Subgroup.center G)
:
A group is commutative if the quotient by the center is cyclic.
Equations
Instances For
def
addCommGroupOfAddCyclicCenterQuotient
{G : Type u_1}
{H : Type u_2}
[AddGroup G]
[AddGroup H]
[IsAddCyclic H]
(f : G →+ H)
(hf : f.ker ≤ AddSubgroup.center G)
:
A group is commutative if the quotient by the center is cyclic.
Equations
Instances For
@[instance 100]
Equations
- ⋯ = ⋯
@[instance 100]
Equations
- ⋯ = ⋯
theorem
IsSimpleAddGroup.prime_card
{α : Type u}
[AddCommGroup α]
[IsSimpleAddGroup α]
[Fintype α]
:
theorem
CommGroup.is_simple_iff_isCyclic_and_prime_card
{α : Type u}
[Fintype α]
[CommGroup α]
:
IsSimpleGroup α ↔ IsCyclic α ∧ Nat.Prime (Fintype.card α)
theorem
AddCommGroup.is_simple_iff_isAddCyclic_and_prime_card
{α : Type u}
[Fintype α]
[AddCommGroup α]
:
IsSimpleAddGroup α ↔ IsAddCyclic α ∧ Nat.Prime (Fintype.card α)
Equations
- ⋯ = ⋯
theorem
IsCyclic.of_exponent_eq_card
{α : Type u}
[CommGroup α]
[Fintype α]
(h : Monoid.exponent α = Fintype.card α)
:
IsCyclic α
theorem
IsAddCyclic.of_exponent_eq_card
{α : Type u}
[AddCommGroup α]
[Fintype α]
(h : AddMonoid.exponent α = Fintype.card α)
:
theorem
IsCyclic.iff_exponent_eq_card
{α : Type u}
[CommGroup α]
[Fintype α]
:
IsCyclic α ↔ Monoid.exponent α = Fintype.card α
theorem
IsCyclic.exponent_eq_zero_of_infinite
{α : Type u}
[Group α]
[IsCyclic α]
[Infinite α]
:
Monoid.exponent α = 0
theorem
IsAddCyclic.exponent_eq_zero_of_infinite
{α : Type u}
[AddGroup α]
[IsAddCyclic α]
[Infinite α]
:
AddMonoid.exponent α = 0
theorem
not_isAddCyclic_iff_exponent_eq_prime
{α : Type u}
[AddGroup α]
{p : ℕ}
(hp : Nat.Prime p)
(hα : Nat.card α = p ^ 2)
:
¬IsAddCyclic α ↔ AddMonoid.exponent α = p
theorem
zmultiplesHom_ker_eq
{G : Type u_1}
[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_1}
[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.
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.
Instances For
noncomputable def
zmodCyclicMulEquiv
{G : Type u_1}
[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 ⋯)
Instances For
noncomputable def
addEquivOfAddCyclicCardEq
{G : Type u_1}
{H : Type u_2}
[AddGroup G]
[AddGroup H]
[hG : IsAddCyclic G]
[hH : IsAddCyclic H]
(hcard : Nat.card G = Nat.card H)
:
G ≃+ H
Two cyclic additive groups of the same cardinality are isomorphic.
Equations
- addEquivOfAddCyclicCardEq hcard = (hcard ▸ zmodAddCyclicAddEquiv hG).symm.trans (zmodAddCyclicAddEquiv hH)
Instances For
noncomputable def
mulEquivOfCyclicCardEq
{G : Type u_1}
{H : Type u_2}
[Group G]
[Group H]
[hG : IsCyclic G]
[hH : IsCyclic H]
(hcard : Nat.card G = Nat.card H)
:
G ≃* H
Two cyclic groups of the same cardinality are isomorphic.
Equations
- mulEquivOfCyclicCardEq hcard = (hcard ▸ zmodCyclicMulEquiv hG).symm.trans (zmodCyclicMulEquiv hH)
Instances For
noncomputable def
mulEquivOfPrimeCardEq
{G : Type u_1}
{H : Type u_2}
{p : ℕ}
[Fintype G]
[Fintype H]
[Group G]
[Group H]
[Fact (Nat.Prime p)]
(hG : Fintype.card G = p)
(hH : Fintype.card H = p)
:
G ≃* H
Two groups of the same prime cardinality are isomorphic.
Equations
Instances For
noncomputable def
addEquivOfPrimeCardEq
{G : Type u_1}
{H : Type u_2}
{p : ℕ}
[Fintype G]
[Fintype H]
[AddGroup G]
[AddGroup H]
[Fact (Nat.Prime p)]
(hG : Fintype.card G = p)
(hH : Fintype.card H = p)
:
G ≃+ H
Two additive groups of the same prime cardinality are isomorphic.
Equations
Instances For
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_1}
{G' : Type u_2}
[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' := ⋯ }
Instances For
noncomputable def
addMonoidHomOfForallMemZmultiples
{G : Type u_1}
{G' : Type u_2}
[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' := ⋯ }
Instances For
@[simp]
theorem
monoidHomOfForallMemZpowers_apply_gen
{G : Type u_1}
{G' : Type u_2}
[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_1}
{G' : Type u_2}
[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
AddMonoidHom.eq_iff_eq_on_generator
{G : Type u_1}
{G' : Type u_2}
[AddGroup G]
[AddGroup G']
{g : G}
(hg : ∀ (x : G), x ∈ AddSubgroup.zmultiples g)
(f₁ : G →+ G')
(f₂ : G →+ G')
:
Two homomorphisms G →+ G' of additive groups are equal if and only if they agree
on a generator of G.
theorem
AddEquiv.eq_iff_eq_on_generator
{G : Type u_1}
{G' : Type u_2}
[AddGroup G]
[AddGroup G']
{g : G}
(hg : ∀ (x : G), x ∈ AddSubgroup.zmultiples g)
(f₁ : G ≃+ G')
(f₂ : G ≃+ 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_1}
{G' : Type u_2}
[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' ⋯) ⋯ ⋯
Instances For
noncomputable def
addEquivOfAddOrderOfEq
{G : Type u_1}
{G' : Type u_2}
[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' ⋯) ⋯ ⋯
Instances For
@[simp]
theorem
mulEquivOfOrderOfEq_apply_gen
{G : Type u_1}
{G' : Type u_2}
[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_1}
{G' : Type u_2}
[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_1}
{G' : Type u_2}
[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_1}
{G' : Type u_2}
[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_1}
{G' : Type u_2}
[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_1}
{G' : Type u_2}
[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