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
andzmod.quotient_zmultiples_equiv_zmod
:zmod n
is the group quotient ofℤ
byn ℤ := add_subgroup.zmultiples (n)
, (wheren : ℕ
andn : ℤ
respectively)zmod.quotient_span_nat_equiv_zmod
andzmod.quotient_span_equiv_zmod
:zmod n
is the ring quotient ofℤ
byn ℤ : ideal.span {n}
(wheren : ℕ
andn : ℤ
respectively)zmod.lift n f
is the map fromzmod n
induced byf : ℤ →+ A
that mapsn
to0
.
Tags #
zmod, quotient group, quotient ring, ideal quotient
ℤ
modulo multiples of n : ℕ
is zmod n
.
ℤ
modulo multiples of a : ℤ
is zmod a.nat_abs
.
ℤ
modulo the ideal generated by n : ℕ
is zmod n
.
ℤ
modulo the ideal generated by a : ℤ
is zmod a.nat_abs
.
Equations
noncomputable
def
add_action.zmultiples_quotient_stabilizer_equiv
{α : Type u_3}
{β : Type u_4}
[add_group α]
(a : α)
[add_action α β]
(b : β) :
The quotient (ℤ ∙ a) ⧸ (stabilizer b)
is cyclic of order minimal_period ((+ᵥ) a) b
.
Equations
- add_action.zmultiples_quotient_stabilizer_equiv a b = (add_equiv.of_bijective (quotient_add_group.map (add_subgroup.zmultiples ↑(function.minimal_period (has_vadd.vadd ⟨a, _⟩) b)) (add_action.stabilizer ↥(add_subgroup.zmultiples a) b) (⇑(zmultiples_hom ↥(add_subgroup.zmultiples a)) ⟨a, _⟩) _) _).symm.trans (int.quotient_zmultiples_nat_equiv_zmod (function.minimal_period (has_vadd.vadd a) b))
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)) :
noncomputable
def
mul_action.zpowers_quotient_stabilizer_equiv
{α : Type u_3}
{β : Type u_4}
[group α]
(a : α)
[mul_action α β]
(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' := _}
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)) :
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
.
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
.
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)) :
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)) :
theorem
mul_action.orbit_zpowers_equiv_symm_apply'
{α : Type u_3}
{β : Type u_4}
[group α]
(a : α)
[mul_action α β]
(b : β)
(k : ℤ) :
theorem
add_action.orbit_zmultiples_equiv_symm_apply'
{α : Type u_1}
{β : Type u_2}
[add_group α]
(a : α)
[add_action α β]
(b : β)
(k : ℤ) :
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)] :
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)] :
@[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)] :
@[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)] :