TameNormPacket.lean

1 import PaperXI.TameExponent
2 
3 /-! Paper XI, Proposition 5.3. The interaction character is built from actual
4 finite-field norms, the actual Frobenius, and multiplication of characters.
5 Exponent coordinates on the two subfields come from one faithful common-field
6 character. Every pair of characters admits these compatible coordinates. -/
7 set_option autoImplicit false
8 noncomputable section
9 namespace PaperXI.TameNormPacket
10 
11 variable (K M L Q : Type*) [Field K] [Field M] [Field L] [Field Q]
12   [Finite K] [Finite M] [Finite L] [Fintype Q]
13   [Algebra K L] [Algebra M L] [Algebra Q M] [Algebra Q L]
14 
15 /-- The actual interaction character, with the second residue character shifted
16 by the chosen iterate of Frobenius before its norm lift. -/
17 def interaction (ξ : Kˣ →* ℂˣ) (η : Mˣ →* ℂˣ) (i : ℕ) : Lˣ →* ℂˣ :=
18   ξ.comp (TameNorm.norm K L) *
19     (η.comp (TameNorm.frobenius M Q i)).comp (TameNorm.norm M L)
20 
21 omit [Finite K] in
22 /-- Norm lifting, Frobenius, and character multiplication give the refined exponent. -/
23 theorem refined_exponent (χ : Lˣ →* ℂˣ) (a b i : ℕ) :
24     interaction K M L Q ((χ.comp (TameNorm.embedding K L)) ^ a)
25       ((χ.comp (TameNorm.embedding M L)) ^ b) i =
26     χ ^ (a * TameNorm.normExponent K L +
27       b * Fintype.card Q ^ i * TameNorm.normExponent M L) := by
28   unfold interaction
29   rw [TameNorm.norm_lift, TameNorm.shifted_lower_norm_lift]
30   exact TameExponent.product χ _ _
31 
32 omit [Finite K] in
33 /-- Triviality concerns the actual multiplicative character, and follows from
34 faithfulness rather than being assumed as an exponent-model axiom. -/
35 theorem refined_trivial_iff (χ : Lˣ →* ℂˣ) (hχ : Function.Injective χ)
36     (a b i : ℕ) :
37     interaction K M L Q ((χ.comp (TameNorm.embedding K L)) ^ a)
38       ((χ.comp (TameNorm.embedding M L)) ^ b) i = 1 ↔
39     ((a * TameNorm.normExponent K L +
40       b * Fintype.card Q ^ i * TameNorm.normExponent M L : ℕ) :
41         ZMod (Nat.card L - 1)) = 0 := by
42   rw [refined_exponent, TameExponent.pow_eq_one_iff χ hχ]
43 
44 omit [Finite K] in
45 /-- The boxed source formula for actual residue fields of sizes q^n, q^m, q^ell. -/
46 theorem source_formula (χ : Lˣ →* ℂˣ) (q n m ell : ℕ)
47     (hQ : Fintype.card Q = q) (hK : Nat.card K = q ^ n)
48     (hM : Nat.card M = q ^ m) (hL : Nat.card L = q ^ ell) (a b i : ℕ) :
49     interaction K M L Q ((χ.comp (TameNorm.embedding K L)) ^ a)
50       ((χ.comp (TameNorm.embedding M L)) ^ b) i =
51     χ ^ (a * ((q ^ ell - 1) / (q ^ n - 1)) +
52       b * q ^ i * ((q ^ ell - 1) / (q ^ m - 1))) := by
53   simpa only [TameNorm.normExponent, hQ, hK, hM, hL] using
54     refined_exponent K M L Q χ a b i
55 
56 omit [Finite K] in
57 /-- The source zero-exponent criterion in Z/(q^ell-1). -/
58 theorem source_trivial_iff (χ : Lˣ →* ℂˣ) (hχ : Function.Injective χ)
59     (q n m ell : ℕ) (hQ : Fintype.card Q = q) (hK : Nat.card K = q ^ n)
60     (hM : Nat.card M = q ^ m) (hL : Nat.card L = q ^ ell) (a b i : ℕ) :
61     interaction K M L Q ((χ.comp (TameNorm.embedding K L)) ^ a)
62       ((χ.comp (TameNorm.embedding M L)) ^ b) i = 1 ↔
63     ((a * ((q ^ ell - 1) / (q ^ n - 1)) +
64       b * q ^ i * ((q ^ ell - 1) / (q ^ m - 1)) : ℕ) :
65         ZMod (q ^ ell - 1)) = 0 := by
66   rw [source_formula K M L Q χ q n m ell hQ hK hM hL,
67     TameExponent.pow_eq_one_iff χ hχ, hL]
68 
69 omit [Finite K] [Finite M] [Finite L] [Fintype Q] [Algebra Q M] [Algebra Q L] in
70 /-- Compatible basic characters on the subfields are faithful. -/
71 theorem restricted_faithful (χ : Lˣ →* ℂˣ) (hχ : Function.Injective χ) :
72     Function.Injective (χ.comp (TameNorm.embedding K L)) ∧
73     Function.Injective (χ.comp (TameNorm.embedding M L)) :=
74   ⟨hχ.comp (TameNorm.embedding_injective K L),
75     hχ.comp (TameNorm.embedding_injective M L)⟩
76 
77 omit [Finite L] [Fintype Q] [Algebra Q M] [Algebra Q L] in
78 /-- Every given pair of residue characters admits compatible exponent coordinates;
79 no relation between independently chosen generators is postulated. -/
80 theorem exists_compatible_exponents (χ : Lˣ →* ℂˣ) (hχ : Function.Injective χ)
81     (ξ : Kˣ →* ℂˣ) (η : Mˣ →* ℂˣ) :
82     ∃ a < Nat.card K - 1, ∃ b < Nat.card M - 1,
83       ξ = (χ.comp (TameNorm.embedding K L)) ^ a ∧
84       η = (χ.comp (TameNorm.embedding M L)) ^ b := by
85   obtain ⟨a, ha, hξ⟩ := TameExponent.exists_exponent _
86     (restricted_faithful K M L χ hχ).1 ξ
87   obtain ⟨b, hb, hη⟩ := TameExponent.exists_exponent _
88     (restricted_faithful K M L χ hχ).2 η
89   exact ⟨a, ha, b, hb, hξ, hη⟩
90 
91 /-- Complete source-level existence statement, starting with arbitrary actual
92 characters and constructing a faithful coordinate system for every interaction. -/
93 theorem source (ξ : Kˣ →* ℂˣ) (η : Mˣ →* ℂˣ)
94     (q n m ell : ℕ) (hQ : Fintype.card Q = q) (hK : Nat.card K = q ^ n)
95     (hM : Nat.card M = q ^ m) (hL : Nat.card L = q ^ ell) :
96     ∃ χ : Lˣ →* ℂˣ, Function.Injective χ ∧
97       ∃ a < q ^ n - 1, ∃ b < q ^ m - 1,
98       ξ = (χ.comp (TameNorm.embedding K L)) ^ a ∧
99       η = (χ.comp (TameNorm.embedding M L)) ^ b ∧
100       ∀ i : ℕ,
101         interaction K M L Q ξ η i =
102           χ ^ (a * ((q ^ ell - 1) / (q ^ n - 1)) +
103             b * q ^ i * ((q ^ ell - 1) / (q ^ m - 1))) ∧
104         (interaction K M L Q ξ η i = 1 ↔
105           ((a * ((q ^ ell - 1) / (q ^ n - 1)) +
106             b * q ^ i * ((q ^ ell - 1) / (q ^ m - 1)) : ℕ) :
107               ZMod (q ^ ell - 1)) = 0) := by
108   let χ := TameExponent.faithfulCharacter L
109   have hχ := TameExponent.faithfulCharacter_injective L
110   obtain ⟨a, ha, b, hb, hξ, hη⟩ := exists_compatible_exponents K M L χ hχ ξ η
111   refine ⟨χ, hχ, a, by simpa only [hK] using ha,
112     b, by simpa only [hM] using hb, hξ, hη, ?_⟩
113   intro i
114   rw [hξ, hη]
115   exact ⟨source_formula K M L Q χ q n m ell hQ hK hM hL a b i,
116     source_trivial_iff K M L Q χ hχ q n m ell hQ hK hM hL a b i⟩
117 
118 end PaperXI.TameNormPacket

Back to source controls