QuadraticValuationInertia.lean

1 import Mathlib.RingTheory.Valuation.RamificationGroup
2 import Mathlib.Tactic
3 
4 /-!+# Valuation inertia fixes a square root of minus one away from two
5 
6 The inertia group here is Mathlib's actual kernel of the residue-field action
7 of a valuation's decomposition subgroup. No identification of that subgroup
8 with an entire absolute Galois group is asserted.
9 -/
10 
11 noncomputable section
12 
13 namespace PaperX.QuadraticValuationInertia
14 
15 variable {L : Type*} [Field L]
16 
17 theorem inverse_of_square_neg_one {y : L} (hy : y ^ 2 = -1) : y⁻¹ = -y := by
18   have hy0 : y ≠ 0 := by
19     intro h
20     simp [h] at hy
21   have hi : y * (-y) = 1 := by linear_combination -hy
22   calc
23     y⁻¹ = y⁻¹ * (y * (-y)) := by rw [hi, mul_one]
24     _ = -y := by rw [← mul_assoc, inv_mul_cancel₀ hy0, one_mul]
25 
26 theorem mem_of_square_neg_one (A : ValuationSubring L) {y : L}
27     (hy : y ^ 2 = -1) : y ∈ A := by
28   rcases A.mem_or_inv_mem y with h | h
29   · exact h
30   · simpa [inverse_of_square_neg_one hy] using A.neg_mem _ h
31 
32 def integralRoot (A : ValuationSubring L) (y : L) (hy : y ^ 2 = -1) : A :=
33   ⟨y, mem_of_square_neg_one A hy⟩
34 
35 @[simp] theorem integralRoot_val (A : ValuationSubring L) (y : L)
36     (hy : y ^ 2 = -1) : (integralRoot A y hy : L) = y := rfl
37 
38 theorem integralRoot_sq (A : ValuationSubring L) (y : L)
39     (hy : y ^ 2 = -1) : integralRoot A y hy ^ 2 = -1 := by
40   apply Subtype.ext
41   exact hy
42 
43 theorem integralRoot_isUnit (A : ValuationSubring L) (y : L)
44     (hy : y ^ 2 = -1) : IsUnit (integralRoot A y hy) := by
45   apply isUnit_iff_exists_inv.mpr
46   refine ⟨-integralRoot A y hy, ?_⟩
47   linear_combination -(integralRoot_sq A y hy)
48 
49 variable (K : Type*) [Field K] [Algebra K L]
50 
51 theorem inertia_fixes_square_neg_one (A : ValuationSubring L)
52     (h2 : IsUnit (2 : A)) (y : L) (hy : y ^ 2 = -1)
53     (σ : A.decompositionSubgroup K) (hσ : σ ∈ A.inertiaSubgroup K) :
54     (σ.val : L ≃ₐ[K] L) y = y := by
55   let z : A := integralRoot A y hy
56   have hz : z ^ 2 = -1 := integralRoot_sq A y hy
57   have hzu : IsUnit z := integralRoot_isUnit A y hy
58   have hres : IsLocalRing.residue A (σ • z) = IsLocalRing.residue A z := by
59     change MulSemiringAction.toRingAut (A.decompositionSubgroup K)
60       (IsLocalRing.ResidueField A) σ = 1 at hσ
61     exact congrArg (fun f : RingAut (IsLocalRing.ResidueField A) =>
62       f (IsLocalRing.residue A z)) hσ
63   have hs : (σ • z) ^ 2 = z ^ 2 := by
64     change (MulSemiringAction.toRingAut (A.decompositionSubgroup K) A σ z) ^ 2 = z ^ 2
65     rw [← map_pow, hz, map_neg, map_one]
66   rcases sq_eq_sq_iff_eq_or_eq_neg.mp hs with heq | hneg
67   · exact congrArg (fun t : A => (t : L)) heq
68   · have hr : IsLocalRing.residue A (-z) = IsLocalRing.residue A z := by
69       rwa [hneg] at hres
70     have hz0 : IsLocalRing.residue A z ≠ 0 :=
71       (IsLocalRing.residue_ne_zero_iff_isUnit z).mpr hzu
72     have h20 : (2 : IsLocalRing.ResidueField A) ≠ 0 := by
73       have := (IsLocalRing.residue_ne_zero_iff_isUnit (2 : A)).mpr h2
74       simpa only [map_ofNat] using this
75     have hm : (2 : IsLocalRing.ResidueField A) * IsLocalRing.residue A z = 0 := by
76       simp only [map_neg] at hr
77       linear_combination -hr
78     exact False.elim ((mul_ne_zero h20 hz0) hm)
79 
80 end PaperX.QuadraticValuationInertia

Back to source controls