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

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

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

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

Equations

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

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

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

Equations

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

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

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

Equations

• Int.quotientSpanEquivZMod a = RingEquiv.trans (RingEquiv.symm (Ideal.quotEquivOfEq (_ : Ideal.span {↑(Int.natAbs a)} = Ideal.span {a}))) (Int.quotientSpanNatEquivZMod (Int.natAbs a))

def ZMod.prodEquivPi {ι : Type u_3} [Fintype ι] (a : ι → ℕ) (coprime : Pairwise fun (i j : ι) => Nat.Coprime (a i) (a j)) : ZMod (Finset.prod Finset.univ fun (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)) : (AddEquiv.symm (AddAction.zmultiplesQuotientStabilizerEquiv a b)) n = ZMod.cast n • ↑{ val := a, property := (_ : a ∈ AddSubgroup.zmultiples 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)) : (MulEquiv.symm (MulAction.zpowersQuotientStabilizerEquiv a b)) n = ↑{ val := a, property := (_ : a ∈ Subgroup.zpowers a) } ^ ZMod.cast n

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.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 = ZMod.cast k • { val := a, property := (_ : a ∈ AddSubgroup.zmultiples a) } +ᵥ { val := b, property := (_ : b ∈ AddAction.orbit (↥(AddSubgroup.zmultiples 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 = { val := a, property := (_ : a ∈ Subgroup.zpowers a) } ^ ZMod.cast k • { val := b, property := (_ : b ∈ MulAction.orbit (↥(Subgroup.zpowers a)) b) }

theorem MulAction.orbitZPowersEquiv_symm_apply' {α : Type u_3} {β : Type u_4} [Group α] (a : α) [MulAction α β] (b : β) (k : ℤ) : (MulAction.orbitZPowersEquiv a b).symm ↑k = { val := a, property := (_ : a ∈ Subgroup.zpowers a) } ^ k • { val := b, property := (_ : b ∈ MulAction.orbit (↥(Subgroup.zpowers a)) b) }

theorem AddAction.orbitZMultiplesEquiv_symm_apply' {α : Type u_5} {β : Type u_6} [AddGroup α] (a : α) [AddAction α β] (b : β) (k : ℤ) : (AddAction.orbitZMultiplesEquiv a b).symm ↑k = k • { val := a, property := (_ : a ∈ AddSubgroup.zmultiples a) } +ᵥ { val := b, property := (_ : b ∈ AddAction.orbit (↥(AddSubgroup.zmultiples 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

• (_ : NeZero (Function.minimalPeriod (fun (x : β) => a +ᵥ x) b)) = (_ : NeZero (Function.minimalPeriod (fun (x : β) => a +ᵥ x) b))

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

• (_ : NeZero (Function.minimalPeriod (fun (x : β) => a • x) b)) = (_ : NeZero (Function.minimalPeriod (fun (x : β) => a • x) b))

@[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 : α} : Set.Finite ↑(AddSubgroup.zmultiples a) ↔ IsOfFinAddOrder a

@[simp]

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

@[simp]

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

@[simp]

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

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

Alias of the reverse direction of finite_zpowers.

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