UnramifiedConductor.lean

1 import PaperXI.ResidueDegreeBaseChange
2 import PaperXI.ValuationConductor
3 
4 /-! Restriction across an inertia-containing subgroup, with a power change of
5 residue Frobenius. The congruence groups, fixed spaces and EVERY lower conductor
6 summand are preserved, for wild as well as tame representations. This is not the
7 ramified-quotient/Herbrand change-of-extension theorem. -/
8 set_option autoImplicit false
9 noncomputable section
10 open scoped Classical
11 namespace PaperXI.UnramifiedConductor
12 open PaperXI.ResidueWeil PaperXI.ValuationRamification PaperXI.ValuationConductor
13 
14 variable (R D : Type*) [CommRing R] [IsLocalRing R] [Group D] [MulSemiringAction D R]
15 variable (H : Subgroup D)
16 
17 /-- Lower ramification in a subgroup is its literal intersection with the ambient lower group. -/
18 theorem lower_eq_comap (i : ℕ) : lower R H i = (lower R D i).comap H.subtype := rfl
19 
20 /-- If H contains inertia, ALL lower ramification groups are unchanged. -/
21 def lowerEquiv (hI : lower R D 0 ≤ H) (i : ℕ) : lower R H i ≃* lower R D i where
22   toFun g := ⟨g.val.val, g.property⟩
23   invFun g := ⟨⟨g.val, hI ((ValuationRamification.antitone R D (Nat.zero_le i)) g.property)⟩, g.property⟩
24   left_inv _ := rfl
25   right_inv _ := rfl
26   map_mul' _ _ := rfl
27 
28 theorem lower_card (hI : lower R D 0 ≤ H) (i : ℕ) :
29     Nat.card (lower R H i) = Nat.card (lower R D i) :=
30   Nat.card_congr (lowerEquiv R D H hI i).toEquiv
31 
32 /-- Actual subgroup and degree-dilation inclusion. -/
33 def embedding (F F' : RingAut (IsLocalRing.ResidueField R)) (n : ℕ) (hp : F^n = F') :
34     Pullback (residue R H) F' →* Pullback (residue R D) F where
35   toFun w := ⟨(w.val.1.val, Multiplicative.ofAdd ((n : ℤ) * Multiplicative.toAdd w.val.2)), by
36     change residue R D w.val.1.val = F ^ ((n : ℤ) * Multiplicative.toAdd w.val.2)
37     rw [zpow_mul, zpow_natCast, hp]
38     exact w.property⟩
39   map_one' := by apply Subtype.ext; simp
40   map_mul' a b := by
41     apply Subtype.ext
42     apply Prod.ext
43     · rfl
44     · change Multiplicative.ofAdd ((n : ℤ) * (Multiplicative.toAdd a.val.2 + Multiplicative.toAdd b.val.2)) = _
45       simp [mul_add]
46 
47 @[simp] theorem embedding_degree (F F' : RingAut (IsLocalRing.ResidueField R))
48     (n : ℕ) (hp : F^n = F') (w : Pullback (residue R H) F') :
49     Multiplicative.toAdd (degree (residue R D) F (embedding R D H F F' n hp w)) =
50       (n : ℤ) * Multiplicative.toAdd (degree (residue R H) F' w) := rfl
51 
52 theorem embedding_injective (F F' : RingAut (IsLocalRing.ResidueField R))
53     {n : ℕ} (hn : n ≠ 0) (hp : F^n = F') :
54     Function.Injective (embedding R D H F F' n hp) := by
55   intro a b hab
56   have h1 := congrArg (fun w : Pullback (residue R D) F => w.val.1) hab
57   have h2 := congrArg (fun w : Pullback (residue R D) F => Multiplicative.toAdd w.val.2) hab
58   have hnz : (n : ℤ) ≠ 0 := by exact_mod_cast hn
59   apply Subtype.ext
60   apply Prod.ext
61   · exact Subtype.ext h1
62   · exact Multiplicative.toAdd.injective (mul_left_cancel₀ hnz h2)
63 
64 /-- Restriction matches the actual lower-group operators, not merely their cardinalities. -/
65 theorem embedding_lift (F F' : RingAut (IsLocalRing.ResidueField R))
66     (n : ℕ) (hp : F^n = F') (hI : lower R D 0 ≤ H) (i : ℕ) (g : lower R H i) :
67     embedding R D H F F' n hp (lift R H F' i g) =
68       lift R D F i (lowerEquiv R D H hI i g) := by
69   apply Subtype.ext
70   apply Prod.ext
71   · rfl
72   · simp [embedding, lift]
73 
74 variable {V : Type*} [AddCommGroup V] [Module ℂ V]
75 
76 /-- Fixed subspaces of the same vector space agree exactly at every depth. -/
77 theorem fixed_eq (F F' : RingAut (IsLocalRing.ResidueField R))
78     (n : ℕ) (hp : F^n = F') (hI : lower R D 0 ≤ H)
79     (ρ : Representation ℂ (Pullback (residue R D) F) V) (i : ℕ) :
80     fixed R H F' (ρ.comp (embedding R D H F F' n hp)) i = fixed R D F ρ i := by
81   ext v
82   constructor
83   · intro hv g
84     let g' := (lowerEquiv R D H hI i).symm g
85     have h := hv g'
86     change ρ (embedding R D H F F' n hp (lift R H F' i g')) v = v at h
87     rw [embedding_lift R D H F F' n hp hI, (lowerEquiv R D H hI i).apply_symm_apply] at h
88     exact h
89   · intro hv g
90     change ρ (embedding R D H F F' n hp (lift R H F' i g)) v = v
91     rw [embedding_lift R D H F F' n hp hI]
92     exact hv _
93 
94 /-- The full lower-numbering weight and fixed-space defect are preserved together. -/
95 theorem summand_eq (F F' : RingAut (IsLocalRing.ResidueField R))
96     (n : ℕ) (hp : F^n = F') (hI : lower R D 0 ≤ H)
97     (ρ : Representation ℂ (Pullback (residue R D) F) V) (i : ℕ) :
98     summand R H F' (ρ.comp (embedding R D H F F' n hp)) i = summand R D F ρ i := by
99   unfold summand codimension
100   rw [lower_card R D H hI i, lower_card R D H hI 0, fixed_eq R D H F F' n hp hI ρ i]
101 
102 /-- In particular this is not merely a zero-Swan/tame invariance theorem. -/
103 theorem swan_eq (F F' : RingAut (IsLocalRing.ResidueField R))
104     (n : ℕ) (hp : F^n = F') (hI : lower R D 0 ≤ H)
105     (ρ : Representation ℂ (Pullback (residue R D) F) V) :
106     swan R H F' (ρ.comp (embedding R D H F F' n hp)) = swan R D F ρ := by
107   unfold swan
108   apply tsum_congr
109   intro i
110   exact summand_eq R D H F F' n hp hI ρ (i+1)
111 
112 theorem artin_eq (F F' : RingAut (IsLocalRing.ResidueField R))
113     (n : ℕ) (hp : F^n = F') (hI : lower R D 0 ≤ H)
114     (ρ : Representation ℂ (Pullback (residue R D) F) V) :
115     artin R H F' (ρ.comp (embedding R D H F F' n hp)) = artin R D F ρ := by
116   unfold artin codimension
117   rw [swan_eq R D H F F' n hp hI, fixed_eq R D H F F' n hp hI ρ 0]
118 
119 /-- With faithful finite action the series has finite support, independently of tameness. -/
120 theorem summable_restriction [IsNoetherianRing R] [Finite D] [FaithfulSMul D R]
121     (F F' : RingAut (IsLocalRing.ResidueField R))
122     (n : ℕ) (hp : F^n = F') (hI : lower R D 0 ≤ H)
123     (ρ : Representation ℂ (Pullback (residue R D) F) V) :
124     Summable (summand R H F' (ρ.comp (embedding R D H F F' n hp))) := by
125   have he : summand R H F' (ρ.comp (embedding R D H F F' n hp)) = summand R D F ρ := by
126     funext i
127     exact summand_eq R D H F F' n hp hI ρ i
128   rw [he]
129   exact summable_summands R D F ρ
130 
131 end PaperXI.UnramifiedConductor

Back to source controls