Documentation

Mathlib.Data.ZMod.QuotientGroup

ZMod n and quotient groups / rings #

This file relates ZMod n to the quotient group ℤ / AddSubgroup.zmultiples (n : ℤ).

Main definitions #

Tags #

zmod, quotient group

noncomputable def AddAction.zmultiplesQuotientStabilizerEquiv {α : Type u_3} {β : Type u_4} [AddGroup α] (a : α) [AddAction α β] (b : β) :

The quotient (ℤ ∙ a) ⧸ (stabilizer b) is cyclic of order minimalPeriod (a +ᵥ ·) b.

Equations
  • One or more equations did not get rendered due to their size.
theorem AddAction.zmultiplesQuotientStabilizerEquiv_symm_apply {α : Type u_3} {β : Type u_4} [AddGroup α] (a : α) [AddAction α β] (b : β) (n : ZMod (Function.minimalPeriod (fun (x : β) => a +ᵥ x) b)) :
noncomputable def MulAction.zpowersQuotientStabilizerEquiv {α : Type u_3} {β : Type u_4} [Group α] (a : α) [MulAction α β] (b : β) :

The quotient (a ^ ℤ) ⧸ (stabilizer b) is cyclic of order minimalPeriod ((•) a) b.

Equations
theorem MulAction.zpowersQuotientStabilizerEquiv_symm_apply {α : Type u_3} {β : Type u_4} [Group α] (a : α) [MulAction α β] (b : β) (n : ZMod (Function.minimalPeriod (fun (x : β) => a x) b)) :
noncomputable def MulAction.orbitZPowersEquiv {α : Type u_3} {β : Type u_4} [Group α] (a : α) [MulAction α β] (b : β) :
(orbit (↥(Subgroup.zpowers a)) b) ZMod (Function.minimalPeriod (fun (x : β) => a x) b)

The orbit (a ^ ℤ) • b is a cycle of order minimalPeriod ((•) a) b.

Equations
noncomputable def AddAction.orbitZMultiplesEquiv {α : Type u_5} {β : Type u_6} [AddGroup α] (a : α) [AddAction α β] (b : β) :
(orbit (↥(AddSubgroup.zmultiples a)) b) ZMod (Function.minimalPeriod (fun (x : β) => a +ᵥ x) b)

The orbit (ℤ • a) +ᵥ b is a cycle of order minimalPeriod (a +ᵥ ·) b.

Equations
theorem MulAction.orbitZPowersEquiv_symm_apply {α : Type u_3} {β : Type u_4} [Group α] (a : α) [MulAction α β] (b : β) (k : ZMod (Function.minimalPeriod (fun (x : β) => a x) b)) :
(orbitZPowersEquiv a b).symm k = a, ^ k.cast b,
theorem AddAction.orbitZMultiplesEquiv_symm_apply {α : Type u_3} {β : Type u_4} [AddGroup α] (a : α) [AddAction α β] (b : β) (k : ZMod (Function.minimalPeriod (fun (x : β) => a +ᵥ x) b)) :
theorem MulAction.orbitZPowersEquiv_symm_apply' {α : Type u_3} {β : Type u_4} [Group α] (a : α) [MulAction α β] (b : β) (k : ) :
(orbitZPowersEquiv a b).symm k = a, ^ k b,
theorem AddAction.orbitZMultiplesEquiv_symm_apply' {α : Type u_5} {β : Type u_6} [AddGroup α] (a : α) [AddAction α β] (b : β) (k : ) :
(orbitZMultiplesEquiv a b).symm k = k a, +ᵥ b,
theorem MulAction.minimalPeriod_eq_card {α : Type u_3} {β : Type u_4} [Group α] (a : α) [MulAction α β] (b : β) [Fintype (orbit (↥(Subgroup.zpowers a)) b)] :
Function.minimalPeriod (fun (x : β) => a x) b = Fintype.card (orbit (↥(Subgroup.zpowers a)) b)
theorem AddAction.minimalPeriod_eq_card {α : Type u_3} {β : Type u_4} [AddGroup α] (a : α) [AddAction α β] (b : β) [Fintype (orbit (↥(AddSubgroup.zmultiples a)) b)] :
Function.minimalPeriod (fun (x : β) => a +ᵥ x) b = Fintype.card (orbit (↥(AddSubgroup.zmultiples a)) b)
instance MulAction.minimalPeriod_pos {α : Type u_3} {β : Type u_4} [Group α] (a : α) [MulAction α β] (b : β) [Finite (orbit (↥(Subgroup.zpowers a)) b)] :
NeZero (Function.minimalPeriod (fun (x : β) => a x) b)
instance AddAction.minimalPeriod_pos {α : Type u_3} {β : Type u_4} [AddGroup α] (a : α) [AddAction α β] (b : β) [Finite (orbit (↥(AddSubgroup.zmultiples a)) b)] :
NeZero (Function.minimalPeriod (fun (x : β) => a +ᵥ x) b)
@[simp]
theorem Nat.card_zpowers {α : Type u_3} [Group α] (a : α) :

See also Fintype.card_zpowers.

@[simp]
theorem finite_zpowers {α : Type u_3} [Group α] {a : α} :
@[simp]
theorem finite_zmultiples {α : Type u_3} [AddGroup α] {a : α} :
@[simp]
theorem infinite_zpowers {α : Type u_3} [Group α] {a : α} :
@[simp]
theorem IsOfFinOrder.finite_zpowers {α : Type u_3} [Group α] {a : α} :

Alias of the reverse direction of finite_zpowers.

noncomputable def Subgroup.quotientEquivSigmaZMod {G : Type u_3} [Group G] (H : Subgroup G) (g : G) :
G H (q : MulAction.orbitRel.Quotient (↥(zpowers g)) (G H)) × ZMod (Function.minimalPeriod (fun (x : G H) => g x) (Quotient.out q))

Partition G ⧸ H into orbits of the action of g : G.

Equations
  • One or more equations did not get rendered due to their size.
theorem Subgroup.quotientEquivSigmaZMod_apply {G : Type u_3} [Group G] (H : Subgroup G) (g : G) (q : MulAction.orbitRel.Quotient (↥(zpowers g)) (G H)) (k : ) :