PrimeDegreeSummabilityTower.lean

1 import PaperX.PrimeDegreeSummability
2 
3 /-!
4 # Degree-one primes in number-field towers
5 
6 The contraction map, residue degrees and exclusions are actual arithmetic objects.
7 Nonsummability of the supplied prime set remains an explicit hypothesis.
8 -/
9 
10 noncomputable section
11 set_option autoImplicit false
12 set_option maxHeartbeats 1000000
13 
14 namespace PaperX.PrimeDegreeSummabilityTower
15 
16 open NumberField IsDedekindDomain PrimeDegreeSummability
17 
18 variable (K L : Type*) [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L]
19 
20 /-- Absolute degree one implies relative degree one in an actual number-field tower. -/
21 theorem relative_degree_one (q : HeightOneSpectrum (𝓞 L))
22     (hq : q.asIdeal.inertiaDeg ℤ = 1) : q.asIdeal.inertiaDeg (𝓞 K) = 1 := by
23   have ht := Ideal.inertiaDeg_tower (R := ℤ) (q := q.asIdeal.under (𝓞 K)) q.asIdeal
24   rw [hq] at ht
25   have hpos := (q.asIdeal.under (𝓞 K)).inertiaDeg_pos ℤ
26   have hle := Nat.le_mul_of_pos_left (q.asIdeal.inertiaDeg (𝓞 K)) hpos
27   have hrel := q.asIdeal.inertiaDeg_pos (𝓞 K)
28   omega
29 
30 /-- Only finitely many actual upper primes contract to a fixed lower prime. -/
31 theorem finite_under_fibre (p : HeightOneSpectrum (𝓞 K)) :
32     {q : HeightOneSpectrum (𝓞 L) | q.under (𝓞 K) = p}.Finite := by
33   have hf : {q : HeightOneSpectrum (𝓞 L) | q.asIdeal ∈ p.asIdeal.primesOver (𝓞 L)}.Finite :=
34     (Algebra.QuasiFinite.finite_primesOver (S := 𝓞 L) p.asIdeal).preimage
35       (fun _ _ _ _ h => HeightOneSpectrum.ext h)
36   apply hf.subset
37   intro q hq
38   have he := congrArg HeightOneSpectrum.asIdeal hq
39   exact ⟨q.isPrime, ⟨he.symm⟩⟩
40 
41 /-- A finite set of lower primes excludes only finitely many upper primes. -/
42 theorem finite_under_preimage (bad : Set (HeightOneSpectrum (𝓞 K))) (hbad : bad.Finite) :
43     ((fun q : HeightOneSpectrum (𝓞 L) => q.under (𝓞 K)) ⁻¹' bad).Finite := by
44   apply hbad.preimage'
45   intro p _
46   exact finite_under_fibre K L p
47 
48 /-- Divergence supplies a relative degree-one prime outside prescribed lower exclusions. -/
49 theorem exists_relative_degree_one_outside_finite
50     (S : Set (HeightOneSpectrum (𝓞 L)))
51     (hS : ¬ Summable (fun q : S => (q.1.asIdeal.absNorm : ℝ)⁻¹))
52     (bad : Set (HeightOneSpectrum (𝓞 K))) (hbad : bad.Finite) :
53     ∃ q : HeightOneSpectrum (𝓞 L), q ∈ S ∧ q.under (𝓞 K) ∉ bad ∧
54       q.asIdeal.inertiaDeg (𝓞 K) = 1 := by
55   obtain ⟨q, hq, hb, hd⟩ := exists_degree_one_outside_finite L S hS _
56     (finite_under_preimage K L bad hbad)
57   exact ⟨q, hq, hb, relative_degree_one K L q hd⟩
58 
59 /-- Infinitely many such relative degree-one primes survive the lower-field exclusions. -/
60 theorem infinite_relative_degree_one_outside_finite
61     (S : Set (HeightOneSpectrum (𝓞 L)))
62     (hS : ¬ Summable (fun q : S => (q.1.asIdeal.absNorm : ℝ)⁻¹))
63     (bad : Set (HeightOneSpectrum (𝓞 K))) (hbad : bad.Finite) :
64     {q : HeightOneSpectrum (𝓞 L) | q ∈ S ∧ q.under (𝓞 K) ∉ bad ∧
65       q.asIdeal.inertiaDeg (𝓞 K) = 1}.Infinite := by
66   apply (infinite_degree_one_outside_finite L S hS _
67     (finite_under_preimage K L bad hbad)).mono
68   intro q hq
69   exact ⟨hq.1, hq.2.1, relative_degree_one K L q hq.2.2⟩
70 
71 end PaperX.PrimeDegreeSummabilityTower

Back to source controls