Commutative monoids that have enough roots of unity

theorem ZMod.inv_mul_eq_one_of_isUnit {n : ℕ} {a : ZMod n} (ha : IsUnit a) (b : ZMod n) : a⁻¹ * b = 1 ↔ a = b

instance IsAlgClosed.hasEnoughRootsOfUnity (F : Type u_1) [Field F] [IsAlgClosed F] [CharZero F] (n : ℕ) [NeZero n] : HasEnoughRootsOfUnity F n

An algebraically closed field of characteristic zero satisfies HasEnoughRootsOfUnity for all n.

Equations

• ⋯ = ⋯

Results specific for cyclic groups

noncomputable def IsCyclic.monoidHomMulEquivRootsOfUnityOfGenerator {G : Type u_1} [CommGroup G] [Fintype G] {g : G} (hg : ∀ (x : G), x ∈ Subgroup.zpowers g) (G' : Type u_2) [CommGroup G'] : (G →* G') ≃* ↥(rootsOfUnity (Fintype.card G) G')

The isomorphism from the group of group homomorphisms from a finite cyclic group G of order n into another group G' to the group of nth roots of unity in G' determined by a generator g of G. It sends φ : G →* G' to φ g.

Equations

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

theorem IsCyclic.monoidHom_mulEquiv_rootsOfUnity (G : Type u_1) [CommGroup G] [Finite G] [IsCyclic G] (G' : Type u_2) [CommGroup G'] : Nonempty ((G →* G') ≃* ↥(rootsOfUnity (Nat.card G) G'))

The group of group homomorphisms from a finite cyclic group G of order n into another group G' is (noncanonically) isomorphic to the group of nth roots of unity in G'.

theorem IsCyclic.exists_apply_ne_one {G : Type u_1} {G' : Type u_2} [CommGroup G] [IsCyclic G] [Finite G] [CommGroup G'] (hG' : ∃ (ζ : G'), IsPrimitiveRoot ζ (Nat.card G)) ⦃a : G⦄ (ha : a ≠ 1) : ∃ (φ : G →* G'), φ a ≠ 1

If G is cyclic of order n and G' contains a primitive nth root of unity, then for each a : G with a ≠ 1 there is a homomorphism φ : G →* G' such that φ a ≠ 1.

theorem IsCyclic.monoidHom_equiv_self (G : Type u_1) (M : Type u_2) [CommGroup G] [Finite G] [IsCyclic G] [CommMonoid M] [HasEnoughRootsOfUnity M (Nat.card G)] : Nonempty ((G →* Mˣ) ≃* G)

The group of group homomorphims from a finite cyclic group G of order n into the group of units of a ring M with all roots of unity is isomorphic to G

theorem ZMod.exists_monoidHom_apply_ne_one {M : Type u_1} [CommMonoid M] {n : ℕ} [NeZero n] (hG : ∃ (ζ : M), IsPrimitiveRoot ζ n) {a : ZMod n} (ha : a ≠ 0) : ∃ (φ : Multiplicative (ZMod n) →* Mˣ), φ (Multiplicative.ofAdd a) ≠ 1

If M is a commutative group that contains a primitive nth root of unity and a : ZMod n is nonzero, then there exists a group homomorphism φ from the additive group ZMod n to the multiplicative group Mˣ such that φ a ≠ 1.

Results for general finite abelian groups

theorem CommGroup.exists_apply_ne_one_of_hasEnoughRootsOfUnity (G : Type u_1) (M : Type u_2) [CommGroup G] [Finite G] [CommMonoid M] [HasEnoughRootsOfUnity M (Monoid.exponent G)] {a : G} (ha : a ≠ 1) : ∃ (φ : G →* Mˣ), φ a ≠ 1

If G is a finite commutative group of exponent n and M is a commutative monoid with enough nth roots of unity, then for each a ≠ 1 in G, there exists a group homomorphism φ : G → Mˣ such that φ a ≠ 1.

theorem CommGroup.monoidHom_mulEquiv_self_of_hasEnoughRootsOfUnity (G : Type u_1) (M : Type u_2) [CommGroup G] [Finite G] [CommMonoid M] [HasEnoughRootsOfUnity M (Monoid.exponent G)] : Nonempty (G ≃* (G →* Mˣ))

A finite commutative group G is (noncanonically) isomorphic to the group G →* Mˣ of M-valued characters when M is a commutative monoid with enough nth roots of unity, where n is the exponent of G.

Results for multiplicative characters

We provide instances for Finite (MulChar M R) and Fintype (MulChar M R) when M is a finite commutative monoid and R is an integral domain.

We also show that MulChar M R and Mˣ have the same cardinality when R has enough roots of unity.

instance MulChar.finite {M : Type u_1} {R : Type u_2} [CommMonoid M] [CommRing R] [Finite Mˣ] [IsDomain R] : Finite (MulChar M R)

Equations

• ⋯ = ⋯

noncomputable instance MulChar.fintype {M : Type u_1} {R : Type u_2} [CommMonoid M] [CommRing R] [Finite M] [IsDomain R] : Fintype (MulChar M R)

Equations

• MulChar.fintype = Fintype.ofFinite (MulChar M R)

theorem MulChar.exists_apply_ne_one_iff_exists_monoidHom {M : Type u_1} {R : Type u_2} [CommMonoid M] [CommRing R] (a : Mˣ) : (∃ (χ : MulChar M R), χ ↑a ≠ 1) ↔ ∃ (φ : Mˣ →* Rˣ), φ a ≠ 1

theorem MulChar.exists_apply_ne_one_of_hasEnoughRootsOfUnity (M : Type u_1) (R : Type u_2) [CommMonoid M] [CommRing R] [Finite M] [HasEnoughRootsOfUnity R (Monoid.exponent Mˣ)] [Nontrivial R] {a : M} (ha : a ≠ 1) : ∃ (χ : MulChar M R), χ a ≠ 1

If M is a finite commutative monoid and R is a ring that has enough roots of unity, then for each a ≠ 1 in M, there exists a multiplicative character χ : M → R such that χ a ≠ 1.

theorem MulChar.mulEquiv_units (M : Type u_1) (R : Type u_2) [CommMonoid M] [CommRing R] [Finite M] [HasEnoughRootsOfUnity R (Monoid.exponent Mˣ)] : Nonempty (MulChar M R ≃* Mˣ)

The group of R-valued multiplicative characters on a finite commutative monoid M is (noncanonically) isomorphic to its unit group Mˣ when R is a ring that has enough roots of unity.

theorem MulChar.card_eq_card_units_of_hasEnoughRootsOfUnity (M : Type u_1) (R : Type u_2) [CommMonoid M] [CommRing R] [Finite M] [HasEnoughRootsOfUnity R (Monoid.exponent Mˣ)] : Nat.card (MulChar M R) = Nat.card Mˣ

The cardinality of the group of R-valued multiplicative characters on a finite commutative monoid M is the same as that of its unit group Mˣ when R is a ring that has enough roots of unity.

Results for Dirichlet characters

The main goal of this section is to show that ∑ χ : DirichletCharacter R n, χ a vanishes if a ≠ 1 and takes the value n.totient otherwise.

noncomputable instance DirichletCharacter.inhabited (R : Type u_1) [CommMonoidWithZero R] (n : ℕ) : Inhabited (DirichletCharacter R n)

Equations

• DirichletCharacter.inhabited R n = { default := 1 }

instance DirichletCharacter.finite {n : ℕ} {R : Type u_1} [CommRing R] [IsDomain R] : Finite (DirichletCharacter R n)

Equations

• ⋯ = ⋯

noncomputable instance DirichletCharacter.fintype {n : ℕ} {R : Type u_1} [CommRing R] [IsDomain R] : Fintype (DirichletCharacter R n)

Equations

• DirichletCharacter.fintype = Fintype.ofFinite (DirichletCharacter R n)

theorem DirichletCharacter.sum_characters_eq_zero_aux {n : ℕ} {R : Type u_1} [CommRing R] [IsDomain R] {a : ZMod n} (h : ∃ (χ : DirichletCharacter R n), χ a ≠ 1) : ∑ χ : DirichletCharacter R n, χ a = 0

theorem DirichletCharacter.sum_characters_eq_zero_iff_aux {n : ℕ} {R : Type u_1} [CommRing R] [IsDomain R] {a : ZMod n} [CharZero R] (h : ∀ (a : ZMod n), a ≠ 1 → ∃ (χ : DirichletCharacter R n), χ a ≠ 1) : ∑ χ : DirichletCharacter R n, χ a = 0 ↔ a ≠ 1

theorem DirichletCharacter.mulEquiv_units (R : Type u_1) [CommRing R] (n : ℕ) [NeZero n] [HasEnoughRootsOfUnity R n.totient] : Nonempty (DirichletCharacter R n ≃* (ZMod n)ˣ)

The group of Dirichlet characters mod n with values in a ring R that has enough roots of unity is (noncanonically) isomorphic to (ZMod n)ˣ.

theorem DirichletCharacter.card_eq_totient_of_hasEnoughRootsOfUnity (R : Type u_1) [CommRing R] (n : ℕ) [NeZero n] [HasEnoughRootsOfUnity R n.totient] : Nat.card (DirichletCharacter R n) = n.totient

There are n.totient Dirichlet characters mod n with values in a ring that has all roots of unity.

theorem DirichletCharacter.exists_apply_ne_one_of_hasEnoughRootsOfUnity (R : Type u_1) [CommRing R] {n : ℕ} [NeZero n] [HasEnoughRootsOfUnity R n.totient] [Nontrivial R] ⦃a : ZMod n⦄ (ha : a ≠ 1) : ∃ (χ : DirichletCharacter R n), χ a ≠ 1

If R is a ring that has enough roots of unity and n ≠ 0, then for each a ≠ 1 in ZMod n, there exists a Dirichlet character χ mod n with values in R such that χ a ≠ 1.

theorem DirichletCharacter.sum_characters_eq_zero (R : Type u_1) [CommRing R] {n : ℕ} [NeZero n] [HasEnoughRootsOfUnity R n.totient] [IsDomain R] ⦃a : ZMod n⦄ (ha : a ≠ 1) : ∑ χ : DirichletCharacter R n, χ a = 0

If R is an integral domain that has enough roots of unity and n ≠ 0, then for each a ≠ 1 in ZMod n, the sum of χ a over all Dirichlet characters mod n with values in R vanishes.

theorem DirichletCharacter.sum_characters_eq (R : Type u_1) [CommRing R] {n : ℕ} [NeZero n] [HasEnoughRootsOfUnity R n.totient] [IsDomain R] (a : ZMod n) : ∑ χ : DirichletCharacter R n, χ a = if a = 1 then ↑n.totient else 0

If R is an integral domain that has enough roots of unity and n ≠ 0, then for a in ZMod n, the sum of χ a over all Dirichlet characters mod n with values in R vanishes if a ≠ 1 and has the value n.totient if a = 1.

theorem DirichletCharacter.sum_char_inv_mul_char_eq (R : Type u_1) [CommRing R] {n : ℕ} [NeZero n] [HasEnoughRootsOfUnity R n.totient] [IsDomain R] {a : ZMod n} (ha : IsUnit a) (b : ZMod n) : ∑ χ : DirichletCharacter R n, χ a⁻¹ * χ b = ↑(if a = b then n.totient else 0)

If R is an integral domain that has enough roots of unity and n ≠ 0, then for a and b in ZMod n with a a unit, the sum of χ a⁻¹ * χ b over all Dirichlet characters mod n with values in R vanihses if a ≠ b and has the value n.totient if a = b.