RamificationSeparation.lean

1 import PaperXI.ValuationRamification
2 import Mathlib.RingTheory.Filtration
3 import Mathlib.Data.Finset.Lattice.Fold
4 
5 /-! Separated local rings and finite faithful automorphism groups have a terminating
6 lower congruence filtration. This justifies finite support of the conductor sum;
7 eventual triviality is a theorem, not an assumed cutoff. -/
8 set_option autoImplicit false
9 noncomputable section
10 open scoped Classical
11 namespace PaperXI.RamificationSeparation
12 open PaperXI.ValuationRamification
13 variable (R D : Type*) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
14   [Group D] [MulSemiringAction D R] [FaithfulSMul D R]
15 
16 /-- Krull intersection separates automorphisms that agree to every depth. -/
17 theorem mem_all_lower_iff (g : D) : (∀ i, g ∈ lower R D i) ↔ g = 1 := by
18   constructor
19   · intro hg
20     apply eq_of_smul_eq_smul (α := R)
21     intro x
22     rw [one_smul]
23     apply sub_eq_zero.mp
24     have hx : g • x - x ∈ ⨅ n : ℕ, (IsLocalRing.maximalIdeal R)^n := by
25       rw [Submodule.mem_iInf]
26       intro n
27       cases n with
28       | zero => simp
29       | succ n => exact hg n x
30     rw [Ideal.iInf_pow_eq_bot_of_isLocalRing (IsLocalRing.maximalIdeal R)
31       Ideal.IsPrime.ne_top'] at hx
32     exact hx
33   · rintro rfl i
34     exact (lower R D i).one_mem
35 
36 /-- A finite group admits a single cutoff valid for every automorphism. -/
37 theorem eventually_trivial [Finite D] : ∃ N : ℕ, ∀ i, N ≤ i → lower R D i = ⊥ := by
38   classical
39   let := Fintype.ofFinite D
40   have hex : ∀ g : D, ∃ n : ℕ, ∀ i, n ≤ i → g ∈ lower R D i → g = 1 := by
41     intro g
42     by_cases hg : g = 1
43     · exact ⟨0, fun _ _ _ => hg⟩
44     · have hn : ¬ ∀ i, g ∈ lower R D i := fun hh => hg ((mem_all_lower_iff R D g).mp hh)
45       obtain ⟨n, hn⟩ := not_forall.mp hn
46       exact ⟨n, fun i hi hh => False.elim (hn (antitone R D hi hh))⟩
47   choose n hn using hex
48   refine ⟨Finset.univ.sup n, fun i hi => ?_⟩
49   apply le_antisymm
50   · intro g hg
51     exact hn g i (le_trans (Finset.le_sup (f := n) (Finset.mem_univ g)) hi) hg
52   · exact bot_le
53 
54 section Valuation
55 variable (K : Type*) {L : Type*} [Field K] [Field L] [Algebra K L]
56 
57 /-- Restricting a decomposition-group element to its valuation ring is faithful:
58 every field element or its inverse lies in that ring. -/
59 instance valuation_faithful (A : ValuationSubring L) :
60     FaithfulSMul (A.decompositionSubgroup K) A where
61   eq_of_smul_eq_smul {g h} hh := by
62     apply Subtype.ext
63     apply AlgEquiv.ext
64     intro x
65     rcases A.mem_or_inv_mem x with hx | hx
66     · exact congrArg (fun z : A => (z : L)) (hh ⟨x, hx⟩)
67     · have hi := congrArg (fun z : A => (z : L)) (hh ⟨x⁻¹, hx⟩)
68       change g.val (x⁻¹) = h.val (x⁻¹) at hi
69       simpa only [map_inv₀, inv_inj] using hi
70 
71 /-- A valuation-ring specialization with derived faithfulness. -/
72 theorem valuation_eventually_trivial (A : ValuationSubring L)
73     [IsNoetherianRing A] [Finite (A.decompositionSubgroup K)] :
74     ∃ N : ℕ, ∀ i, N ≤ i → lower A (A.decompositionSubgroup K) i = ⊥ :=
75   eventually_trivial A (A.decompositionSubgroup K)
76 
77 end Valuation
78 end PaperXI.RamificationSeparation

Back to source controls