RamificationPolyphaseBaseChange.lean

1 import PaperXI.RamificationPolyphase
2 import PaperXI.UnramifiedConductor
3 
4 /-! # Unramified transport of ramification polyphase channels
5 
6 For an inertia-containing subgroup and the corresponding Frobenius power
7 change, every literal lower-depth averaging projector is preserved. Hence every
8 successive ramification-detail projector is preserved as an actual endomorphism,
9 not only at the level of dimensions or conductor sums.
10 -/
11 set_option autoImplicit false
12 noncomputable section
13 open scoped Classical BigOperators
14 
15 namespace PaperXI.RamificationPolyphaseBaseChange
16 
17 open PaperXI.ResidueWeil
18 open PaperXI.ValuationRamification
19 open PaperXI.ValuationConductor
20 open PaperXI.UnramifiedConductor
21 open PaperXI.RamificationPolyphase
22 open PaperXI.FiniteAverage
23 
24 variable (R D : Type*) [CommRing R] [IsLocalRing R] [Group D] [Fintype D]
25   [MulSemiringAction D R]
26 variable (H : Subgroup D)
27 variable (F F' : RingAut (IsLocalRing.ResidueField R))
28 variable (n : ℕ) (hp : F ^ n = F') (hI : lower R D 0 ≤ H)
29 variable {V : Type*} [AddCommGroup V] [Module ℂ V]
30 variable (ρ : Representation ℂ (Pullback (residue R D) F) V)
31 
32 include hI
33 
34 /-- Reindexing the restricted lower group by its actual equivalence with the
35 ambient lower group preserves the literal Reynolds projector. -/
36 theorem depthProjector_eq (i : ℕ) :
37     depthProjector (R := R) (D := H) (F := F')
38         (ρ := ρ.comp (embedding R D H F F' n hp)) i =
39       depthProjector (R := R) (D := D) (F := F) (ρ := ρ) i := by
40   ext v
41   simp only [depthProjector, average_apply]
42   have hcard : Fintype.card (lower R H i) = Fintype.card (lower R D i) :=
43     Fintype.card_congr (lowerEquiv R D H hI i).toEquiv
44   rw [hcard]
45   congr 1
46   calc
47     (∑ g : lower R H i,
48         (ρ.comp (embedding R D H F F' n hp)) (lift R H F' i g) v) =
49       ∑ g : lower R H i, ρ (lift R D F i (lowerEquiv R D H hI i g)) v := by
50         apply Finset.sum_congr rfl
51         intro g _
52         rw [MonoidHom.comp_apply, embedding_lift R D H F F' n hp hI]
53     _ = ∑ g : lower R D i, ρ (lift R D F i g) v := by
54       exact (lowerEquiv R D H hI i).toEquiv.sum_comp
55         (fun g : lower R D i => ρ (lift R D F i g) v)
56 
57 /-- Every ramification-detail channel is preserved as the same endomorphism of
58 the same representation space. -/
59 theorem detailProjector_eq (i : ℕ) :
60     detailProjector (R := R) (D := H) (F := F')
61         (ρ := ρ.comp (embedding R D H F F' n hp)) i =
62       detailProjector (R := R) (D := D) (F := F) (ρ := ρ) i := by
63   unfold detailProjector
64   rw [depthProjector_eq R D H F F' n hp hI ρ (i+1),
65     depthProjector_eq R D H F F' n hp hI ρ i]
66 
67 /-- The newly visible detail subspace is literally unchanged by unramified
68 restriction. -/
69 theorem detailRange_eq (i : ℕ) :
70     LinearMap.range
71         (detailProjector (R := R) (D := H) (F := F')
72           (ρ := ρ.comp (embedding R D H F F' n hp)) i) =
73       LinearMap.range
74         (detailProjector (R := R) (D := D) (F := F) (ρ := ρ) i) := by
75   rw [detailProjector_eq R D H F F' n hp hI ρ i]
76 
77 /-- The full finite-depth polyphase reconstruction is preserved term by term. -/
78 theorem finiteReconstruction_eq (N : ℕ) :
79     depthProjector (R := R) (D := H) (F := F')
80         (ρ := ρ.comp (embedding R D H F F' n hp)) 0 +
81         ∑ i ∈ Finset.range N,
82           detailProjector (R := R) (D := H) (F := F')
83             (ρ := ρ.comp (embedding R D H F F' n hp)) i =
84       depthProjector (R := R) (D := D) (F := F) (ρ := ρ) 0 +
85         ∑ i ∈ Finset.range N,
86           detailProjector (R := R) (D := D) (F := F) (ρ := ρ) i := by
87   rw [depthProjector_eq R D H F F' n hp hI ρ 0]
88   apply congrArg (fun z => depthProjector (R := R) (D := D) (F := F) (ρ := ρ) 0 + z)
89   apply Finset.sum_congr rfl
90   intro i hi
91   rw [detailProjector_eq R D H F F' n hp hI ρ i]
92 
93 omit [Fintype D] in
94 /-- The existing conductor summand is recovered unchanged together with the
95 stronger projector-level statement. -/
96 theorem conductorSummand_eq (i : ℕ) :
97     summand R H F' (ρ.comp (embedding R D H F F' n hp)) i =
98       summand R D F ρ i :=
99   summand_eq R D H F F' n hp hI ρ i
100 
101 omit [Fintype D] in
102 /-- Swan invariance follows without collapsing the individual detail channels. -/
103 theorem swan_eq :
104     swan R H F' (ρ.comp (embedding R D H F F' n hp)) =
105       swan R D F ρ :=
106   UnramifiedConductor.swan_eq R D H F F' n hp hI ρ
107 
108 omit [Fintype D] in
109 /-- Artin invariance follows without collapsing the individual detail channels. -/
110 theorem artin_eq :
111     artin R H F' (ρ.comp (embedding R D H F F' n hp)) =
112       artin R D F ρ :=
113   UnramifiedConductor.artin_eq R D H F F' n hp hI ρ
114 
115 end PaperXI.RamificationPolyphaseBaseChange

Back to source controls