CyclotomicFrobeniusPrimes.lean

1 import PaperX.CyclotomicPrimeCoverage
2 
3 /-! Existence of actual primes above the rational prime samples. Lying-over
4 supplies maximal ideals of the ring of integers; the preceding module then
5 proves unramifiedness and the arithmetic Frobenius residue action there. -/
6 set_option autoImplicit false
7 noncomputable section
8 namespace PaperX.CyclotomicFrobeniusPrimes
9 open NumberField PaperX.CyclotomicPrimeCoverage
10 open scoped Pointwise
11 
12 variable (n : ℕ) [NeZero n] (K : Type*) [Field K] [NumberField K]
13   [IsCyclotomicExtension {n} ℚ K]
14 
15 /-- Every rational prime coprime to the conductor has an actual maximal ideal
16 above it witnessing the unramified arithmetic Frobenius property. -/
17 theorem exists_prime_above_with_frobenius (p : ℕ) [Fact (Nat.Prime p)]
18     (hp : p.Coprime n) :
19     ∃ P : Ideal (𝓞 K), P.IsMaximal ∧ P.LiesOver (Ideal.span {(p : ℤ)}) ∧
20       Ideal.ramificationIdx P ℤ = 1 ∧
21       primePowerAutomorphism n K p hp ∈ MulAction.stabilizer Gal(K/ℚ) P ∧
22       ∀ x : 𝓞 K, Ideal.Quotient.mk P (primePowerAutomorphism n K p hp • x) =
23         (Ideal.Quotient.mk P x) ^ p := by
24   let : (Ideal.span {(p : ℤ)}).IsMaximal := Int.ideal_span_isMaximal_of_prime p
25   obtain ⟨P, hP, hPlies⟩ :=
26     Ideal.exists_maximal_ideal_liesOver_of_isIntegral (S := 𝓞 K) (Ideal.span {(p : ℤ)})
27   let : P.IsMaximal := hP
28   let : P.LiesOver (Ideal.span {(p : ℤ)}) := hPlies
29   exact ⟨P, hP, hPlies, primePowerAutomorphism_unramified_arithmeticFrobenius n K p P hp⟩
30 
31 /-- Each permitted prime comes with an actual prime ideal and the proved
32 unramified Frobenius action, rather than only a conditional statement about
33 all prime ideals that might lie above it. -/
34 theorem permitted_prime_has_frobenius_witness (forbidden : Finset ℕ)
35     (p : PermittedPrime n forbidden) :
36     ∃ P : Ideal (𝓞 K), P.IsMaximal ∧ P.LiesOver (Ideal.span {(p.val : ℤ)}) ∧
37       Ideal.ramificationIdx P ℤ = 1 ∧
38       primeSample n K forbidden p ∈ MulAction.stabilizer Gal(K/ℚ) P ∧
39       ∀ x : 𝓞 K, Ideal.Quotient.mk P (primeSample n K forbidden p • x) =
40         (Ideal.Quotient.mk P x) ^ p.val := by
41   let : Fact (Nat.Prime p.val) := ⟨p.property.1⟩
42   exact exists_prime_above_with_frobenius n K p.val p.property.2.1
43 
44 /-- Every automorphism is arithmetic Frobenius at an actual unramified prime
45 ideal above a rational prime outside the chosen finite set and above the bound. -/
46 theorem exists_arithmetic_frobenius_prime (forbidden : Finset ℕ) (σ : Gal(K/ℚ)) (B : ℕ) :
47     ∃ (p : PermittedPrime n forbidden) (P : Ideal (𝓞 K)),
48       B < p.val ∧ primeSample n K forbidden p = σ ∧
49       P.IsMaximal ∧ P.LiesOver (Ideal.span {(p.val : ℤ)}) ∧
50       Ideal.ramificationIdx P ℤ = 1 ∧
51       σ ∈ MulAction.stabilizer Gal(K/ℚ) P ∧
52       ∀ x : 𝓞 K, Ideal.Quotient.mk P (σ • x) = (Ideal.Quotient.mk P x) ^ p.val := by
53   obtain ⟨p, hB, hσ⟩ := exists_prime_with_automorphism n K forbidden σ B
54   obtain ⟨P, hP, hPlies, he, hstab, hres⟩ :=
55     permitted_prime_has_frobenius_witness n K forbidden p
56   refine ⟨p, P, hB, hσ, hP, hPlies, he, ?_, ?_⟩
57   · rwa [hσ] at hstab
58   · rwa [hσ] at hres
59 
60 end PaperX.CyclotomicFrobeniusPrimes

Back to source controls