NumberFieldFrobeniusRestriction.lean

1 import PaperX.NumberFieldPrimeRestriction
2 
3 /-! Restriction of an actual absolute arithmetic Frobenius element to an
4 arbitrary normal number field. The prime downstairs is the contraction of the
5 same absolute prime. Decomposition membership, the arithmetic p-power residue
6 action, and inertia membership are transported along the chosen integral
7 embedding. The existence statements construct one simultaneous absolute and
8 finite witness; no finite Frobenius witness is assumed separately. -/
9 set_option autoImplicit false
10 noncomputable section
11 namespace PaperX.NumberFieldFrobeniusRestriction
12 open NumberField AbsoluteIntegralFrobenius NumberFieldPrimeRestriction
13 open scoped Pointwise
14 
15 variable (L : Type*) [Field L] [NumberField L] [Normal ℚ L]
16   (Q : Ideal IntegralClosure)
17 
18 /-- Absolute decomposition elements restrict to the decomposition group of the
19 actual contracted prime. No maximality assumption is needed for this transfer. -/
20 theorem restriction_mem_stabilizer (γ : GQ)
21     (hγ : γ ∈ MulAction.stabilizer GQ Q) :
22     AbsoluteGaloisRestriction.restriction L γ ∈
23       MulAction.stabilizer Gal(L/ℚ) (restrictedPrime L Q) := by
24   apply MulAction.mem_stabilizer_iff.mpr
25   ext x
26   rw [Ideal.mem_pointwise_smul_iff_inv_smul_mem]
27   change integralEmbedding L ((AbsoluteGaloisRestriction.restriction L γ)⁻¹ • x) ∈ Q ↔
28     integralEmbedding L x ∈ Q
29   rw [← (AbsoluteGaloisRestriction.restriction L).map_inv
30     (show Field.absoluteGaloisGroup ℚ from γ)]
31   change integralEmbedding L (AbsoluteGaloisRestriction.restriction L (γ⁻¹) • x) ∈ Q ↔
32     integralEmbedding L x ∈ Q
33   erw [integralEmbedding_smul L (γ⁻¹) x]
34   have hinv : γ⁻¹ • Q = Q :=
35     MulAction.mem_stabilizer_iff.mp ((MulAction.stabilizer GQ Q).inv_mem hγ)
36   simpa only [hinv] using
37     (Ideal.smul_mem_pointwise_smul_iff (a := γ⁻¹) (S := Q) (x := integralEmbedding L x))
38 
39 /-- Absolute ideal inertia restricts into the actual finite ideal inertia. -/
40 theorem restriction_mem_inertia (γ : GQ) (hγ : γ ∈ Q.inertia GQ) :
41     AbsoluteGaloisRestriction.restriction L γ ∈
42       (restrictedPrime L Q).inertia Gal(L/ℚ) := by
43   intro x
44   change integralEmbedding L (AbsoluteGaloisRestriction.restriction L γ • x - x) ∈ Q
45   rw [map_sub, integralEmbedding_smul]
46   exact hγ (integralEmbedding L x)
47 
48 /-- An arithmetic p-power residue action restricts to the same arithmetic
49 p-power action on the actual residue field of the contracted prime. -/
50 theorem restriction_residue_power (p : ℕ) (γ : GQ)
51     (hγ : ∀ x : IntegralClosure, Ideal.Quotient.mk Q (γ • x) =
52       (Ideal.Quotient.mk Q x) ^ p) :
53     ∀ x : 𝓞 L,
54       Ideal.Quotient.mk (restrictedPrime L Q) (AbsoluteGaloisRestriction.restriction L γ • x) =
55         (Ideal.Quotient.mk (restrictedPrime L Q) x) ^ p := by
56   intro x
57   rw [← map_pow]
58   apply Ideal.Quotient.eq.mpr
59   change integralEmbedding L (AbsoluteGaloisRestriction.restriction L γ • x - x ^ p) ∈ Q
60   rw [map_sub, integralEmbedding_smul, map_pow]
61   apply Ideal.Quotient.eq.mp
62   simpa only [map_pow] using hγ (integralEmbedding L x)
63 
64 /-- Actual arithmetic Frobenius data restrict together to the contracted prime. -/
65 theorem restriction_arithmeticFrobenius (p : ℕ) (γ : GQ)
66     (hstab : γ ∈ MulAction.stabilizer GQ Q)
67     (hres : ∀ x : IntegralClosure, Ideal.Quotient.mk Q (γ • x) =
68       (Ideal.Quotient.mk Q x) ^ p) :
69     AbsoluteGaloisRestriction.restriction L γ ∈
70         MulAction.stabilizer Gal(L/ℚ) (restrictedPrime L Q) ∧
71       ∀ x : 𝓞 L,
72         Ideal.Quotient.mk (restrictedPrime L Q) (AbsoluteGaloisRestriction.restriction L γ • x) =
73           (Ideal.Quotient.mk (restrictedPrime L Q) x) ^ p :=
74   ⟨restriction_mem_stabilizer L Q γ hstab, restriction_residue_power L Q p γ hres⟩
75 
76 /-- At any supplied actual maximal ideal above p, the constructed absolute
77 Frobenius also gives a finite Frobenius at its contraction. The same element
78 and the same contracted prime occur in both conclusions. -/
79 theorem exists_simultaneous_frobenius_at (p : ℕ) [Fact p.Prime]
80     [Q.IsMaximal] [Q.LiesOver (Ideal.span {(p : ℤ)})] :
81     ∃ γ : GQ, γ ∈ MulAction.stabilizer GQ Q ∧
82       (∀ x : IntegralClosure, Ideal.Quotient.mk Q (γ • x) =
83         (Ideal.Quotient.mk Q x) ^ p) ∧
84       AbsoluteGaloisRestriction.restriction L γ ∈
85         MulAction.stabilizer Gal(L/ℚ) (restrictedPrime L Q) ∧
86       ∀ x : 𝓞 L,
87         Ideal.Quotient.mk (restrictedPrime L Q) (AbsoluteGaloisRestriction.restriction L γ • x) =
88           (Ideal.Quotient.mk (restrictedPrime L Q) x) ^ p := by
89   obtain ⟨γ, hγ⟩ := AbsoluteIntegralFrobenius.exists_frobenius_at p Q
90   exact ⟨γ.val, γ.property, hγ, restriction_arithmeticFrobenius L Q p γ.val γ.property hγ⟩
91 
92 omit Q in
93 /-- For each rational prime, construct an actual absolute prime, its actual
94 maximal contraction to the number field, and a single absolute element which
95 has arithmetic Frobenius action at both primes. This does not assert that the
96 prime is unramified or that any prescribed finite automorphism occurs. -/
97 theorem exists_simultaneous_frobenius (p : ℕ) [Fact p.Prime] :
98     ∃ Q : Ideal IntegralClosure,
99       Q.IsMaximal ∧ Q.LiesOver (Ideal.span {(p : ℤ)}) ∧
100       (restrictedPrime L Q).IsMaximal ∧
101       (restrictedPrime L Q).LiesOver (Ideal.span {(p : ℤ)}) ∧
102       ∃ γ : GQ, γ ∈ MulAction.stabilizer GQ Q ∧
103         (∀ x : IntegralClosure, Ideal.Quotient.mk Q (γ • x) =
104           (Ideal.Quotient.mk Q x) ^ p) ∧
105         AbsoluteGaloisRestriction.restriction L γ ∈
106           MulAction.stabilizer Gal(L/ℚ) (restrictedPrime L Q) ∧
107         ∀ x : 𝓞 L,
108           Ideal.Quotient.mk (restrictedPrime L Q) (AbsoluteGaloisRestriction.restriction L γ • x) =
109             (Ideal.Quotient.mk (restrictedPrime L Q) x) ^ p := by
110   obtain ⟨Q, hmax, hover, γ, hγ⟩ := AbsoluteIntegralFrobenius.exists_frobenius p
111   let : Q.IsMaximal := hmax
112   let : Q.LiesOver (Ideal.span {(p : ℤ)}) := hover
113   exact ⟨Q, hmax, hover, restrictedPrime_isMaximal L p Q,
114     restrictedPrime_liesOver L p Q, γ.val, γ.property, hγ,
115     restriction_arithmeticFrobenius L Q p γ.val γ.property hγ⟩
116 
117 end PaperX.NumberFieldFrobeniusRestriction

Back to source controls