HenselianConductorTransport.lean

1 import PaperXI.HenselianWeilAttachment
2 
3 /-! Conductor invariance for the actual base change to the Hensel-generated field.
4 The valuation ring is unchanged upstairs. This is not ramified quotient invariance. -/
5 set_option autoImplicit false
6 noncomputable section
7 namespace PaperXI.HenselianConductorTransport
8 open IsLocalRing PaperXI.ResidueWeil PaperXI.FiniteResidueBaseChange
9 open PaperXI.ValuationRamification PaperXI.ValuationConductor PaperXI.HenselianWeilAttachment
10 variable (k k' K : Type*) {L : Type*} [Field k] [Fintype k] [Field k'] [Fintype k']
11   [Algebra k k'] [Field K] [Field L] [Algebra K L]
12 variable (A : ValuationSubring L) [HenselianLocalRing A]
13   [Algebra k (ResidueField A)] [Algebra k' (ResidueField A)]
14   [Algebra.IsAlgebraic k (ResidueField A)] [Algebra.IsAlgebraic k' (ResidueField A)]
15 
16 /-- Lower congruence groups commute with the constructed decomposition equivalence. -/
17 def localLowerEquiv (i : ℕ) :
18     lower A (A.decompositionSubgroup (liftedField k' K A)) i ≃*
19     lower A (UnramifiedValuation.fixingGroup k' K A) i where
20   toFun g := ⟨decompositionEquiv k' K A g.val, g.property⟩
21   invFun g := ⟨(decompositionEquiv k' K A).symm g.val, by
22     intro x
23     rw [← HenselianWeilAttachment.ring_action k' K A,
24       (decompositionEquiv k' K A).apply_symm_apply]
25     exact g.property x⟩
26   left_inv g := Subtype.ext ((decompositionEquiv k' K A).symm_apply_apply g.val)
27   right_inv g := Subtype.ext ((decompositionEquiv k' K A).apply_symm_apply g.val)
28   map_mul' g h := Subtype.ext ((decompositionEquiv k' K A).map_mul g.val h.val)
29 
30 /-- Every lower group over the new field is isomorphic to the original lower group. -/
31 def lowerEquiv (i : ℕ) :
32     lower A (A.decompositionSubgroup (liftedField k' K A)) i ≃*
33     lower A (A.decompositionSubgroup K) i :=
34   (localLowerEquiv k' K A i).trans (UnramifiedConductor.lowerEquiv A
35     (A.decompositionSubgroup K) (UnramifiedValuation.fixingGroup k' K A)
36     (UnramifiedValuation.contains_inertia k' K A) i)
37 
38 omit [Algebra.IsAlgebraic k' (ResidueField A)] in
39 theorem lower_card (i : ℕ) :
40     Nat.card (lower A (A.decompositionSubgroup (liftedField k' K A)) i) =
41     Nat.card (lower A (A.decompositionSubgroup K) i) :=
42   Nat.card_congr (lowerEquiv k' K A i).toEquiv
43 
44 /-- The actual operators agree under the degree-dilating embedding. -/
45 theorem embedding_lift (i : ℕ) (g : lower A (A.decompositionSubgroup (liftedField k' K A)) i) :
46     HenselianWeilAttachment.embedding k k' K A
47       (lift A (A.decompositionSubgroup (liftedField k' K A)) (geometric k' (ResidueField A)) i g) =
48     lift A (A.decompositionSubgroup K) (geometric k (ResidueField A)) i (lowerEquiv k' K A i g) := by
49   apply Subtype.ext
50   apply Prod.ext
51   · rfl
52   · simp [HenselianWeilAttachment.embedding, HenselianWeilAttachment.pullbackEquiv,
53       UnramifiedValuation.embedding, UnramifiedConductor.embedding, lift]
54 
55 variable {V : Type*} [AddCommGroup V] [Module ℂ V]
56 
57 /-- Equality of genuine fixed subspaces on the same carrier. -/
58 theorem fixed_eq
59     (ρ : Representation ℂ (Pullback (residue A (A.decompositionSubgroup K))
60       (geometric k (ResidueField A))) V) (i : ℕ) :
61     fixed A (A.decompositionSubgroup (liftedField k' K A)) (geometric k' (ResidueField A))
62       (ρ.comp (HenselianWeilAttachment.embedding k k' K A)) i =
63     fixed A (A.decompositionSubgroup K) (geometric k (ResidueField A)) ρ i := by
64   ext v
65   constructor
66   · intro hv g
67     let g' := (lowerEquiv k' K A i).symm g
68     have h := hv g'
69     change ρ (HenselianWeilAttachment.embedding k k' K A (lift A _ _ i g')) v = v at h
70     rw [embedding_lift, (lowerEquiv k' K A i).apply_symm_apply] at h
71     exact h
72   · intro hv g
73     change ρ (HenselianWeilAttachment.embedding k k' K A (lift A _ _ i g)) v = v
74     rw [embedding_lift]
75     exact hv _
76 
77 /-- The conventional inertia denominator and fixed-space codimension agree together. -/
78 theorem summand_eq
79     (ρ : Representation ℂ (Pullback (residue A (A.decompositionSubgroup K))
80       (geometric k (ResidueField A))) V) (i : ℕ) :
81     summand A (A.decompositionSubgroup (liftedField k' K A)) (geometric k' (ResidueField A))
82       (ρ.comp (HenselianWeilAttachment.embedding k k' K A)) i =
83     summand A (A.decompositionSubgroup K) (geometric k (ResidueField A)) ρ i := by
84   unfold summand codimension
85   rw [lower_card k' K A i, lower_card k' K A 0, fixed_eq k k' K A ρ i]
86 
87 theorem swan_eq
88     (ρ : Representation ℂ (Pullback (residue A (A.decompositionSubgroup K))
89       (geometric k (ResidueField A))) V) :
90     swan A (A.decompositionSubgroup (liftedField k' K A)) (geometric k' (ResidueField A))
91       (ρ.comp (HenselianWeilAttachment.embedding k k' K A)) =
92     swan A (A.decompositionSubgroup K) (geometric k (ResidueField A)) ρ := by
93   unfold swan
94   apply tsum_congr
95   intro i
96   exact summand_eq k k' K A ρ (i+1)
97 
98 theorem artin_eq
99     (ρ : Representation ℂ (Pullback (residue A (A.decompositionSubgroup K))
100       (geometric k (ResidueField A))) V) :
101     artin A (A.decompositionSubgroup (liftedField k' K A)) (geometric k' (ResidueField A))
102       (ρ.comp (HenselianWeilAttachment.embedding k k' K A)) =
103     artin A (A.decompositionSubgroup K) (geometric k (ResidueField A)) ρ := by
104   unfold artin codimension
105   rw [swan_eq, fixed_eq]
106 
107 /-- For a finite decomposition group over a DVR, the common sum is summable. -/
108 theorem summable_source [IsDiscreteValuationRing A] [Finite (A.decompositionSubgroup K)]
109     (ρ : Representation ℂ (Pullback (residue A (A.decompositionSubgroup K))
110       (geometric k (ResidueField A))) V) :
111     Summable (summand A (A.decompositionSubgroup (liftedField k' K A))
112       (geometric k' (ResidueField A)) (ρ.comp (HenselianWeilAttachment.embedding k k' K A))) := by
113   have h : summand A (A.decompositionSubgroup (liftedField k' K A))
114       (geometric k' (ResidueField A)) (ρ.comp (HenselianWeilAttachment.embedding k k' K A)) =
115       summand A (A.decompositionSubgroup K) (geometric k (ResidueField A)) ρ := by
116     funext i; exact summand_eq k k' K A ρ i
117   rw [h]
118   exact summable_summands A (A.decompositionSubgroup K) _ ρ
119 
120 end PaperXI.HenselianConductorTransport

Back to source controls