QuadraticPadicInertia.lean

1 import PaperX.QuadraticValuationInertia
2 import Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure
3 import Mathlib.NumberTheory.Padics.PadicIntegers
4 import Mathlib.RingTheory.Valuation.LocalSubring
5 
6 /-!+# Actual valuation rings above the p-adic integers
7 
8 Local domination is constructed, rather than assumed to exist. The inertia
9 statement uses the decomposition subgroup of the resulting valuation ring.
10 -/
11 
12 noncomputable section
13 
14 namespace PaperX.QuadraticPadicInertia
15 
16 variable (p : ℕ) [hp : Fact p.Prime]
17 
18 abbrev LocalClosure := AlgebraicClosure ℚ_[p]
19 
20 def integralMap : ℤ_[p] →+* LocalClosure p :=
21   (algebraMap ℚ_[p] (LocalClosure p)).comp PadicInt.Coe.ringHom
22 
23 theorem exists_dominating_valuation :
24     ∃ (A : ValuationSubring (LocalClosure p))
25       (h : ∀ x : ℤ_[p], integralMap p x ∈ A),
26       IsLocalHom ((integralMap p).codRestrict A.toSubring h) :=
27   IsLocalRing.exists_factor_valuationRing (integralMap p)
28 
29 theorem two_isUnit (hodd : p ≠ 2) : IsUnit (2 : ℤ_[p]) := by
30   apply PadicInt.isUnit_iff.mpr
31   change ‖((2 : ℕ) : ℤ_[p])‖ = 1
32   rw [PadicInt.norm_natCast_eq_one_iff]
33   exact (hp.out.coprime_iff_not_dvd).mpr (by
34     intro h
35     exact hodd ((Nat.dvd_prime Nat.prime_two).mp h |>.resolve_left hp.out.ne_one))
36 
37 theorem two_isUnit_of_contains (hodd : p ≠ 2)
38     (A : ValuationSubring (LocalClosure p))
39     (h : ∀ x : ℤ_[p], integralMap p x ∈ A) : IsUnit (2 : A) := by
40   simpa only [map_ofNat] using
41     (two_isUnit p hodd).map ((integralMap p).codRestrict A.toSubring h)
42 
43 theorem inertia_fixes_square_neg_one (hodd : p ≠ 2)
44     (A : ValuationSubring (LocalClosure p))
45     (h : ∀ x : ℤ_[p], integralMap p x ∈ A)
46     (y : LocalClosure p) (hy : y ^ 2 = -1)
47     (σ : A.decompositionSubgroup ℚ_[p]) (hσ : σ ∈ A.inertiaSubgroup ℚ_[p]) :
48     (σ.val : LocalClosure p ≃ₐ[ℚ_[p]] LocalClosure p) y = y :=
49   QuadraticValuationInertia.inertia_fixes_square_neg_one ℚ_[p] A
50     (two_isUnit_of_contains p hodd A h) y hy σ hσ
51 
52 theorem exists_dominating_valuation_with_fixed_roots (hodd : p ≠ 2) :
53     ∃ (A : ValuationSubring (LocalClosure p))
54       (h : ∀ x : ℤ_[p], integralMap p x ∈ A),
55       IsLocalHom ((integralMap p).codRestrict A.toSubring h) ∧
56       ∀ (y : LocalClosure p), y ^ 2 = -1 →
57         ∀ (σ : A.decompositionSubgroup ℚ_[p]), σ ∈ A.inertiaSubgroup ℚ_[p] →
58           (σ.val : LocalClosure p ≃ₐ[ℚ_[p]] LocalClosure p) y = y := by
59   obtain ⟨A, h, hlocal⟩ := exists_dominating_valuation p
60   exact ⟨A, h, hlocal, fun y hy σ hσ =>
61     inertia_fixes_square_neg_one p hodd A h y hy σ hσ⟩
62 
63 end PaperX.QuadraticPadicInertia

Back to source controls