NumberFieldWitnessIndependence.lean

1 import PaperX.FrobeniusChoiceIndependence
2 import PaperX.NumberFieldFrobeniusRestriction
3 import PaperX.UnramifiedFrobeniusUniqueness
4 
5 /-! Outside the discriminant, absolute Frobenius choices have conjugate
6 restrictions to any fixed finite normal number field. -/
7 set_option autoImplicit false
8 noncomputable section
9 namespace PaperX.NumberFieldWitnessIndependence
10 open PaperX.AbsoluteIntegralFrobenius PaperX.AbsoluteFrobeniusWitnesses
11 open PaperX.NumberFieldPrimeRestriction PaperX.NumberFieldFrobeniusRestriction
12 open PaperX.UnramifiedFrobeniusUniqueness
13 open scoped Pointwise
14 
15 variable (L : Type*) [Field L] [NumberField L] [Normal ℚ L]
16 
17 /-- The actual absolute inertia at p restricts trivially to a finite normal
18 number field whenever p is outside its discriminant primes. -/
19 theorem restriction_inertia_eq_one (p : ℕ) [Fact p.Prime] (v : Witness p)
20     (hp : p ∉ discriminantPrimes L) (g : GQ) (hg : g ∈ v.primeIdeal.inertia GQ) :
21     AbsoluteGaloisRestriction.restriction L g = 1 := by
22   let : v.primeIdeal.IsMaximal := v.isMaximal
23   let : v.primeIdeal.LiesOver (Ideal.span {(p : ℤ)}) := v.liesOver
24   let : (restrictedPrime L v.primeIdeal).IsMaximal := restrictedPrime_isMaximal L p v.primeIdeal
25   let : (restrictedPrime L v.primeIdeal).LiesOver (Ideal.span {(p : ℤ)}) :=
26     restrictedPrime_liesOver L p v.primeIdeal
27   have h := restriction_mem_inertia L v.primeIdeal g hg
28   rw [inertia_eq_bot_of_not_mem L p (restrictedPrime L v.primeIdeal) hp] at h
29   exact Subgroup.mem_bot.mp h
30 
31 /-- All actual choices at p give one finite Frobenius conjugacy class outside
32 the discriminant. -/
33 theorem restricted_witnesses_conjugate (p : ℕ) [Fact p.Prime] (u v : Witness p)
34     (hp : p ∉ discriminantPrimes L) :
35     ∃ a : Gal(L/ℚ),
36       a * AbsoluteGaloisRestriction.restriction L u.element * a⁻¹ =
37         AbsoluteGaloisRestriction.restriction L v.element := by
38   obtain ⟨a, _, ha⟩ := PaperX.FrobeniusChoiceIndependence.witnesses_conjugate_mod_inertia p u v
39   have h := restriction_inertia_eq_one L p v hp _ ha
40   let r : GQ →* Gal(L/ℚ) := AbsoluteGaloisRestriction.restriction L
41   change r (v.element⁻¹ * (a * u.element * a⁻¹)) = 1 at h
42   have h' := congrArg (fun z => r v.element * z) h
43   refine ⟨r a, ?_⟩
44   change r a * r u.element * (r a)⁻¹ = r v.element
45   simpa only [map_mul, map_inv, ← mul_assoc, mul_inv_cancel, one_mul, mul_one] using h'
46 
47 /-- Every representation factoring through the finite number field is actually
48 trivial on the inertia attached to the chosen absolute prime away from its
49 discriminant. -/
50 theorem pullback_inertia_eq_one {K V : Type*} [Field K] [AddCommGroup V] [Module K V]
51     (ρ : Representation K Gal(L/ℚ) V) (p : ℕ) [Fact p.Prime] (v : Witness p)
52     (hp : p ∉ discriminantPrimes L) (g : GQ) (hg : g ∈ v.primeIdeal.inertia GQ) :
53     (ρ.comp (AbsoluteGaloisRestriction.restriction L)) g = 1 := by
54   change ρ (AbsoluteGaloisRestriction.restriction L g) = 1
55   rw [restriction_inertia_eq_one L p v hp g hg, map_one]
56 
57 /-- The trace of a finite-field-factor representation is independent of the
58 actual arithmetic Frobenius choice outside the discriminant. -/
59 theorem pullback_witness_character_eq {K V : Type*} [Field K] [AddCommGroup V] [Module K V]
60     (ρ : Representation K Gal(L/ℚ) V) (p : ℕ) [Fact p.Prime] (u v : Witness p)
61     (hp : p ∉ discriminantPrimes L) :
62     Representation.character (ρ.comp (AbsoluteGaloisRestriction.restriction L)) u.element =
63       Representation.character (ρ.comp (AbsoluteGaloisRestriction.restriction L)) v.element := by
64   exact PaperX.FrobeniusChoiceIndependence.witness_character_eq _ p u v
65     (pullback_inertia_eq_one L ρ p v hp)
66 
67 end PaperX.NumberFieldWitnessIndependence

Back to source controls