ResidueWeil.lean

1 import PaperXI.NormalInertia
2 import Mathlib.RingTheory.Valuation.RamificationGroup
3 import Mathlib.GroupTheory.QuotientGroup.Basic
4 
5 /-! A pullback of an actual residue-field action along the integer powers of a
6 chosen residue automorphism. No equivalence with the absolute local Weil group
7 is postulated. The inertia identification below is with Mathlib's valuation
8 inertia subgroup, not with an independently named abstract kernel. -/
9 set_option autoImplicit false
10 noncomputable section
11 open scoped Classical
12 
13 namespace PaperXI.ResidueWeil
14 
15 variable {D C : Type*} [Group D] [Group C]
16 
17 /-- The infinite degree direction is retained, even for finite residue data. -/
18 def subgroup (r : D →* C) (F : C) : Subgroup (D × Multiplicative ℤ) where
19   carrier := {x | r x.1 = F ^ Multiplicative.toAdd x.2}
20   one_mem' := by simp
21   mul_mem' := by
22     intro a b ha hb
23     change r (a.1 * b.1) = F ^ (Multiplicative.toAdd a.2 + Multiplicative.toAdd b.2)
24     rw [map_mul, ha, hb, zpow_add]
25   inv_mem' := by
26     intro a ha
27     change r a.1⁻¹ = F ^ (-Multiplicative.toAdd a.2)
28     rw [map_inv, ha, zpow_neg]
29 
30 abbrev Pullback (r : D →* C) (F : C) := subgroup r F
31 
32 def projection (r : D →* C) (F : C) : Pullback r F →* D :=
33   (MonoidHom.fst D (Multiplicative ℤ)).comp (subgroup r F).subtype
34 
35 def degree (r : D →* C) (F : C) : Pullback r F →* Multiplicative ℤ :=
36   (MonoidHom.snd D (Multiplicative ℤ)).comp (subgroup r F).subtype
37 
38 @[simp] theorem projection_apply (r : D →* C) (F : C) (w : Pullback r F) :
39     projection r F w = w.val.1 := rfl
40 
41 @[simp] theorem degree_apply (r : D →* C) (F : C) (w : Pullback r F) :
42     degree r F w = w.val.2 := rfl
43 
44 /-- The degree kernel is precisely residue inertia, with inverse g ↦ (g,0). -/
45 def inertiaEquiv (r : D →* C) (F : C) : (degree r F).ker ≃* r.ker where
46   toFun w := ⟨w.val.val.1, by
47     change r w.val.val.1 = 1
48     have h : r w.val.val.1 = F ^ Multiplicative.toAdd w.val.val.2 := w.val.property
49     have hz : w.val.val.2 = 1 := w.property
50     rw [hz] at h
51     simpa using h⟩
52   invFun g := ⟨⟨(g.val, 1), by
53     change r g.val = F ^ (0 : ℤ)
54     simpa only [zpow_zero] using (show r g.val = 1 from g.property)⟩, rfl⟩
55   left_inv w := by
56     apply Subtype.ext
57     apply Subtype.ext
58     apply Prod.ext
59     · rfl
60     · exact w.property.symm
61   right_inv g := rfl
62   map_mul' _ _ := rfl
63 
64 /-- The quotient needs only to embed into the abelian degree group. -/
65 instance degreeQuotientCommutative (r : D →* C) (F : C) :
66     IsMulCommutative (Pullback r F ⧸ (degree r F).ker) := by
67   apply IsMulCommutative.of_comm
68   intro a b
69   apply QuotientGroup.kerLift_injective (degree r F)
70   simp only [map_mul, mul_comm]
71 
72 /-- A degree-one lift exists exactly when the selected residue automorphism lifts. -/
73 theorem exists_degree_one_iff (r : D →* C) (F : C) :
74     (∃ w : Pullback r F, degree r F w = Multiplicative.ofAdd (1 : ℤ)) ↔
75     F ∈ r.range := by
76   constructor
77   · rintro ⟨w, hw⟩
78     refine ⟨projection r F w, ?_⟩
79     have hh : r w.val.1 = F ^ Multiplicative.toAdd w.val.2 := w.property
80     change w.val.2 = Multiplicative.ofAdd (1 : ℤ) at hw
81     simpa [hw] using hh
82   · rintro ⟨g, hg⟩
83     refine ⟨⟨(g, Multiplicative.ofAdd (1 : ℤ)), ?_⟩, rfl⟩
84     change r g = F ^ (1 : ℤ)
85     simpa using hg
86 
87 section Valuation
88 variable (K : Type*) {L : Type*} [Field K] [Field L] [Algebra K L]
89 
90 abbrev residueAction (A : ValuationSubring L) :
91     A.decompositionSubgroup K →* RingAut (IsLocalRing.ResidueField A) :=
92   MulSemiringAction.toRingAut (A.decompositionSubgroup K) (IsLocalRing.ResidueField A)
93 
94 abbrev valuationGroup (A : ValuationSubring L) (F : RingAut (IsLocalRing.ResidueField A)) :=
95   Pullback (residueAction K A) F
96 
97 /-- Specialization to the actual valuation-ring inertia subgroup. -/
98 def valuationInertiaEquiv (A : ValuationSubring L)
99     (F : RingAut (IsLocalRing.ResidueField A)) :
100     (degree (residueAction K A) F).ker ≃* A.inertiaSubgroup K :=
101   inertiaEquiv (residueAction K A) F
102 
103 variable {V : Type*} [AddCommGroup V] [Module ℂ V] [FiniteDimensional ℂ V]
104 
105 /-- No cyclic finite-inertia presentation is needed for this vanishing result. -/
106 theorem valuation_invariants_eq_bot (A : ValuationSubring L)
107     (F : RingAut (IsLocalRing.ResidueField A))
108     (ρ : Representation ℂ (valuationGroup K A F) V) [Representation.IsIrreducible ρ]
109     (hdim : 1 < Module.finrank ℂ V) :
110     Representation.invariants (ρ.comp (degree (residueAction K A) F).ker.subtype) = ⊥ :=
111   NormalInertia.fixed_eq_bot_of_dimension_gt_one ρ (degree (residueAction K A) F).ker hdim
112 
113 end Valuation
114 end PaperXI.ResidueWeil

Back to source controls