`zmod n` and quotient groups / rings #

This file relates zmod n to the quotient group quotient_add_group.quotient (add_subgroup.zmultiples n) and to the quotient ring (ideal.span {n}).quotient.

Main definitions #

zmod.quotient_zmultiples_nat_equiv_zmod and zmod.quotient_zmultiples_equiv_zmod: zmod n is the group quotient of ℤ by n ℤ := add_subgroup.zmultiples (n), (where n : ℕ and n : ℤ respectively)
zmod.quotient_span_nat_equiv_zmod and zmod.quotient_span_equiv_zmod: 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

source

def int.quotient_zmultiples_nat_equiv_zmod (n : ℕ) :

ℤ ⧸ add_subgroup.zmultiples ↑n ≃+ zmod n

ℤ modulo multiples of n : ℕ is zmod n.

Equations

int.quotient_zmultiples_nat_equiv_zmod n = (quotient_add_group.equiv_quotient_of_eq _).symm.trans (quotient_add_group.quotient_ker_equiv_of_right_inverse (int.cast_add_hom (zmod n)) coe zmod.int_cast_zmod_cast)

source

def int.quotient_zmultiples_equiv_zmod (a : ℤ) :

ℤ ⧸ add_subgroup.zmultiples a ≃+ zmod a.nat_abs

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

Equations

a.quotient_zmultiples_equiv_zmod = (quotient_add_group.equiv_quotient_of_eq _).symm.trans (int.quotient_zmultiples_nat_equiv_zmod a.nat_abs)

source

def int.quotient_span_nat_equiv_zmod (n : ℕ) :

ℤ ⧸ ideal.span {↑n} ≃+* zmod n

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

Equations

int.quotient_span_nat_equiv_zmod n = (ideal.quot_equiv_of_eq _).symm.trans (ring_hom.quotient_ker_equiv_of_right_inverse _)

source

def int.quotient_span_equiv_zmod (a : ℤ) :

ℤ ⧸ ideal.span {a} ≃+* zmod a.nat_abs

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

Equations

a.quotient_span_equiv_zmod = (ideal.quot_equiv_of_eq _).symm.trans (int.quotient_span_nat_equiv_zmod a.nat_abs)

source

noncomputable def add_action.zmultiples_quotient_stabilizer_equiv {α : Type u_3} {β : Type u_4} [add_group α] (a : α) [add_action α β] (b : β) :

↥(add_subgroup.zmultiples a) ⧸ add_action.stabilizer ↥(add_subgroup.zmultiples a) b ≃+ zmod (function.minimal_period (has_vadd.vadd a) b)

The quotient (ℤ ∙ a) ⧸ (stabilizer b) is cyclic of order minimal_period ((+ᵥ) a) b.

Equations

source

theorem add_action.zmultiples_quotient_stabilizer_equiv_symm_apply {α : Type u_3} {β : Type u_4} [add_group α] (a : α) [add_action α β] (b : β) (n : zmod (function.minimal_period (has_vadd.vadd a) b)) :

⇑((add_action.zmultiples_quotient_stabilizer_equiv a b).symm) n = ↑n • ↑⟨a, _⟩

source

noncomputable def mul_action.zpowers_quotient_stabilizer_equiv {α : Type u_3} {β : Type u_4} [group α] (a : α) [mul_action α β] (b : β) :

↥(subgroup.zpowers a) ⧸ mul_action.stabilizer ↥(subgroup.zpowers a) b ≃* multiplicative (zmod (function.minimal_period (has_scalar.smul a) b))

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

Equations

mul_action.zpowers_quotient_stabilizer_equiv a b = let f : ↥(add_subgroup.zmultiples (⇑additive.of_mul a)) ⧸ add_action.stabilizer ↥(add_subgroup.zmultiples (⇑additive.of_mul a)) b ≃+ zmod (function.minimal_period (has_vadd.vadd (⇑additive.of_mul a)) b) := add_action.zmultiples_quotient_stabilizer_equiv (⇑additive.of_mul a) b in {to_fun := f.to_fun, inv_fun := f.inv_fun, left_inv := _, right_inv := _, map_mul' := _}

source

theorem mul_action.zpowers_quotient_stabilizer_equiv_symm_apply {α : Type u_3} {β : Type u_4} [group α] (a : α) [mul_action α β] (b : β) (n : zmod (function.minimal_period (has_scalar.smul a) b)) :

⇑((mul_action.zpowers_quotient_stabilizer_equiv a b).symm) n = ↑⟨a, _⟩ ^ ↑n

source

noncomputable def mul_action.orbit_zpowers_equiv {α : Type u_3} {β : Type u_4} [group α] (a : α) [mul_action α β] (b : β) :

↥(mul_action.orbit ↥(subgroup.zpowers a) b) ≃ zmod (function.minimal_period (has_scalar.smul a) b)

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

Equations

mul_action.orbit_zpowers_equiv a b = (mul_action.orbit_equiv_quotient_stabilizer ↥(subgroup.zpowers a) b).trans (mul_action.zpowers_quotient_stabilizer_equiv a b).to_equiv

source

noncomputable def add_action.orbit_zmultiples_equiv {α : Type u_1} {β : Type u_2} [add_group α] (a : α) [add_action α β] (b : β) :

↥(add_action.orbit ↥(add_subgroup.zmultiples a) b) ≃ zmod (function.minimal_period (has_vadd.vadd a) b)

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

Equations

add_action.orbit_zmultiples_equiv a b = (add_action.orbit_equiv_quotient_stabilizer ↥(add_subgroup.zmultiples a) b).trans (add_action.zmultiples_quotient_stabilizer_equiv a b).to_equiv

source

theorem mul_action.orbit_zpowers_equiv_symm_apply {α : Type u_3} {β : Type u_4} [group α] (a : α) [mul_action α β] (b : β) (k : zmod (function.minimal_period (has_scalar.smul a) b)) :

⇑((mul_action.orbit_zpowers_equiv a b).symm) k = ⟨a, _⟩ ^ ↑k • ⟨b, _⟩

source

theorem add_action.orbit_zmultiples_equiv_symm_apply {α : Type u_3} {β : Type u_4} [add_group α] (a : α) [add_action α β] (b : β) (k : zmod (function.minimal_period (has_vadd.vadd a) b)) :

⇑((add_action.orbit_zmultiples_equiv a b).symm) k = ↑k • ⟨a, _⟩ +ᵥ ⟨b, _⟩

source

theorem mul_action.orbit_zpowers_equiv_symm_apply' {α : Type u_3} {β : Type u_4} [group α] (a : α) [mul_action α β] (b : β) (k : ℤ) :

⇑((mul_action.orbit_zpowers_equiv a b).symm) ↑k = ⟨a, _⟩ ^ k • ⟨b, _⟩

source

theorem add_action.orbit_zmultiples_equiv_symm_apply' {α : Type u_1} {β : Type u_2} [add_group α] (a : α) [add_action α β] (b : β) (k : ℤ) :

⇑((add_action.orbit_zmultiples_equiv a b).symm) ↑k = k • ⟨a, _⟩ +ᵥ ⟨b, _⟩

source

theorem add_action.minimal_period_eq_card {α : Type u_3} {β : Type u_4} [add_group α] (a : α) [add_action α β] (b : β) [fintype ↥(add_action.orbit ↥(add_subgroup.zmultiples a) b)] :

function.minimal_period (has_vadd.vadd a) b = fintype.card ↥(add_action.orbit ↥(add_subgroup.zmultiples a) b)

source

theorem mul_action.minimal_period_eq_card {α : Type u_3} {β : Type u_4} [group α] (a : α) [mul_action α β] (b : β) [fintype ↥(mul_action.orbit ↥(subgroup.zpowers a) b)] :

function.minimal_period (has_scalar.smul a) b = fintype.card ↥(mul_action.orbit ↥(subgroup.zpowers a) b)

source

@[protected, instance]

def add_action.minimal_period_pos {α : Type u_3} {β : Type u_4} [add_group α] (a : α) [add_action α β] (b : β) [fintype ↥(add_action.orbit ↥(add_subgroup.zmultiples a) b)] :

ne_zero (function.minimal_period (has_vadd.vadd a) b)

source

@[protected, instance]

def mul_action.minimal_period_pos {α : Type u_3} {β : Type u_4} [group α] (a : α) [mul_action α β] (b : β) [fintype ↥(mul_action.orbit ↥(subgroup.zpowers a) b)] :

ne_zero (function.minimal_period (has_scalar.smul a) b)

zmod n and quotient groups / rings #

Main definitions #

Tags #

`zmod n` and quotient groups / rings #