PrimeDegreeSummabilityFrobenius.lean

1 import PaperX.PrimeDegreeSummabilityTower
2 import Mathlib.RingTheory.Frobenius
3 
4 /-!
5 # Frobenius descent at relative degree-one primes
6 
7 The input is an actual supplied Frobenius endomorphism, not an assertion that a
8 prime with a prescribed Frobenius exists. The residue congruence descends because
9 relative degree one makes the two base residue cardinalities equal.
10 -/
11 
12 noncomputable section
13 set_option autoImplicit false
14 set_option maxHeartbeats 1000000
15 
16 namespace PaperX.PrimeDegreeSummabilityFrobenius
17 
18 open NumberField IsDedekindDomain
19 
20 variable (K E T : Type*) [Field K] [Field E] [Field T]
21   [NumberField K] [NumberField E] [NumberField T]
22   [Algebra K E] [Algebra E T] [Algebra K T] [IsScalarTower K E T]
23 
24 omit [NumberField T] in
25 /-- Residue cardinalities agree below a relative degree-one prime. -/
26 theorem residue_card_eq_of_degree_one (Q : HeightOneSpectrum (𝓞 T))
27     (hdegree : (Q.asIdeal.under (𝓞 E)).inertiaDeg (𝓞 K) = 1) :
28     Nat.card (𝓞 E ⧸ Q.asIdeal.under (𝓞 E)) =
29       Nat.card (𝓞 K ⧸ Q.asIdeal.under (𝓞 K)) := by
30   have hnorm := Ideal.absNorm_pow_inertiaDeg
31     (Q.asIdeal.under (𝓞 K)) (Q.asIdeal.under (𝓞 E))
32   rw [hdegree, pow_one] at hnorm
33   exact hnorm.symm
34 
35 omit [NumberField T] in
36 /-- The same actual endomorphism is Frobenius over the lower field at degree one. -/
37 theorem restrictScalars_isArithFrobAt_of_degree_one
38     (φ : (𝓞 T) →ₐ[𝓞 E] (𝓞 T)) (Q : HeightOneSpectrum (𝓞 T))
39     (hφ : φ.IsArithFrobAt Q.asIdeal)
40     (hdegree : (Q.asIdeal.under (𝓞 E)).inertiaDeg (𝓞 K) = 1) :
41     (φ.restrictScalars (𝓞 K)).IsArithFrobAt Q.asIdeal := by
42   intro x
43   change φ x - x ^ Nat.card (𝓞 K ⧸ Q.asIdeal.under (𝓞 K)) ∈ Q.asIdeal
44   rw [← residue_card_eq_of_degree_one K E T Q hdegree]
45   exact hφ x
46 
47 /-- Actual intermediate primes admitting the supplied Frobenius endomorphism upstairs. -/
48 def prescribedPrimes (φ : (𝓞 T) →ₐ[𝓞 E] (𝓞 T)) : Set (HeightOneSpectrum (𝓞 E)) :=
49   {q | ∃ Q : HeightOneSpectrum (𝓞 T), Q.under (𝓞 E) = q ∧ φ.IsArithFrobAt Q.asIdeal}
50 
51 omit [NumberField T] in
52 /-- Divergence of the prescribed Frobenius set produces an actual descended Frobenius. -/
53 theorem exists_descended_frobenius
54     (φ : (𝓞 T) →ₐ[𝓞 E] (𝓞 T))
55     (hdiv : ¬ Summable (fun q : prescribedPrimes E T φ => (q.1.asIdeal.absNorm : ℝ)⁻¹))
56     (bad : Set (HeightOneSpectrum (𝓞 K))) (hbad : bad.Finite) :
57     ∃ Q : HeightOneSpectrum (𝓞 T), (Q.under (𝓞 E)).under (𝓞 K) ∉ bad ∧
58       (Q.asIdeal.under (𝓞 E)).inertiaDeg (𝓞 K) = 1 ∧
59       (φ.restrictScalars (𝓞 K)).IsArithFrobAt Q.asIdeal := by
60   obtain ⟨q, hq, hb, hd⟩ :=
61     PrimeDegreeSummabilityTower.exists_relative_degree_one_outside_finite K E
62       (prescribedPrimes E T φ) hdiv bad hbad
63   obtain ⟨Q, hQ, hφ⟩ := hq
64   subst q
65   exact ⟨Q, hb, hd, restrictScalars_isArithFrobAt_of_degree_one K E T φ Q hφ hd⟩
66 
67 end PaperX.PrimeDegreeSummabilityFrobenius

Back to source controls