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_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 = ⊤
@[instance 100]
@[instance 100]
@[simp]
theorem
isCyclic_multiplicative_iff
{α : Type u_1}
[AddGroup α]
:
IsCyclic (Multiplicative α) ↔ IsAddCyclic α
@[simp]
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
isAddCyclic_iff_exists_addOrderOf_eq_natCard
{α : Type u_1}
[AddGroup α]
[Finite α]
:
IsAddCyclic α ↔ ∃ (g : α), addOrderOf g = Nat.card α
@[deprecated isAddCyclic_iff_exists_addOrderOf_eq_natCard]
theorem
isAddCyclic_iff_exists_ofOrder_eq_natCard
{α : Type u_1}
[AddGroup α]
[Finite α]
:
IsAddCyclic α ↔ ∃ (g : α), addOrderOf g = Nat.card α
@[deprecated isAddCyclic_iff_exists_addOrderOf_eq_natCard]
theorem
IsAddCyclic.iff_exists_ofOrder_eq_natCard_of_Fintype
{α : Type u_1}
[AddGroup α]
[Finite α]
:
IsAddCyclic α ↔ ∃ (g : α), addOrderOf g = Nat.card α
theorem
isAddCyclic_of_addOrderOf_eq_card
{α : Type u_1}
[AddGroup α]
[Finite α]
(x : α)
(hx : addOrderOf x = Nat.card α)
:
@[deprecated isAddCyclic_of_addOrderOf_eq_card]
theorem
isAddCyclic_of_orderOf_eq_card
{α : Type u_1}
[AddGroup α]
[Finite α]
(x : α)
(hx : addOrderOf x = Nat.card α)
:
Alias of isAddCyclic_of_addOrderOf_eq_card.
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)
:
IsCyclic G
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)
:
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]
theorem
orderOf_generator_eq_natCard
{α : Type u_1}
[Group α]
{g : α}
(hx : ∀ (x : α), x ∈ Subgroup.zpowers g)
:
Alias of orderOf_eq_card_of_forall_mem_zpowers.
@[deprecated addOrderOf_eq_card_of_forall_mem_zmultiples]
theorem
addOrderOf_generator_eq_natCard
{α : Type u_1}
[AddGroup α]
{g : α}
(hx : ∀ (x : α), x ∈ AddSubgroup.zmultiples g)
:
addOrderOf g = Nat.card α
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
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)
:
IsCyclic G
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
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)
:
(Finset.filter (fun (a : α) => a ^ n = 1) Finset.univ).card ≤ n
theorem
IsAddCyclic.card_nsmul_eq_zero_le
{α : Type u_1}
[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_1}
[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_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
IsAddCyclic.exists_ofOrder_eq_natCard
{α : Type u_1}
[AddGroup α]
[h : IsAddCyclic α]
:
∃ (g : α), addOrderOf g = Nat.card α
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
card_orderOf_eq_totient_aux₂
{α : Type u_1}
[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_1}
[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_1}
[Group α]
[DecidableEq α]
[Fintype α]
(hn : ∀ (n : ℕ), 0 < n → (Finset.filter (fun (a : α) => a ^ n = 1) Finset.univ).card ≤ n)
:
IsCyclic α
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 → (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_1}
[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_1}
[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_1}
[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_1}
[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
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 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 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_2}
{G' : Type u_3}
[AddGroup G]
[AddGroup G']
[IsAddCyclic G']
(f : G →+ G')
(hf : f.ker ≤ AddSubgroup.center G)
(a 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_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
Instances For
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
Instances For
@[instance 100]
@[instance 100]
theorem
IsSimpleAddGroup.prime_card
{α : Type u_1}
[AddCommGroup α]
[IsSimpleAddGroup α]
[Finite α]
:
theorem
AddCommGroup.is_simple_iff_isAddCyclic_and_prime_card
{α : Type u_1}
[Finite α]
[AddCommGroup α]
:
IsSimpleAddGroup α ↔ IsAddCyclic α ∧ Nat.Prime (Nat.card α)
theorem
IsCyclic.exponent_eq_card
{α : Type u_1}
[Group α]
[IsCyclic α]
:
Monoid.exponent α = Nat.card α
theorem
IsCyclic.of_exponent_eq_card
{α : Type u_1}
[CommGroup α]
[Finite α]
(h : Monoid.exponent α = Nat.card α)
:
IsCyclic α
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
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.
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_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 ⋯)
Instances For
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)
Instances For
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)
Instances For
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))
Instances For
@[simp]
theorem
IsCyclic.val_inv_mulAutMulEquiv_apply
(G : Type u_2)
[Group G]
[h : IsCyclic G]
(a✝ : MulAut G)
:
↑((IsCyclic.mulAutMulEquiv G) a✝)⁻¹ = ((MulAutMultiplicative (ZMod (Nat.card G)))
((zmodCyclicMulEquiv h).trans (MulEquiv.trans a✝ (zmodCyclicMulEquiv h).symm)))⁻¹
1
@[simp]
theorem
IsCyclic.val_mulAutMulEquiv_apply
(G : Type u_2)
[Group G]
[h : IsCyclic G]
(a✝ : MulAut G)
:
↑((IsCyclic.mulAutMulEquiv G) a✝) = Multiplicative.toAdd ((zmodCyclicMulEquiv h).symm (a✝ ((zmodCyclicMulEquiv h) (Multiplicative.ofAdd 1))))
@[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 ((IsCyclic.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)
:
((IsCyclic.mulAutMulEquiv G).symm a✝) a✝¹ = (zmodCyclicMulEquiv h) (Multiplicative.ofAdd (a✝ • Multiplicative.toAdd ((zmodCyclicMulEquiv h).symm a✝¹)))
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' := ⋯ }
Instances For
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' := ⋯ }
Instances For
@[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
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')
:
Two homomorphisms 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' ⋯) ⋯ ⋯
Instances For
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' ⋯) ⋯ ⋯
Instances For
@[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