FiniteTameComparison.lean

1 import PaperXI.InducedTameProfile
2 import PaperXI.TameGaussNaturality
3 import PaperXI.TameTensorSource
4 
5 /-! Proposition 16.1: an explicit finite comparison package on genuine induced
6 representations. The local-Weil and standard Artin/epsilon-factor identifications
7 are intentionally NOT fields of this finite record and are not proved here. -/
8 set_option autoImplicit false
9 noncomputable section
10 namespace PaperXI.FiniteTameComparison
11 open Polynomial PaperXI.CyclicInduced
12 open PaperXI.GeneratedIrreducibility PaperXI.TameOrbitTransitivity
13 open scoped Classical BigOperators TensorProduct
14 
15 /-- A finite output record. The conductor fields are the declared finite sums,
16 not the standard arithmetic Swan/Artin conductors. -/
17 @[ext] structure Observables (M : ℕ) where
18   dimension : ℕ
19   inertiaSupport : Set (ZMod M)
20   cyclePolynomial : ℂ[X]
21   localPolynomial : ℂ[X]
22   finiteSwan : ℚ
23   finiteArtin : ℚ
24   residuePhase : ℂ
25 
26 variable {G k : Type*} [Group G] [Field k] [Fintype k]
27 variable {M : ℕ} [NeZero M]
28 variable (δ : G →* Multiplicative ℤ) (ι : Multiplicative (ZMod M) →* G)
29 variable (φ : G) (hφ : δ φ = Multiplicative.ofAdd (1 : ℤ))
30 variable (n : ℕ) [NeZero n] (ξ : TameDegree.degreeSubgroup δ n →* ℂˣ)
31 variable (q : (ZMod M)ˣ) (j : ZMod M)
32 variable (hrel : φ⁻¹ * ι (Multiplicative.ofAdd (1 : ZMod M)) * φ =
33   ι (Multiplicative.ofAdd (q : ZMod M)))
34 variable (hξ : ∀ a : ZMod M,
35   (ξ (InducedTameProfile.inertiaInDegree δ ι n (Multiplicative.ofAdd a)) : ℂ) =
36     ZMod.stdAddChar (j * a))
37 variable [FiniteDimensional ℂ (DegreeIndSpace δ n ξ)]
38 
39 /-- Observations use actual spaces, operators, and character sums. -/
40 def observed (S : Finset ℕ) (J : ℕ → Subgroup G) (w : ℕ → ℚ)
41     (χ : kˣ →* ℂˣ) (ψ : AddChar k ℂ) : Observables M where
42   dimension := Module.finrank ℂ (DegreeIndSpace δ n ξ)
43   inertiaSupport := {b | PacketTransport.packet (tameRestriction (degreeInduced δ n ξ) ι) b ≠ ⊥}
44   cyclePolynomial := (degreeInduced δ n ξ φ).charpoly
45   localPolynomial := InvariantPolynomial.localPolynomial
46     (tameRestriction (degreeInduced δ n ξ) ι) (actionEquiv (degreeInduced δ n ξ) φ) q
47     (geometric_relation (degreeInduced δ n ξ) ι φ q hrel)
48   finiteSwan := TameConductor.finiteSwan (degreeInduced δ n ξ) S J w
49   finiteArtin := TameConductor.finiteArtin (degreeInduced δ n ξ) ι S J w
50   residuePhase := GaussCharacters.phase χ ψ
51 
52 /-- Prediction from packet coordinates and the declared residue/additive characters. -/
53 def fromCoordinates (c : ℂˣ) (χ : kˣ →* ℂˣ) (ψ : AddChar k ℂ) : Observables M where
54   dimension := n
55   inertiaSupport := {b | ∃ i : Fin n, ((q ^ (i : ℕ) : (ZMod M)ˣ) : ZMod M) * j = b}
56   cyclePolynomial := X ^ n - C (c : ℂ)
57   localPolynomial := if j = 0 then 1 - C (c : ℂ) * X ^ n else 1
58   finiteSwan := 0
59   finiteArtin := if j = 0 then 0 else n
60   residuePhase := (∑ x : kˣ, (χ x : ℂ) * ψ x) / (Real.sqrt (Fintype.card k) : ℂ)
61 
62 include hφ hξ in
63 /-- The complete finite record is derived, not included as input data. -/
64 theorem observations_eq_coordinates (P : Subgroup G)
65     (hP : ∀ g ∈ P, ∀ v, degreeInduced δ n ξ g v = v)
66     (S : Finset ℕ) (J : ℕ → Subgroup G) (w : ℕ → ℚ)
67     (hJP : ∀ r ∈ S, J r ≤ P) (χ : kˣ →* ℂˣ) (ψ : AddChar k ℂ) :
68     observed δ ι φ n ξ q hrel S J w χ ψ =
69       fromCoordinates n q j (InducedCycleInvariants.returnScalar δ φ hφ n ξ) χ ψ := by
70   apply Observables.ext
71   · exact InducedCycleInvariants.dimension δ φ hφ n ξ
72   · apply Set.ext
73     intro b
74     exact InducedTameProfile.inertia_support δ ι φ hφ n ξ q j hrel hξ b
75   · exact (InducedCycleInvariants.cycle_invariants δ φ hφ n ξ).1
76   · exact InducedTameProfile.local_polynomial δ ι φ hφ n ξ q j hrel hξ
77   · exact (InducedTameProfile.finite_conductors δ ι φ hφ n ξ q j hrel hξ P hP S J w hJP).1
78   · exact (InducedTameProfile.finite_conductors δ ι φ hφ n ξ q j hrel hξ P hP S J w hJP).2
79   · rfl
80 
81 /-- The tensor part of the package is an actual constructed equivalence of
82 representations; it is not encoded merely as matching dimensions. -/
83 def interactionEquiv (m : ℕ) [NeZero m] (η : TameDegree.degreeSubgroup δ m →* ℂˣ) :
84     Representation.Equiv ((degreeInduced δ n ξ).tprod (degreeInduced δ m η))
85       (Representation.directSum (fun i : Fin (Nat.gcd n m) =>
86         degreeInduced δ (Nat.lcm n m) (TameTensorSource.interactionCharacter δ φ n m ξ η i))) :=
87   TameTensorSource.decomposition δ φ n m ξ η hφ
88 
89 include hφ hξ in
90 /-- Source-facing finite package with all six advertised components. The final
91 residue magnitude includes the trivial-character exception. Its interpretation
92 as the arithmetic package still requires the separate local-field attachment. -/
93 theorem finite_comparison_package (P : Subgroup G)
94     (hP : ∀ g ∈ P, ∀ v, degreeInduced δ n ξ g v = v)
95     (S : Finset ℕ) (J : ℕ → Subgroup G) (w : ℕ → ℚ)
96     (hJP : ∀ r ∈ S, J r ≤ P)
97     (m : ℕ) [NeZero m] (η : TameDegree.degreeSubgroup δ m →* ℂˣ)
98     (χ : kˣ →* ℂˣ) (ψ : AddChar k ℂ) (hψ : ψ ≠ 1) :
99     observed δ ι φ n ξ q hrel S J w χ ψ =
100       fromCoordinates n q j (InducedCycleInvariants.returnScalar δ φ hφ n ξ) χ ψ ∧
101     Nonempty (Representation.Equiv ((degreeInduced δ n ξ).tprod (degreeInduced δ m η))
102       (Representation.directSum (fun i : Fin (Nat.gcd n m) =>
103         degreeInduced δ (Nat.lcm n m) (TameTensorSource.interactionCharacter δ φ n m ξ η i)))) ∧
104     (∑ i : Fin (Nat.gcd n m), Module.finrank ℂ (DegreeIndSpace δ (Nat.lcm n m)
105       (TameTensorSource.interactionCharacter δ φ n m ξ η i))) = n*m ∧
106     ‖GaussCharacters.phase χ ψ‖ =
107       if χ = 1 then (Real.sqrt (Fintype.card k))⁻¹ else 1 := by
108   exact ⟨observations_eq_coordinates δ ι φ hφ n ξ q j hrel hξ P hP S J w hJP χ ψ,
109     ⟨interactionEquiv δ φ hφ n ξ m η⟩,
110     TameTensorSource.interaction_dimension_sum δ φ n m ξ η hφ,
111     TameGaussNaturality.phase_norm_cases χ hψ⟩
112 
113 end PaperXI.FiniteTameComparison

Back to source controls