UnramifiedValuation.lean

1 import PaperXI.FiniteResidueSubgroup
2 import PaperXI.UnramifiedConductor
3 import PaperXI.ValuationTameEndpoint
4 
5 /-! Source-facing unramified residue-base attachment to an actual valuation
6 subring and decomposition-group action. The subgroup fixes the actual embedded
7 finite residue extension, rather than being assigned an index by a certificate.
8 This still does not construct its lift to a local-field unramified extension. -/
9 set_option autoImplicit false
10 noncomputable section
11 namespace PaperXI.UnramifiedValuation
12 open PaperXI.ResidueWeil PaperXI.ResidueDegreeBaseChange PaperXI.FiniteResidueBaseChange
13 open PaperXI.ValuationRamification PaperXI.ValuationConductor
14 
15 variable (k k' K : Type*) {L : Type*} [Field k] [Fintype k] [Field k'] [Fintype k']
16   [Algebra k k'] [Field K] [Field L] [Algebra K L]
17 variable (A : ValuationSubring L) [Algebra k (IsLocalRing.ResidueField A)]
18   [Algebra k' (IsLocalRing.ResidueField A)]
19   [Algebra.IsAlgebraic k (IsLocalRing.ResidueField A)]
20   [Algebra.IsAlgebraic k' (IsLocalRing.ResidueField A)]
21 
22 abbrev fixingGroup :=
23   FiniteResidueSubgroup.fixing k' (IsLocalRing.ResidueField A)
24     (residue A (A.decompositionSubgroup K))
25 
26 /-- No new convention relative to the preceding valuation release. -/
27 theorem frobenius_agrees : geometric k (IsLocalRing.ResidueField A) =
28     ValuationTameEndpoint.geometricFrobenius k A := rfl
29 
30 omit [Fintype k'] [Algebra.IsAlgebraic k' (IsLocalRing.ResidueField A)] in
31 /-- The pointwise residue-field stabilizer contains all actual inertia. -/
32 theorem contains_inertia : lower A (A.decompositionSubgroup K) 0 ≤ fixingGroup k' K A := by
33   rw [lower_zero_eq_residue_kernel]
34   exact FiniteResidueSubgroup.kernel_le_fixing k' (IsLocalRing.ResidueField A) _
35 
36 /-- Natural inclusion of the two actually constructed residue-action pullbacks. -/
37 def embedding :
38     Pullback (residue A (fixingGroup k' K A)) (geometric k' (IsLocalRing.ResidueField A)) →*
39       Pullback (residue A (A.decompositionSubgroup K)) (geometric k (IsLocalRing.ResidueField A)) :=
40   UnramifiedConductor.embedding A (A.decompositionSubgroup K) (fixingGroup k' K A)
41     (geometric k (IsLocalRing.ResidueField A)) (geometric k' (IsLocalRing.ResidueField A))
42     (Module.finrank k k') (geometric_tower k (IsLocalRing.ResidueField A) k')
43 
44 /-- The arithmetic field degree controls the integer degree dilation. -/
45 theorem degree_formula (w : Pullback (residue A (fixingGroup k' K A))
46     (geometric k' (IsLocalRing.ResidueField A))) :
47     Multiplicative.toAdd (degree (residue A (A.decompositionSubgroup K))
48       (geometric k (IsLocalRing.ResidueField A)) (embedding k k' K A w)) =
49     (Module.finrank k k' : ℤ) * Multiplicative.toAdd
50       (degree (residue A (fixingGroup k' K A)) (geometric k' (IsLocalRing.ResidueField A)) w) := rfl
51 
52 /-- The equivalence is to the subgroup defined by divisibility, not merely a subgroup
53 having the same finite index. -/
54 def degreeSubgroupEquiv :
55     Pullback (residue A (fixingGroup k' K A)) (geometric k' (IsLocalRing.ResidueField A)) ≃*
56       periodSubgroup (residue A (A.decompositionSubgroup K))
57         (geometric k (IsLocalRing.ResidueField A)) (Module.finrank k k') :=
58   FiniteResidueSubgroup.unramifiedEquiv k k' (IsLocalRing.ResidueField A) _
59 
60 /-- This direct inclusion is faithful before passing to a quotient. -/
61 theorem embedding_injective : Function.Injective (embedding k k' K A) :=
62   UnramifiedConductor.embedding_injective A (A.decompositionSubgroup K) (fixingGroup k' K A)
63     _ _ Module.finrank_pos.ne' (geometric_tower k (IsLocalRing.ResidueField A) k')
64 
65 /-- The natural embedding has exactly the stated degree-divisible range. -/
66 theorem embedding_range : (embedding k k' K A).range =
67     periodSubgroup (residue A (A.decompositionSubgroup K))
68       (geometric k (IsLocalRing.ResidueField A)) (Module.finrank k k') := by
69   ext w
70   constructor
71   · rintro ⟨v, rfl⟩
72     rw [mem_periodSubgroup, degree_formula]
73     exact dvd_mul_right _ _
74   · intro hw
75     obtain ⟨m, hm⟩ := (mem_periodSubgroup _ _ _ w).mp hw
76     have hg : w.val.1 ∈ fixingGroup k' K A :=
77       (FiniteResidueSubgroup.projection_mem_iff k k' (IsLocalRing.ResidueField A) _ w).mpr
78         ((mem_periodSubgroup _ _ _ w).mp hw)
79     let v : Pullback (residue A (fixingGroup k' K A)) (geometric k' (IsLocalRing.ResidueField A)) :=
80       ⟨(⟨w.val.1, hg⟩, Multiplicative.ofAdd m), by
81         change residue A (A.decompositionSubgroup K) w.val.1 =
82           geometric k' (IsLocalRing.ResidueField A) ^ m
83         rw [← geometric_tower k (IsLocalRing.ResidueField A) k', ← zpow_natCast, ← zpow_mul, ← hm]
84         exact w.property⟩
85     refine ⟨v, ?_⟩
86     apply Subtype.ext
87     apply Prod.ext
88     · rfl
89     · exact Multiplicative.toAdd.injective hm.symm
90 
91 omit [Algebra k' (IsLocalRing.ResidueField A)] [Algebra.IsAlgebraic k' (IsLocalRing.ResidueField A)] in
92 /-- Index f is a theorem once degree one lifts; existence of that lift stays explicit. -/
93 theorem degree_index (hF : geometric k (IsLocalRing.ResidueField A) ∈
94     (residue A (A.decompositionSubgroup K)).range) :
95     Nat.card (Pullback (residue A (A.decompositionSubgroup K))
96       (geometric k (IsLocalRing.ResidueField A)) ⧸
97       periodSubgroup (residue A (A.decompositionSubgroup K))
98         (geometric k (IsLocalRing.ResidueField A)) (Module.finrank k k')) = Module.finrank k k' := by
99   let : NeZero (Module.finrank k k') := ⟨Module.finrank_pos.ne'⟩
100   exact quotient_card _ _ _ hF
101 
102 /-- Compatible q^{-degree} normalization; no reduction of integer degree modulo a residue order. -/
103 theorem norm_compatibility (w : Pullback (residue A (fixingGroup k' K A))
104     (geometric k' (IsLocalRing.ResidueField A))) :
105     (Fintype.card k' : ℝ) ^ (-Multiplicative.toAdd
106       (degree (residue A (fixingGroup k' K A)) (geometric k' (IsLocalRing.ResidueField A)) w)) =
107     (Fintype.card k : ℝ) ^ (-Multiplicative.toAdd
108       (degree (residue A (A.decompositionSubgroup K)) (geometric k (IsLocalRing.ResidueField A))
109         (embedding k k' K A w))) := by
110   have hc : (Fintype.card k' : ℝ) = (Fintype.card k : ℝ) ^ Module.finrank k k' := by
111     exact_mod_cast (Module.card_eq_pow_finrank (K := k) (V := k'))
112   rw [hc, ← zpow_natCast, ← zpow_mul, degree_formula, mul_neg]
113 
114 variable {V : Type*} [AddCommGroup V] [Module ℂ V]
115 
116 /-- All fixed spaces and ALL weighted terms are invariant under the actual residue-base restriction.
117 The statement does not assume tame action, irreducibility, or a precomputed conductor. -/
118 theorem source [IsDiscreteValuationRing A] [Finite (A.decompositionSubgroup K)]
119     (ρ : Representation ℂ (Pullback (residue A (A.decompositionSubgroup K))
120       (geometric k (IsLocalRing.ResidueField A))) V) :
121     (∀ i : ℕ, Nat.card (lower A (fixingGroup k' K A) i) = Nat.card (lower A (A.decompositionSubgroup K) i)) ∧
122     (∀ i : ℕ, fixed A (fixingGroup k' K A) (geometric k' (IsLocalRing.ResidueField A))
123       (ρ.comp (embedding k k' K A)) i =
124       fixed A (A.decompositionSubgroup K) (geometric k (IsLocalRing.ResidueField A)) ρ i) ∧
125     (∀ i : ℕ, summand A (fixingGroup k' K A) (geometric k' (IsLocalRing.ResidueField A))
126       (ρ.comp (embedding k k' K A)) i =
127       summand A (A.decompositionSubgroup K) (geometric k (IsLocalRing.ResidueField A)) ρ i) ∧
128     swan A (fixingGroup k' K A) (geometric k' (IsLocalRing.ResidueField A))
129       (ρ.comp (embedding k k' K A)) =
130       swan A (A.decompositionSubgroup K) (geometric k (IsLocalRing.ResidueField A)) ρ ∧
131     artin A (fixingGroup k' K A) (geometric k' (IsLocalRing.ResidueField A))
132       (ρ.comp (embedding k k' K A)) =
133       artin A (A.decompositionSubgroup K) (geometric k (IsLocalRing.ResidueField A)) ρ ∧
134     Summable (summand A (fixingGroup k' K A) (geometric k' (IsLocalRing.ResidueField A))
135       (ρ.comp (embedding k k' K A))) := by
136   let hI := contains_inertia k' K A
137   let hp := geometric_tower k (IsLocalRing.ResidueField A) k'
138   exact ⟨UnramifiedConductor.lower_card A (A.decompositionSubgroup K) _ hI,
139     UnramifiedConductor.fixed_eq A (A.decompositionSubgroup K) _ _ _ _ hp hI ρ,
140     UnramifiedConductor.summand_eq A (A.decompositionSubgroup K) _ _ _ _ hp hI ρ,
141     UnramifiedConductor.swan_eq A (A.decompositionSubgroup K) _ _ _ _ hp hI ρ,
142     UnramifiedConductor.artin_eq A (A.decompositionSubgroup K) _ _ _ _ hp hI ρ,
143     UnramifiedConductor.summable_restriction A (A.decompositionSubgroup K) _ _ _ _ hp hI ρ⟩
144 
145 end PaperXI.UnramifiedValuation

Back to source controls