Skip to content

Commit d6ac8e9

Browse files
MichaelStollBayreuthMichaelStollBayreuth
committed
feat(NumberTheory/MulChar): extend API for multiplicative characters (#13939)
This adds some more API lemmas for multiplicative characters.
1 parent 7052367 commit d6ac8e9

File tree

3 files changed

+242
-0
lines changed

3 files changed

+242
-0
lines changed

‎Mathlib.lean‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -3304,6 +3304,7 @@ import Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
33043304
import Mathlib.NumberTheory.ModularForms.SlashActions
33053305
import Mathlib.NumberTheory.ModularForms.SlashInvariantForms
33063306
import Mathlib.NumberTheory.MulChar.Basic
3307+
import Mathlib.NumberTheory.MulChar.Lemmas
33073308
import Mathlib.NumberTheory.Multiplicity
33083309
import Mathlib.NumberTheory.NumberField.Basic
33093310
import Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

‎Mathlib/NumberTheory/MulChar/Basic.lean‎

Lines changed: 21 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -476,6 +476,27 @@ def ringHomComp (χ : MulChar R R') (f : R' →+* R'') : MulChar R R'' :=
476476
map_nonunit' := fun a ha => by simp only [map_nonunit χ ha, map_zero] }
477477
#align mul_char.ring_hom_comp MulChar.ringHomComp
478478

479+
@[simp]
480+
lemma ringHomComp_one (f : R' →+* R'') : (1 : MulChar R R').ringHomComp f = 1 := by
481+
ext1
482+
simp only [MulChar.ringHomComp_apply, MulChar.one_apply_coe, map_one]
483+
484+
lemma ringHomComp_inv {R : Type*} [CommRing R] (χ : MulChar R R') (f : R' →+* R'') :
485+
(χ.ringHomComp f)⁻¹ = χ⁻¹.ringHomComp f := by
486+
ext1
487+
simp only [inv_apply, Ring.inverse_unit, ringHomComp_apply]
488+
489+
lemma ringHomComp_mul (χ φ : MulChar R R') (f : R' →+* R'') :
490+
(χ * φ).ringHomComp f = χ.ringHomComp f * φ.ringHomComp f := by
491+
ext1
492+
simp only [ringHomComp_apply, coeToFun_mul, Pi.mul_apply, map_mul]
493+
494+
lemma ringHomComp_pow (χ : MulChar R R') (f : R' →+* R'') (n : ℕ) :
495+
χ.ringHomComp f ^ n = (χ ^ n).ringHomComp f := by
496+
induction n
497+
case zero => simp only [pow_zero, ringHomComp_one]
498+
case succ n ih => simp only [pow_succ, ih, ringHomComp_mul]
499+
479500
lemma injective_ringHomComp {f : R' →+* R''} (hf : Function.Injective f) :
480501
Function.Injective (ringHomComp (R := R) · f) := by
481502
simpa only [Function.Injective, ext_iff, ringHomComp, coe_mk, MonoidHom.coe_mk, OneHom.coe_mk]

‎Mathlib/NumberTheory/MulChar/Lemmas.lean‎

Lines changed: 220 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,220 @@
1+
/-
2+
Copyright (c) 2024 Michael Stoll. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Michael Stoll
5+
-/
6+
import Mathlib.NumberTheory.MulChar.Basic
7+
import Mathlib.RingTheory.Ideal.LocalRing
8+
import Mathlib.RingTheory.RootsOfUnity.Complex
9+
10+
/-!
11+
# Further Results on multiplicative characters
12+
-/
13+
14+
namespace MulChar
15+
16+
/-- Two multiplicative characters on a monoid whose unit group is generated by `g`
17+
are equal if and only if they agree on `g`. -/
18+
lemma eq_iff {R R' : Type*} [CommMonoid R] [CommMonoidWithZero R'] {g : Rˣ}
19+
(hg : ∀ x, x ∈ Subgroup.zpowers g) (χ₁ χ₂ : MulChar R R') :
20+
χ₁ = χ₂ ↔ χ₁ g.val = χ₂ g.val := by
21+
rw [← Equiv.apply_eq_iff_eq equivToUnitHom, MonoidHom.eq_iff_eq_on_generator hg,
22+
← coe_equivToUnitHom, ← coe_equivToUnitHom, Units.ext_iff]
23+
24+
25+
section Ring
26+
27+
variable {R R' : Type*} [CommRing R] [CommRing R']
28+
29+
/-- Define the conjugation (`star`) of a multiplicative character by conjugating pointwise. -/
30+
@[simps!]
31+
def starComp [StarRing R'] (χ : MulChar R R') : MulChar R R' :=
32+
χ.ringHomComp (starRingEnd R')
33+
34+
instance instStarMul [StarRing R'] : StarMul (MulChar R R') where
35+
star := starComp
36+
star_involutive χ := by
37+
ext1
38+
simp only [starComp_apply, RingHomCompTriple.comp_apply, RingHom.id_apply]
39+
star_mul χ χ' := by
40+
ext1
41+
simp only [starComp_apply, starRingEnd, coeToFun_mul, Pi.mul_apply, map_mul, RingHom.coe_coe,
42+
starRingAut_apply, mul_comm]
43+
44+
@[simp]
45+
lemma star_apply [StarRing R'] (χ : MulChar R R') (a : R) : (star χ) a = star (χ a) :=
46+
rfl
47+
48+
variable [Fintype R] [DecidableEq R]
49+
50+
/-- The values of a multiplicative character on `R` are `n`th roots of unity, where `n = #Rˣ`. -/
51+
lemma apply_mem_rootsOfUnity (a : Rˣ) {χ : MulChar R R'} :
52+
equivToUnitHom χ a ∈ rootsOfUnity ⟨Fintype.card Rˣ, Fintype.card_pos⟩ R' := by
53+
rw [mem_rootsOfUnity, ← map_pow, ← (equivToUnitHom χ).map_one, PNat.mk_coe, pow_card_eq_one]
54+
55+
open Complex in
56+
/-- The conjugate of a multiplicative character with values in `ℂ` is its inverse. -/
57+
lemma star_eq_inv (χ : MulChar R ℂ) : star χ = χ⁻¹ := by
58+
ext1 a
59+
simp only [inv_apply_eq_inv']
60+
exact (inv_eq_conj <| norm_eq_one_of_mem_rootsOfUnity <| χ.apply_mem_rootsOfUnity a).symm
61+
62+
lemma star_apply' (χ : MulChar R ℂ) (a : R) : star (χ a) = χ⁻¹ a := by
63+
simp only [RCLike.star_def, ← star_eq_inv, star_apply]
64+
65+
end Ring
66+
67+
section IsCyclic
68+
69+
/-!
70+
### Multiplicative characters on finite monoids with cyclic unit group
71+
-/
72+
73+
variable {M : Type*} [CommMonoid M] [Fintype M] [DecidableEq M]
74+
variable {R : Type*} [CommMonoidWithZero R]
75+
76+
77+
variable (M) in
78+
/-- The order of the unit group of a finite monoid as a `PNat` (for use in `rootsOfUnity`). -/
79+
abbrev Monoid.orderUnits : ℕ+ := ⟨Fintype.card Mˣ, Fintype.card_pos⟩
80+
81+
/-- Given a finite monoid `M` with unit group `Mˣ` cyclic of order `n` and an `n`th root of
82+
unity `ζ` in `R`, there is a multiplicative character `M → R` that sends a given generator
83+
of `Mˣ` to `ζ`. -/
84+
noncomputable def ofRootOfUnity {ζ : Rˣ} (hζ : ζ ∈ rootsOfUnity (Monoid.orderUnits M) R)
85+
{g : Mˣ} (hg : ∀ x, x ∈ Subgroup.zpowers g) :
86+
MulChar M R := by
87+
have : orderOf ζ ∣ Monoid.orderUnits M :=
88+
orderOf_dvd_iff_pow_eq_one.mpr <| (mem_rootsOfUnity _ ζ).mp hζ
89+
refine ofUnitHom <| monoidHomOfForallMemZpowers hg <| this.trans <| dvd_of_eq ?_
90+
rw [orderOf_generator_eq_natCard hg, Nat.card_eq_fintype_card, PNat.mk_coe]
91+
92+
lemma ofRootOfUnity_spec {ζ : Rˣ} (hζ : ζ ∈ rootsOfUnity (Monoid.orderUnits M) R)
93+
{g : Mˣ} (hg : ∀ x, x ∈ Subgroup.zpowers g) :
94+
ofRootOfUnity hζ hg g = ζ := by
95+
simp only [ofRootOfUnity, ofUnitHom_eq, equivToUnitHom_symm_coe,
96+
monoidHomOfForallMemZpowers_apply_gen]
97+
98+
variable (M R) in
99+
/-- The group of multiplicative characters on a finite monoid `M` with cyclic unit group `Mˣ`
100+
of order `n` is isomorphic to the group of `n`th roots of unity in the target `R`. -/
101+
noncomputable def equiv_rootsOfUnity [inst_cyc : IsCyclic Mˣ] :
102+
MulChar M R ≃* rootsOfUnity (Monoid.orderUnits M) R where
103+
toFun χ :=
104+
⟨χ.toUnitHom <| Classical.choose inst_cyc.exists_generator, by
105+
simp only [toUnitHom_eq, mem_rootsOfUnity, PNat.mk_coe, ← map_pow, pow_card_eq_one, map_one]⟩
106+
invFun ζ := ofRootOfUnity ζ.prop <| Classical.choose_spec inst_cyc.exists_generator
107+
left_inv χ := by
108+
simp only [toUnitHom_eq, eq_iff <| Classical.choose_spec inst_cyc.exists_generator,
109+
ofRootOfUnity_spec, coe_equivToUnitHom]
110+
right_inv ζ := by
111+
ext
112+
simp only [toUnitHom_eq, coe_equivToUnitHom, ofRootOfUnity_spec]
113+
map_mul' x y := by
114+
simp only [toUnitHom_eq, equivToUnitHom_mul_apply, Submonoid.mk_mul_mk]
115+
116+
end IsCyclic
117+
118+
section FiniteField
119+
120+
/-!
121+
### Multiplicative characters on finite fields
122+
-/
123+
124+
variable (F : Type*) [Field F] [Fintype F] [DecidableEq F]
125+
variable {R : Type*} [CommRing R]
126+
127+
/-- There is a character of order `n` on `F` if `#F ≡ 1 mod n` and the target contains
128+
a primitive `n`th root of unity. -/
129+
lemma exists_mulChar_orderOf {n : ℕ} (h : n ∣ Fintype.card F - 1) {ζ : R}
130+
(hζ : IsPrimitiveRoot ζ n) :
131+
∃ χ : MulChar F R, orderOf χ = n := by
132+
have hn₀ : 0 < n := by
133+
refine Nat.pos_of_ne_zero fun hn ↦ ?_
134+
simp only [hn, zero_dvd_iff, Nat.sub_eq_zero_iff_le] at h
135+
exact (Fintype.one_lt_card.trans_le h).false
136+
let e := MulChar.equiv_rootsOfUnity F R
137+
let ζ' : Rˣ := (hζ.isUnit hn₀).unit
138+
have h' : ζ' ^ (Monoid.orderUnits F : ℕ) = 1 := by
139+
have hn : n ∣ Monoid.orderUnits F := by
140+
rwa [Monoid.orderUnits, PNat.mk_coe, Fintype.card_units]
141+
exact Units.ext_iff.mpr <| (IsPrimitiveRoot.pow_eq_one_iff_dvd hζ _).mpr hn
142+
use e.symm ⟨ζ', (mem_rootsOfUnity (Monoid.orderUnits F) ζ').mpr h'⟩
143+
rw [e.symm.orderOf_eq, orderOf_eq_iff hn₀]
144+
refine ⟨?_, fun m hm hm₀ h ↦ ?_⟩
145+
· ext
146+
push_cast
147+
exact hζ.pow_eq_one
148+
· rw [Subtype.ext_iff, Units.ext_iff] at h
149+
push_cast at h
150+
exact ((Nat.le_of_dvd hm₀ <| hζ.dvd_of_pow_eq_one _ h).trans_lt hm).false
151+
152+
/-- If there is a multiplicative character of order `n` on `F`, then `#F ≡ 1 mod n`. -/
153+
lemma orderOf_dvd_card_sub_one (χ : MulChar F R) : orderOf χ ∣ Fintype.card F - 1 := by
154+
rw [← Fintype.card_units]
155+
exact orderOf_dvd_of_pow_eq_one χ.pow_card_eq_one
156+
157+
/-- There is always a character on `F` of order `#F-1` with values in a ring that has
158+
a primitive `(#F-1)`th root of unity. -/
159+
lemma exists_mulChar_orderOf_eq_card_units {ζ : R} (hζ : IsPrimitiveRoot ζ (Monoid.orderUnits F)) :
160+
∃ χ : MulChar F R, orderOf χ = Fintype.card Fˣ :=
161+
exists_mulChar_orderOf F (by rw [Fintype.card_units]) hζ
162+
163+
variable {F}
164+
165+
/- The non-zero values of a multiplicative character of order `n` are `n`th roots of unity. -/
166+
lemma apply_mem_rootsOfUnity_orderOf (χ : MulChar F R) {a : F} (ha : a ≠ 0) :
167+
∃ ζ ∈ rootsOfUnity ⟨orderOf χ, χ.orderOf_pos⟩ R, ζ = χ a := by
168+
have hu : IsUnit (χ a) := ha.isUnit.map χ
169+
refine ⟨hu.unit, ?_, IsUnit.unit_spec hu⟩
170+
rw [mem_rootsOfUnity, PNat.mk_coe, Units.ext_iff, Units.val_pow_eq_pow_val, Units.val_one,
171+
IsUnit.unit_spec, ← χ.pow_apply' χ.orderOf_pos.ne', pow_orderOf_eq_one,
172+
show a = (isUnit_iff_ne_zero.mpr ha).unit by simp only [IsUnit.unit_spec],
173+
MulChar.one_apply_coe]
174+
175+
/-- The non-zero values of a multiplicative character `χ` such that `χ^n = 1`
176+
are `n`th roots of unity. -/
177+
lemma apply_mem_rootsOfUnity_of_pow_eq_one {χ : MulChar F R} {n : ℕ} (hn : n ≠ 0) (hχ : χ ^ n = 1)
178+
{a : F} (ha : a ≠ 0) :
179+
∃ ζ ∈ rootsOfUnity ⟨n, Nat.pos_of_ne_zero hn⟩ R, ζ = χ a := by
180+
obtain ⟨μ, hμ₁, hμ₂⟩ := χ.apply_mem_rootsOfUnity_orderOf ha
181+
have hχ' : PNat.val ⟨orderOf χ, χ.orderOf_pos⟩ ∣ PNat.val ⟨n, Nat.pos_of_ne_zero hn⟩ :=
182+
orderOf_dvd_of_pow_eq_one hχ
183+
exact ⟨μ, rootsOfUnity_le_of_dvd (PNat.dvd_iff.mpr hχ') hμ₁, hμ₂⟩
184+
185+
-- Results involving primitive roots of unity require `R` to be an integral domain.
186+
variable [IsDomain R]
187+
188+
/-- If `χ` is a multiplicative character with `χ^n = 1` and `μ` is a primitive `n`th root
189+
of unity, then, for `a ≠ 0`, there is some `k` such that `χ a = μ^k`. -/
190+
lemma exists_apply_eq_pow {χ : MulChar F R} {n : ℕ} (hn : n ≠ 0) (hχ : χ ^ n = 1) {μ : R}
191+
(hμ : IsPrimitiveRoot μ n) {a : F} (ha : a ≠ 0) :
192+
∃ k < n, χ a = μ ^ k := by
193+
have hn' := Nat.pos_of_ne_zero hn
194+
obtain ⟨ζ, hζ₁, hζ₂⟩ := apply_mem_rootsOfUnity_of_pow_eq_one hn hχ ha
195+
have hζ' : ζ.val ^ n = 1 := (mem_rootsOfUnity' ⟨n, hn'⟩ ↑ζ).mp hζ₁
196+
obtain ⟨k, hk₁, hk₂⟩ := hμ.eq_pow_of_pow_eq_one hζ' hn'
197+
exact ⟨k, hk₁, (hζ₂ ▸ hk₂).symm⟩
198+
199+
/-- The values of a multiplicative character `χ` such that `χ^n = 1` are contained in `ℤ[μ]` when
200+
`μ` is a primitive `n`th root of unity. -/
201+
lemma apply_mem_algebraAdjoin_of_pow_eq_one {χ : MulChar F R} {n : ℕ} (hn : n ≠ 0) (hχ : χ ^ n = 1)
202+
{μ : R} (hμ : IsPrimitiveRoot μ n) (a : F) :
203+
χ a ∈ Algebra.adjoin ℤ {μ} := by
204+
rcases eq_or_ne a 0 with rfl | h
205+
· exact χ.map_zero ▸ Subalgebra.zero_mem _
206+
· obtain ⟨ζ, hζ₁, hζ₂⟩ := apply_mem_rootsOfUnity_of_pow_eq_one hn hχ h
207+
rw [mem_rootsOfUnity, Units.ext_iff, Units.val_pow_eq_pow_val] at hζ₁
208+
obtain ⟨k, _, hk⟩ := IsPrimitiveRoot.eq_pow_of_pow_eq_one hμ hζ₁ (Nat.pos_of_ne_zero hn)
209+
exact hζ₂ ▸ hk ▸ Subalgebra.pow_mem _ (Algebra.self_mem_adjoin_singleton ℤ μ) k
210+
211+
/-- The values of a multiplicative character of order `n` are contained in `ℤ[μ]` when
212+
`μ` is a primitive `n`th root of unity. -/
213+
lemma apply_mem_algebraAdjoin {χ : MulChar F R} {μ : R} (hμ : IsPrimitiveRoot μ (orderOf χ))
214+
(a : F) :
215+
χ a ∈ Algebra.adjoin ℤ {μ} :=
216+
apply_mem_algebraAdjoin_of_pow_eq_one χ.orderOf_pos.ne' (pow_orderOf_eq_one χ) hμ a
217+
218+
end FiniteField
219+
220+
end MulChar

0 commit comments

Comments
 (0)