CyclotomicAbsoluteSamples.lean

1 import PaperX.AbsoluteGaloisRestriction
2 import PaperX.CyclotomicFrobeniusPrimes
3 import Mathlib.RepresentationTheory.Character
4 
5 /-! Global lifts of the finite cyclotomic arithmetic samples. The lifts are
6 actual absolute-Galois elements, but no membership in an absolute decomposition
7 group is asserted. Representations factoring through the finite field take
8 the same value on every lift. -/
9 set_option autoImplicit false
10 noncomputable section
11 namespace PaperX.CyclotomicAbsoluteSamples
12 open PaperX.AbsoluteGaloisRestriction PaperX.CyclotomicPrimeCoverage
13 open NumberField
14 open scoped Pointwise
15 
16 variable (n : ℕ) [NeZero n] (L : Type*) [Field L] [NumberField L]
17   [IsCyclotomicExtension {n} ℚ L]
18 
19 /-- The restriction map with normality derived from the cyclotomic hypothesis. -/
20 def restrictionMap : Field.absoluteGaloisGroup ℚ →* Gal(L/ℚ) := by
21   let : IsGalois ℚ L := IsCyclotomicExtension.isGalois {n} ℚ L
22   exact restriction L
23 
24 /-- The chosen field embedding used by the actual restriction. -/
25 def fieldEmbedding : L →ₐ[ℚ] AlgebraicClosure ℚ := by
26   let : IsGalois ℚ L := IsCyclotomicExtension.isGalois {n} ℚ L
27   exact embedding L
28 
29 omit [NeZero n] in
30 theorem restrictionMap_surjective : Function.Surjective (restrictionMap n L) := by
31   let : IsGalois ℚ L := IsCyclotomicExtension.isGalois {n} ℚ L
32   exact restriction_surjective L
33 
34 omit [NeZero n] in
35 theorem restrictionMap_continuous : Continuous (restrictionMap n L) := by
36   let : IsGalois ℚ L := IsCyclotomicExtension.isGalois {n} ℚ L
37   exact restriction_continuous L
38 
39 omit [NeZero n] in
40 theorem restrictionMap_commutes (γ : Field.absoluteGaloisGroup ℚ) (x : L) :
41     fieldEmbedding n L (restrictionMap n L γ x) =
42       (show Gal(AlgebraicClosure ℚ/ℚ) from γ) (fieldEmbedding n L x) := by
43   let : IsGalois ℚ L := IsCyclotomicExtension.isGalois {n} ℚ L
44   exact restriction_commutes L γ x
45 
46 /-- A chosen global lift, with no assertion that this choice belongs to a
47 specified absolute decomposition subgroup. -/
48 def liftSample (p : PermittedPrime n ∅) : Field.absoluteGaloisGroup ℚ :=
49   (restrictionMap_surjective n L (primeSample n L ∅ p)).choose
50 
51 @[simp] theorem restriction_liftSample (p : PermittedPrime n ∅) :
52     restrictionMap n L (liftSample n L p) = primeSample n L ∅ p :=
53   (restrictionMap_surjective n L (primeSample n L ∅ p)).choose_spec
54 
55 /-- The chosen global element acts by the arithmetic power on every embedded
56 n-th root of unity in the finite field. -/
57 theorem liftSample_apply_root (p : PermittedPrime n ∅) (x : L) (hx : x ^ n = 1) :
58     (show Gal(AlgebraicClosure ℚ/ℚ) from liftSample n L p) (fieldEmbedding n L x) = (fieldEmbedding n L x) ^ p.val := by
59   rw [← restrictionMap_commutes n L, restriction_liftSample,
60     primeSample, primePowerAutomorphism_apply n L p.val p.property.2.1 hx, map_pow]
61 
62 /-- Every lift restricts to the proved arithmetic Frobenius at an actual
63 unramified prime ideal of the finite cyclotomic field. This conclusion is about
64 that finite field, and does not assert absolute decomposition membership. -/
65 theorem lift_restriction_has_prime_witness (p : PermittedPrime n ∅)
66     (γ : Field.absoluteGaloisGroup ℚ) (hγ : restrictionMap n L γ = primeSample n L ∅ p) :
67     ∃ P : Ideal (𝓞 L), P.IsMaximal ∧ P.LiesOver (Ideal.span {(p.val : ℤ)}) ∧
68       Ideal.ramificationIdx P ℤ = 1 ∧
69       restrictionMap n L γ ∈ MulAction.stabilizer Gal(L/ℚ) P ∧
70       ∀ x : 𝓞 L, Ideal.Quotient.mk P (restrictionMap n L γ • x) =
71         (Ideal.Quotient.mk P x) ^ p.val := by
72   rw [hγ]
73   exact PaperX.CyclotomicFrobeniusPrimes.permitted_prime_has_frobenius_witness n L ∅ p
74 
75 section Representations
76 variable {K V : Type*} [Field K] [AddCommGroup V] [Module K V]
77 variable (ρ : Representation K Gal(L/ℚ) V)
78 
79 /-- The entire linear action, rather than only its trace, is independent of
80 the chosen global lift once the representation factors through the field. -/
81 theorem pullback_on_lift (p : PermittedPrime n ∅) (γ : Field.absoluteGaloisGroup ℚ)
82     (hγ : restrictionMap n L γ = primeSample n L ∅ p) :
83     (ρ.comp (restrictionMap n L)) γ = ρ (primeSample n L ∅ p) := by
84   change ρ (restrictionMap n L γ) = _
85   rw [hγ]
86 
87 theorem pullback_character_on_lift (p : PermittedPrime n ∅)
88     (γ : Field.absoluteGaloisGroup ℚ) (hγ : restrictionMap n L γ = primeSample n L ∅ p) :
89     Representation.character (ρ.comp (restrictionMap n L)) γ = ρ.character (primeSample n L ∅ p) := by
90   change LinearMap.trace K V ((ρ.comp (restrictionMap n L)) γ) = _
91   rw [pullback_on_lift n L ρ p γ hγ]
92   rfl
93 
94 end Representations
95 end PaperX.CyclotomicAbsoluteSamples

Back to source controls