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 : ∀ (i j : ι), 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 : β) : { x // x ∈ AddSubgroup.zmultiples a } ⧸ AddAction.stabilizer { x // x ∈ AddSubgroup.zmultiples a } b ≃+ ZMod (Function.minimalPeriod ((fun x x_1 => x +ᵥ x_1) a) 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 x_1 => x +ᵥ x_1) a) b)) : ↑(AddEquiv.symm (AddAction.zmultiplesQuotientStabilizerEquiv a b)) n = ↑(↑n • { val := a, property := (_ : a ∈ AddSubgroup.zmultiples a) })

noncomputable def MulAction.zpowersQuotientStabilizerEquiv {α : Type u_3} {β : Type u_4} [Group α] (a : α) [MulAction α β] (b : β) : { x // x ∈ Subgroup.zpowers a } ⧸ MulAction.stabilizer { x // x ∈ Subgroup.zpowers a } b ≃* Multiplicative (ZMod (Function.minimalPeriod ((fun x x_1 => x • x_1) a) 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 x_1 => x • x_1) a) b)) : ↑(MulEquiv.symm (MulAction.zpowersQuotientStabilizerEquiv a b)) n = ↑({ val := a, property := (_ : a ∈ Subgroup.zpowers a) } ^ ↑n)

noncomputable def MulAction.orbitZpowersEquiv {α : Type u_3} {β : Type u_4} [Group α] (a : α) [MulAction α β] (b : β) : ↑(MulAction.orbit { x // x ∈ Subgroup.zpowers a } b) ≃ ZMod (Function.minimalPeriod ((fun x x_1 => x • x_1) a) b)

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

Equations

• MulAction.orbitZpowersEquiv a b = (MulAction.orbitEquivQuotientStabilizer { x // x ∈ 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 { x // x ∈ AddSubgroup.zmultiples a } b) ≃ ZMod (Function.minimalPeriod ((fun x x_1 => x +ᵥ x_1) a) b)

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

Equations

• AddAction.orbitZmultiplesEquiv a b = (AddAction.orbitEquivQuotientStabilizer { x // x ∈ 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 x_1 => x +ᵥ x_1) a) b)) : ↑(AddAction.orbitZmultiplesEquiv a b).symm k = ↑k • { val := a, property := (_ : a ∈ AddSubgroup.zmultiples a) } +ᵥ { val := b, property := (_ : b ∈ AddAction.orbit { x // x ∈ 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 x_1 => x • x_1) a) b)) : ↑(MulAction.orbitZpowersEquiv a b).symm k = { val := a, property := (_ : a ∈ Subgroup.zpowers a) } ^ ↑k • { val := b, property := (_ : b ∈ MulAction.orbit { x // x ∈ 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 { x // x ∈ 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 { x // x ∈ AddSubgroup.zmultiples a } b) }

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

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

theorem AddAction.minimalPeriod_pos.proof_1 {α : Type u_1} {β : Type u_2} [AddGroup α] (a : α) [AddAction α β] (b : β) [Finite ↑(AddAction.orbit { x // x ∈ AddSubgroup.zmultiples a } b)] : NeZero (Function.minimalPeriod ((fun x x_1 => x +ᵥ x_1) a) b)

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

Equations

• @AddAction.minimalPeriod_pos = @AddAction.minimalPeriod_pos.proof_1

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

Equations

• @MulAction.minimalPeriod_pos = @MulAction.minimalPeriod_pos.proof_1

theorem add_order_eq_card_zmultiples' {α : Type u_3} [AddGroup α] (a : α) : addOrderOf a = Nat.card { x // x ∈ AddSubgroup.zmultiples a }

See also add_order_eq_card_zmultiples.

theorem order_eq_card_zpowers' {α : Type u_3} [Group α] (a : α) : orderOf a = Nat.card { x // x ∈ Subgroup.zpowers a }

See also orderOf_eq_card_zpowers.

theorem IsOfFinAddOrder.finite_zmultiples {α : Type u_3} [AddGroup α] {a : α} (h : IsOfFinAddOrder a) : Finite { x // x ∈ AddSubgroup.zmultiples a }

theorem IsOfFinOrder.finite_zpowers {α : Type u_3} [Group α] {a : α} (h : IsOfFinOrder a) : Finite { x // x ∈ Subgroup.zpowers a }