PrimeDegreeUnramifiedFrobenius.lean

1 import PaperX.PrimeDegreeFieldFrobenius
2 import Mathlib.NumberTheory.NumberField.Discriminant.Different
3 
4 /-!
5 # Unramified Frobenius after discriminant exclusions
6 
7 The excluded set is constructed from the nonzero absolute discriminant of the
8 upper number field. Its finiteness and actual unramifiedness are proved.
9 Only nonsummability of the prescribed Frobenius prime set remains assumed.
10 -/
11 
12 noncomputable section
13 set_option autoImplicit false
14 set_option maxHeartbeats 1000000
15 
16 namespace PaperX.PrimeDegreeUnramifiedFrobenius
17 
18 open NumberField IsDedekindDomain PrimeDegreeSummability PrimeDegreeFieldFrobenius
19 
20 variable (K T : Type*) [Field K] [Field T] [NumberField K] [NumberField T]
21 
22 /-- Lower primes containing the absolute discriminant of the upper field. -/
23 def discriminantPrimes : Set (HeightOneSpectrum (𝓞 K)) :=
24   {p | (NumberField.discr T : 𝓞 K) ∈ p.asIdeal}
25 
26 /-- The discriminant exclusion is finite because the discriminant is nonzero. -/
27 theorem discriminantPrimes_finite : (discriminantPrimes K T).Finite := by
28   have hne : (NumberField.discr T : 𝓞 K) ≠ 0 := by
29     exact_mod_cast NumberField.discr_ne_zero T
30   exact (Ring.HasFiniteQuotients.finite_setOfPred_mem (NumberField.discr T : 𝓞 K) hne).preimage
31     (fun _ _ _ _ h => HeightOneSpectrum.ext h)
32 
33 /-- Avoiding the absolute discriminant gives actual unramifiedness over the integers. -/
34 theorem isUnramifiedAt_int_of_discriminant_notMem (Q : HeightOneSpectrum (𝓞 T))
35     (hdisc : (NumberField.discr T : 𝓞 T) ∉ Q.asIdeal) :
36     Algebra.IsUnramifiedAt ℤ Q.asIdeal := by
37   let p := rationalPrimeBelow T Q
38   have hp : Prime (p.1 : ℤ) := Nat.prime_iff_prime_int.mp p.2
39   have hnd : ¬ (p.1 : ℤ) ∣ NumberField.discr T := by
40     rintro ⟨a, ha⟩
41     apply hdisc
42     rw [ha, Int.cast_mul]
43     apply Q.asIdeal.mul_mem_right
44     simpa only [p, rationalPrimeBelow, Int.cast_natCast] using Int.absNorm_under_mem Q.asIdeal
45   exact (NumberField.not_dvd_discr_iff_forall_liesOver T (𝓞 T) hp).mp hnd
46     Q.asIdeal inferInstance (Int.liesOver_span_absNorm Q.asIdeal)
47 
48 variable [Algebra K T]
49 
50 omit [NumberField K] in
51 /-- The constructed lower exclusion ensures unramifiedness over the lower number field. -/
52 theorem isUnramifiedAt_of_notMem_discriminantPrimes (Q : HeightOneSpectrum (𝓞 T))
53     (hQ : Q.under (𝓞 K) ∉ discriminantPrimes K T) :
54     Algebra.IsUnramifiedAt (𝓞 K) Q.asIdeal := by
55   have hdisc : (NumberField.discr T : 𝓞 T) ∉ Q.asIdeal := by
56     simpa only [discriminantPrimes, Set.mem_ofPred_eq, HeightOneSpectrum.under_asIdeal,
57       Ideal.under, Ideal.mem_comap, map_intCast] using hQ
58   have := isUnramifiedAt_int_of_discriminant_notMem T Q hdisc
59   exact Algebra.IsUnramifiedAt.of_restrictScalars ℤ Q.asIdeal
60 
61 /-- Nonsummability alone supplies the prescribed actual unramified Frobenius after exclusions. -/
62 theorem exists_unramified_fixedField_frobenius
63     (ρ : T ≃ₐ[K] T)
64     (hdiv : ¬ Summable
65       (fun q : prescribedPrimes (IntermediateField.fixedField (Subgroup.zpowers ρ)) T
66         (overFixedField K T ρ) => (q.1.asIdeal.absNorm : ℝ)⁻¹))
67     (bad : Set (HeightOneSpectrum (𝓞 K))) (hbad : bad.Finite) :
68     ∃ Q : HeightOneSpectrum (𝓞 T), Q.under (𝓞 K) ∉ bad ∧
69       Algebra.IsUnramifiedAt (𝓞 K) Q.asIdeal ∧
70       (integralAut K T ρ).toAlgHom.IsArithFrobAt Q.asIdeal := by
71   obtain ⟨Q, hb, _, hF⟩ := exists_fixedField_descended_frobenius K T ρ hdiv
72     (bad ∪ discriminantPrimes K T) (hbad.union (discriminantPrimes_finite K T))
73   have ht :
74       (Q.under (𝓞 (IntermediateField.fixedField (Subgroup.zpowers ρ)))).under (𝓞 K) =
75         Q.under (𝓞 K) := by
76     apply HeightOneSpectrum.ext
77     change (Q.asIdeal.under (𝓞 (IntermediateField.fixedField (Subgroup.zpowers ρ)))).under
78       (𝓞 K) = Q.asIdeal.under (𝓞 K)
79     rw [Ideal.under_under]
80   rw [ht] at hb
81   have hdisc : Q.under (𝓞 K) ∉ discriminantPrimes K T := fun h => hb (Or.inr h)
82   exact ⟨Q, (fun h => hb (Or.inl h)),
83     isUnramifiedAt_of_notMem_discriminantPrimes K T Q hdisc, hF⟩
84 
85 end PaperX.PrimeDegreeUnramifiedFrobenius

Back to source controls