# `ZMod n` and quotient groups / rings #

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

## Main definitions #

- `ZMod.quotientZMultiplesNatEquivZMod` and `ZMod.quotientZMultiplesEquivZMod`: `ZMod n` is the group quotient of `ℤ` by `n ℤ := AddSubgroup.zmultiples (n)`, (where `n : ℕ` and `n : ℤ` respectively)
- `ZMod.lift n f` is the map from `ZMod n` induced by `f : ℤ →+ A` that maps `n` to `0`.

## Tags #

zmod, quotient group

source
def Int.quotientZMultiplesNatEquivZMod (n : ℕ) :
ℤ ⧸ AddSubgroup.zmultiples ↑n ≃+ ZMod n

`ℤ` modulo multiples of `n : ℕ` is `ZMod n`.

Equations

- Int.quotientZMultiplesNatEquivZMod n = (QuotientAddGroup.quotientAddEquivOfEq ⋯).symm.trans (QuotientAddGroup.quotientKerEquivOfRightInverse (Int.castAddHom (ZMod n)) ZMod.cast ⋯)

Instances For

source
def Int.quotientZMultiplesEquivZMod (a : ℤ) :
ℤ ⧸ AddSubgroup.zmultiples a ≃+ ZMod a.natAbs

`ℤ` modulo multiples of `a : ℤ` is `ZMod a.natAbs`.

Equations

- a.quotientZMultiplesEquivZMod = (QuotientAddGroup.quotientAddEquivOfEq ⋯).symm.trans (Int.quotientZMultiplesNatEquivZMod a.natAbs)

Instances For

source
@[simp]
theorem Int.index_zmultiples (a : ℤ) :
(AddSubgroup.zmultiples a).index = a.natAbs
source
noncomputable def AddAction.zmultiplesQuotientStabilizerEquiv {α : Type u_3} {β : Type u_4} [AddGroup α] (a : α) [AddAction α β] (b : β) :
↥(AddSubgroup.zmultiples a) ⧸ stabilizer (↥(AddSubgroup.zmultiples a)) b ≃+ ZMod (Function.minimalPeriod (fun (x : β) => a +ᵥ x) 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.

Instances For

source
theorem AddAction.zmultiplesQuotientStabilizerEquiv_symm_apply {α : Type u_3} {β : Type u_4} [AddGroup α] (a : α) [AddAction α β] (b : β) (n : ZMod (Function.minimalPeriod (fun (x : β) => a +ᵥ x) b)) :
(zmultiplesQuotientStabilizerEquiv a b).symm n = n.cast • ↑⟨a, ⋯⟩
source
noncomputable def MulAction.zpowersQuotientStabilizerEquiv {α : Type u_3} {β : Type u_4} [Group α] (a : α) [MulAction α β] (b : β) :
↥(Subgroup.zpowers a) ⧸ stabilizer (↥(Subgroup.zpowers a)) b ≃* Multiplicative (ZMod (Function.minimalPeriod (fun (x : β) => a • x) b))

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

Equations

- MulAction.zpowersQuotientStabilizerEquiv a b = AddEquiv.toMultiplicative (AddAction.zmultiplesQuotientStabilizerEquiv (Additive.ofMul a) b)

Instances For

source
theorem MulAction.zpowersQuotientStabilizerEquiv_symm_apply {α : Type u_3} {β : Type u_4} [Group α] (a : α) [MulAction α β] (b : β) (n : ZMod (Function.minimalPeriod (fun (x : β) => a • x) b)) :
(zpowersQuotientStabilizerEquiv a b).symm n = ↑⟨a, ⋯⟩ ^ n.cast
source
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

- MulAction.orbitZPowersEquiv a b = (MulAction.orbitEquivQuotientStabilizer (↥(Subgroup.zpowers a)) b).trans (MulAction.zpowersQuotientStabilizerEquiv a b).toEquiv

Instances For

source
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

- AddAction.orbitZMultiplesEquiv a b = (AddAction.orbitEquivQuotientStabilizer (↥(AddSubgroup.zmultiples a)) b).trans (AddAction.zmultiplesQuotientStabilizerEquiv a b).toEquiv

Instances For

source
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, ⋯⟩
source
theorem AddAction.orbitZMultiplesEquiv_symm_apply {α : Type u_3} {β : Type u_4} [AddGroup α] (a : α) [AddAction α β] (b : β) (k : ZMod (Function.minimalPeriod (fun (x : β) => a +ᵥ x) b)) :
(orbitZMultiplesEquiv a b).symm k = k.cast • ⟨a, ⋯⟩ +ᵥ ⟨b, ⋯⟩
source
theorem MulAction.orbitZPowersEquiv_symm_apply' {α : Type u_3} {β : Type u_4} [Group α] (a : α) [MulAction α β] (b : β) (k : ℤ) :
(orbitZPowersEquiv a b).symm ↑k = ⟨a, ⋯⟩ ^ k • ⟨b, ⋯⟩
source
theorem AddAction.orbitZMultiplesEquiv_symm_apply' {α : Type u_5} {β : Type u_6} [AddGroup α] (a : α) [AddAction α β] (b : β) (k : ℤ) :
(orbitZMultiplesEquiv a b).symm ↑k = k • ⟨a, ⋯⟩ +ᵥ ⟨b, ⋯⟩
source
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)
source
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)
source
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)
source
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)
source
@[simp]
theorem Nat.card_zpowers {α : Type u_3} [Group α] (a : α) :
Nat.card ↥(Subgroup.zpowers a) = orderOf a

See also `Fintype.card_zpowers`.

source
@[simp]
theorem Nat.card_zmultiples {α : Type u_3} [AddGroup α] (a : α) :
Nat.card ↥(AddSubgroup.zmultiples a) = addOrderOf a

See also `Fintype.card_zmultiples`.

source
@[simp]
theorem finite_zpowers {α : Type u_3} [Group α] {a : α} :
(↑(Subgroup.zpowers a)).Finite ↔ IsOfFinOrder a
source
@[simp]
theorem finite_zmultiples {α : Type u_3} [AddGroup α] {a : α} :
(↑(AddSubgroup.zmultiples a)).Finite ↔ IsOfFinAddOrder a
source
@[simp]
theorem infinite_zpowers {α : Type u_3} [Group α] {a : α} :
(↑(Subgroup.zpowers a)).Infinite ↔ ¬IsOfFinOrder a
source
@[simp]
theorem infinite_zmultiples {α : Type u_3} [AddGroup α] {a : α} :
(↑(AddSubgroup.zmultiples a)).Infinite ↔ ¬IsOfFinAddOrder a
source
theorem IsOfFinOrder.finite_zpowers {α : Type u_3} [Group α] {a : α} :
IsOfFinOrder a → (↑(Subgroup.zpowers a)).Finite

Alias of the reverse direction of `finite_zpowers`.

source
theorem IsOfFinAddOrder.finite_zmultiples {α : Type u_3} [AddGroup α] {a : α} :
IsOfFinAddOrder a → (↑(AddSubgroup.zmultiples a)).Finite
source
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.

Instances For

source
theorem Subgroup.quotientEquivSigmaZMod_symm_apply {G : Type u_3} [Group G] (H : Subgroup G) (g : G) (q : MulAction.orbitRel.Quotient (↥(zpowers g)) (G ⧸ H)) (k : ZMod (Function.minimalPeriod (fun (x : G ⧸ H) => g • x) (Quotient.out q))) :
(H.quotientEquivSigmaZMod g).symm ⟨q, k⟩ = g ^ k.cast • Quotient.out q
source
theorem Subgroup.quotientEquivSigmaZMod_apply {G : Type u_3} [Group G] (H : Subgroup G) (g : G) (q : MulAction.orbitRel.Quotient (↥(zpowers g)) (G ⧸ H)) (k : ℤ) :
(H.quotientEquivSigmaZMod g) (g ^ k • Quotient.out q) = ⟨q, ↑k⟩