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

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

ℤ modulo multiples of n : ℕ is ZMod n.

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

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

@[simp]

theorem Int.index_zmultiples (a : ℤ) : (AddSubgroup.zmultiples a).index = a.natAbs

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.

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, ⋯⟩

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.

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

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.

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.

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)) : (orbitZMultiplesEquiv a b).symm k = k.cast • ⟨a, ⋯⟩ +ᵥ ⟨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 : α) : Nat.card ↥(Subgroup.zpowers a) = orderOf a

See also Fintype.card_zpowers.

@[simp]

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

See also Fintype.card_zmultiples.

@[simp]

theorem finite_zpowers {α : Type u_3} [Group α] {a : α} : (↑(Subgroup.zpowers a)).Finite ↔ IsOfFinOrder a

@[simp]

theorem finite_zmultiples {α : Type u_3} [AddGroup α] {a : α} : (↑(AddSubgroup.zmultiples a)).Finite ↔ IsOfFinAddOrder a

@[simp]

theorem infinite_zpowers {α : Type u_3} [Group α] {a : α} : (↑(Subgroup.zpowers a)).Infinite ↔ ¬IsOfFinOrder a

@[simp]

theorem infinite_zmultiples {α : Type u_3} [AddGroup α] {a : α} : (↑(AddSubgroup.zmultiples a)).Infinite ↔ ¬IsOfFinAddOrder a

theorem IsOfFinOrder.finite_zpowers {α : Type u_3} [Group α] {a : α} : IsOfFinOrder a → (↑(Subgroup.zpowers a)).Finite

Alias of the reverse direction of finite_zpowers.

theorem IsOfFinAddOrder.finite_zmultiples {α : Type u_3} [AddGroup α] {a : α} : IsOfFinAddOrder a → (↑(AddSubgroup.zmultiples a)).Finite

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.

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

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⟩