FrobeniusChoiceIndependence.lean

1 import PaperX.AbsoluteFrobeniusWitnesses
2 
3 /-! Actual arithmetic Frobenius choices are conjugate modulo ideal inertia.
4 Their traces agree in a representation which kills that inertia. -/
5 set_option autoImplicit false
6 noncomputable section
7 namespace PaperX.FrobeniusChoiceIndependence
8 open PaperX.AbsoluteIntegralFrobenius PaperX.AbsoluteFrobeniusWitnesses
9 open scoped Pointwise
10 
11 local instance : TopologicalSpace IntegralClosure := ⊥
12 local instance : DiscreteTopology IntegralClosure := ⟨rfl⟩
13 attribute [local instance] continuous_integral_action
14 
15 /-- Two actual Frobenius choices at one rational prime are conjugate modulo
16 inertia, even when they use different primes of the algebraic integers. -/
17 theorem witnesses_conjugate_mod_inertia (p : ℕ) (u v : Witness p) :
18     ∃ a : GQ, v.primeIdeal = a • u.primeIdeal ∧
19       v.element⁻¹ * (a * u.element * a⁻¹) ∈ v.primeIdeal.inertia GQ := by
20   let : u.primeIdeal.IsMaximal := u.isMaximal
21   let : v.primeIdeal.IsMaximal := v.isMaximal
22   let : u.primeIdeal.LiesOver (Ideal.span {(p : ℤ)}) := u.liesOver
23   let : v.primeIdeal.LiesOver (Ideal.span {(p : ℤ)}) := v.liesOver
24   have heq : u.primeIdeal.under ℤ = v.primeIdeal.under ℤ := by
25     rw [← Ideal.over_def u.primeIdeal (Ideal.span {(p : ℤ)}),
26       ← Ideal.over_def v.primeIdeal (Ideal.span {(p : ℤ)})]
27   obtain ⟨a, ha⟩ := Algebra.IsInvariant.exists_smul_of_under_eq_of_profinite
28     (A := ℤ) (B := IntegralClosure) (G := GQ) u.primeIdeal v.primeIdeal heq
29   refine ⟨a, ha, same_residue_div_mem_inertia v.primeIdeal v.element
30     (a * u.element * a⁻¹) v.stabilizes ?_⟩
31   intro x
32   have h := residue_conjugate u.primeIdeal p u.element a u.residue x
33   rw [← ha] at h
34   exact h.trans (v.residue x).symm
35 
36 /-- Killing inertia makes the conjugated Frobenius operators equal. -/
37 theorem witness_operator_conjugacy {K V : Type*} [Field K] [AddCommGroup V] [Module K V]
38     (ρ : Representation K GQ V) (p : ℕ) (u v : Witness p)
39     (hunram : ∀ g ∈ v.primeIdeal.inertia GQ, ρ g = 1) :
40     ∃ a : GQ, ρ (a * u.element * a⁻¹) = ρ v.element := by
41   obtain ⟨a, _, ha⟩ := witnesses_conjugate_mod_inertia p u v
42   refine ⟨a, ?_⟩
43   have h := congrArg (fun z => ρ v.element * z) (hunram _ ha)
44   simpa only [← map_mul, mul_inv_cancel_left, mul_one] using h
45 
46 /-- The trace is independent of the actual prime and Frobenius lift once its
47 inertia acts trivially. -/
48 theorem witness_character_eq {K V : Type*} [Field K] [AddCommGroup V] [Module K V]
49     (ρ : Representation K GQ V) (p : ℕ) (u v : Witness p)
50     (hunram : ∀ g ∈ v.primeIdeal.inertia GQ, ρ g = 1) :
51     Representation.character ρ u.element = Representation.character ρ v.element := by
52   obtain ⟨a, ha⟩ := witness_operator_conjugacy ρ p u v hunram
53   rw [← Representation.char_conj ρ u.element a]
54   exact congrArg (LinearMap.trace K V) ha
55 
56 end PaperX.FrobeniusChoiceIndependence

Back to source controls