ZMod n and quotient groups / rings

This file relates ZMod n to the quotient group ℤ / AddSubgroup.zmultiples (n : ℤ) and to the quotient ring ℤ ⧸ Ideal.span {(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.quotient_span_nat_equiv_zmod and ZMod.quotientSpanEquivZMod : ZMod n is the ring quotient of ℤ by n ℤ : Ideal.span {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, quotient ring, ideal quotient

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 ⋯)

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)

def Int.quotientSpanNatEquivZMod (n : ℕ) : ℤ ⧸ Ideal.span {↑n} ≃+* ZMod n

ℤ modulo the ideal generated by n : ℕ is ZMod n.

Equations

• Int.quotientSpanNatEquivZMod n = (Ideal.quotEquivOfEq ⋯).symm.trans (RingHom.quotientKerEquivOfRightInverse ⋯)

def Int.quotientSpanEquivZMod (a : ℤ) : ℤ ⧸ Ideal.span {a} ≃+* ZMod a.natAbs

ℤ modulo the ideal generated by a : ℤ is ZMod a.natAbs.

Equations

• a.quotientSpanEquivZMod = (Ideal.quotEquivOfEq ⋯).symm.trans (Int.quotientSpanNatEquivZMod a.natAbs)

@[simp]

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

def ZMod.prodEquivPi {ι : Type u_3} [Fintype ι] (a : ι → ℕ) (coprime : Pairwise fun (i j : ι) => (a i).Coprime (a j)) : ZMod (∏ i : ι, a i) ≃+* ((i : ι) → ZMod (a i))

The Chinese remainder theorem, elementary version for ZMod. See also Mathlib.Data.ZMod.Basic for versions involving only two numbers.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def AddAction.zmultiplesQuotientStabilizerEquiv {α : Type u_3} {β : Type u_4} [AddGroup α] (a : α) [AddAction α β] (b : β) : ↥(AddSubgroup.zmultiples a) ⧸ AddAction.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.

theorem AddAction.zmultiplesQuotientStabilizerEquiv_symm_apply {α : Type u_3} {β : Type u_4} [AddGroup α] (a : α) [AddAction α β] (b : β) (n : ZMod (Function.minimalPeriod (fun (x : β) => a +ᵥ x) b)) : (AddAction.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) ⧸ MulAction.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)

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

noncomputable def MulAction.orbitZPowersEquiv {α : Type u_3} {β : Type u_4} [Group α] (a : α) [MulAction α β] (b : β) : ↑(MulAction.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

noncomputable def AddAction.orbitZMultiplesEquiv {α : Type u_5} {β : Type u_6} [AddGroup α] (a : α) [AddAction α β] (b : β) : ↑(AddAction.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

theorem AddAction.orbitZMultiplesEquiv_symm_apply {α : Type u_3} {β : Type u_4} [AddGroup α] (a : α) [AddAction α β] (b : β) (k : ZMod (Function.minimalPeriod (fun (x : β) => a +ᵥ x) b)) : (AddAction.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 : ZMod (Function.minimalPeriod (fun (x : β) => a • x) b)) : (MulAction.orbitZPowersEquiv a b).symm k = ⟨a, ⋯⟩ ^ k.cast • ⟨b, ⋯⟩

@[deprecated AddAction.orbitZMultiplesEquiv_symm_apply]

theorem AddAction.orbit_zmultiples_equiv_symm_apply {α : Type u_3} {β : Type u_4} [AddGroup α] (a : α) [AddAction α β] (b : β) (k : ZMod (Function.minimalPeriod (fun (x : β) => a +ᵥ x) b)) : (AddAction.orbitZMultiplesEquiv a b).symm k = k.cast • ⟨a, ⋯⟩ +ᵥ ⟨b, ⋯⟩

Alias of AddAction.orbitZMultiplesEquiv_symm_apply.

theorem MulAction.orbitZPowersEquiv_symm_apply' {α : Type u_3} {β : Type u_4} [Group α] (a : α) [MulAction α β] (b : β) (k : ℤ) : (MulAction.orbitZPowersEquiv a b).symm ↑k = ⟨a, ⋯⟩ ^ k • ⟨b, ⋯⟩

theorem AddAction.orbitZMultiplesEquiv_symm_apply' {α : Type u_5} {β : Type u_6} [AddGroup α] (a : α) [AddAction α β] (b : β) (k : ℤ) : (AddAction.orbitZMultiplesEquiv a b).symm ↑k = k • ⟨a, ⋯⟩ +ᵥ ⟨b, ⋯⟩

theorem AddAction.minimalPeriod_eq_card {α : Type u_3} {β : Type u_4} [AddGroup α] (a : α) [AddAction α β] (b : β) [Fintype ↑(AddAction.orbit (↥(AddSubgroup.zmultiples a)) b)] : Function.minimalPeriod (fun (x : β) => a +ᵥ x) b = Fintype.card ↑(AddAction.orbit (↥(AddSubgroup.zmultiples a)) b)

theorem MulAction.minimalPeriod_eq_card {α : Type u_3} {β : Type u_4} [Group α] (a : α) [MulAction α β] (b : β) [Fintype ↑(MulAction.orbit (↥(Subgroup.zpowers a)) b)] : Function.minimalPeriod (fun (x : β) => a • x) b = Fintype.card ↑(MulAction.orbit (↥(Subgroup.zpowers a)) b)

instance AddAction.minimalPeriod_pos {α : Type u_3} {β : Type u_4} [AddGroup α] (a : α) [AddAction α β] (b : β) [Finite ↑(AddAction.orbit (↥(AddSubgroup.zmultiples a)) b)] : NeZero (Function.minimalPeriod (fun (x : β) => a +ᵥ x) b)

Equations

• ⋯ = ⋯

instance MulAction.minimalPeriod_pos {α : Type u_3} {β : Type u_4} [Group α] (a : α) [MulAction α β] (b : β) [Finite ↑(MulAction.orbit (↥(Subgroup.zpowers a)) b)] : NeZero (Function.minimalPeriod (fun (x : β) => a • x) b)

Equations

• ⋯ = ⋯

@[simp]

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

See also Fintype.card_zmultiples.

@[simp]

theorem Nat.card_zpowers {α : Type u_3} [Group α] (a : α) : Nat.card ↥(Subgroup.zpowers a) = orderOf a

See also Fintype.card_zpowers.

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem infinite_zpowers {α : Type u_3} [Group α] {a : α} : (↑(Subgroup.zpowers a)).Infinite ↔ ¬IsOfFinOrder 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