ValuationRamification.lean

1 import Mathlib.RingTheory.Valuation.RamificationGroup
2 import Mathlib.RingTheory.Ideal.Operations
3 
4 /-! Lower congruence subgroups are defined by their action on an actual local ring.
5 For a discrete valuation ring in a finite Galois extension these are the usual
6 nonnegative lower ramification groups. The generic local-ring definition is NOT
7 asserted to be an absolute Weil ramification filtration. -/
8 set_option autoImplicit false
9 noncomputable section
10 
11 namespace PaperXI.ValuationRamification
12 variable (R D : Type*) [CommRing R] [IsLocalRing R] [Group D] [MulSemiringAction D R]
13 
14 /-- Automorphisms acting as identity modulo the (i+1)-st maximal-ideal power. -/
15 def lower (i : ℕ) : Subgroup D where
16   carrier := {g | ∀ x : R, g • x - x ∈ (IsLocalRing.maximalIdeal R) ^ (i + 1)}
17   one_mem' := by intro x; simp
18   mul_mem' := by
19     intro g h hg hh x
20     have ha := hg (h • x)
21     have hb := hh x
22     have hab := Ideal.add_mem ((IsLocalRing.maximalIdeal R) ^ (i+1)) ha hb
23     simpa only [sub_add_sub_cancel, mul_smul] using hab
24   inv_mem' := by
25     intro g hg x
26     have hh := hg (g⁻¹ • x)
27     have hh' := ((IsLocalRing.maximalIdeal R) ^ (i+1)).neg_mem hh
28     simpa using hh'
29 
30 @[simp] theorem mem_lower (i : ℕ) (g : D) :
31     g ∈ lower R D i ↔ ∀ x : R, g • x - x ∈ (IsLocalRing.maximalIdeal R) ^ (i+1) := Iff.rfl
32 
33 /-- Automorphisms preserve every power of the maximal ideal. -/
34 theorem smul_mem_power (g : D) (n : ℕ) {x : R}
35     (hx : x ∈ (IsLocalRing.maximalIdeal R)^n) :
36     g • x ∈ (IsLocalRing.maximalIdeal R)^n := by
37   let e := MulSemiringAction.toRingAut D R g
38   have hm : Ideal.map (e : R →+* R) ((IsLocalRing.maximalIdeal R)^n) =
39       (IsLocalRing.maximalIdeal R)^n := by
40     rw [Ideal.map_pow]
41     exact congrArg (fun J : Ideal R => J^n)
42       (IsLocalRing.map_maximalIdeal_of_surjective (e : R →+* R) e.surjective)
43   have he := Ideal.mem_map_of_mem (e : R →+* R) hx
44   rw [hm] at he
45   exact he
46 
47 /-- Normality is derived from conjugation on the actual ring. -/
48 instance lower_normal (i : ℕ) : (lower R D i).Normal where
49   conj_mem g hg h := by
50     intro x
51     have hm := smul_mem_power R D h (i+1) (hg (h⁻¹ • x))
52     simpa only [smul_sub, smul_inv_smul, mul_smul] using hm
53 
54 /-- The filtration is decreasing without an assumed filtration certificate. -/
55 theorem antitone : Antitone (lower R D) := by
56   intro i j hij g hg x
57   exact (Ideal.pow_le_pow_right (Nat.add_le_add_right hij 1)) (hg x)
58 
59 /-- Zeroth congruence group equals the kernel of the literal residue-field action. -/
60 theorem lower_zero_eq_residue_kernel : lower R D 0 =
61     (MulSemiringAction.toRingAut D (IsLocalRing.ResidueField R)).ker := by
62   ext g
63   change (∀ x : R, g • x - x ∈ (IsLocalRing.maximalIdeal R) ^ (0+1)) ↔
64     MulSemiringAction.toRingAut D (IsLocalRing.ResidueField R) g = 1
65   simp only [zero_add, pow_one]
66   constructor
67   · intro hg
68     apply RingEquiv.ext
69     intro y
70     obtain ⟨x, rfl⟩ := IsLocalRing.residue_surjective (R := R) y
71     have h := (IsLocalRing.residue_eq_zero_iff (g • x - x)).mpr (hg x)
72     change g • IsLocalRing.residue R x = IsLocalRing.residue R x
73     simpa only [map_sub, IsLocalRing.ResidueField.residue_smul, sub_eq_zero] using h
74   · intro hg x
75     apply (IsLocalRing.residue_eq_zero_iff (g • x - x)).mp
76     rw [map_sub, IsLocalRing.ResidueField.residue_smul]
77     have hh := RingEquiv.congr_fun hg (IsLocalRing.residue R x)
78     exact sub_eq_zero.mpr hh
79 
80 theorem lower_le_inertia (i : ℕ) : lower R D i ≤
81     (MulSemiringAction.toRingAut D (IsLocalRing.ResidueField R)).ker := by
82   rw [← lower_zero_eq_residue_kernel]
83   exact antitone R D (Nat.zero_le i)
84 
85 theorem positive_le_one {i : ℕ} (hi : 1 ≤ i) : lower R D i ≤ lower R D 1 :=
86   antitone R D hi
87 
88 section Valuation
89 variable (K : Type*) {L : Type*} [Field K] [Field L] [Algebra K L]
90 
91 theorem valuation_lower_zero (A : ValuationSubring L) :
92     lower A (A.decompositionSubgroup K) 0 = A.inertiaSubgroup K :=
93   lower_zero_eq_residue_kernel A (A.decompositionSubgroup K)
94 
95 end Valuation
96 end PaperXI.ValuationRamification

Back to source controls