UnramifiedConductorZero.lean

1 import PaperXI.UnramifiedLocalFactor
2 import PaperXI.ValuationConductor
3 
4 /-! # Conductor zero for the finite unramified Weil model
5 
6 This module does two separate things.
7 
8 * It proves a generic theorem in the existing `ValuationConductor` interface:
9   a representation has Artin conductor zero when the actual degree-kernel inertia
10   subgroup is trivial.
11 * It packages the corresponding codimension/Swan/Artin exponents for the finite
12   unramified Weil model constructed in Block 39.
13 
14 The model-specific exponents are not asserted to be the conductor of an absolute
15 Weil representation. They record the exact unramified specialization of the
16 existing fixed-space formula.
17 -/
18 
19 set_option autoImplicit false
20 noncomputable section
21 
22 open scoped Classical
23 
24 namespace PaperXI.ValuationConductor
25 
26 open PaperXI.ResidueWeil PaperXI.ValuationRamification
27 
28 variable (R D : Type*) [CommRing R] [IsLocalRing R] [Group D] [MulSemiringAction D R]
29 variable {V : Type*} [AddCommGroup V] [Module ℂ V]
30 
31 /-- In the existing lower-numbering conductor interface, a literally trivial
32 inertia subgroup forces both the Swan term and the zeroth fixed-space defect to
33 vanish. No irreducibility assumption is required. -/
34 theorem artin_zero_of_degree_kernel_bot
35     (F : RingAut (IsLocalRing.ResidueField R))
36     (ρ : Representation ℂ (Pullback (residue R D) F) V)
37     (hI : (degree (residue R D) F).ker = ⊥) :
38     artin R D F ρ = 0 := by
39   have ht : ∀ g : lower R D 1, ρ (lift R D F 1 g) = 1 := by
40     intro g
41     have hg : lift R D F 1 g ∈ (degree (residue R D) F).ker := by
42       change degree (residue R D) F (lift R D F 1 g) = 1
43       exact lift_degree R D F 1 g
44     have hbot : lift R D F 1 g ∈ (⊥ : Subgroup (Pullback (residue R D) F)) := by
45       rw [← hI]
46       exact hg
47     have he : lift R D F 1 g = 1 := by
48       simpa only [Subgroup.mem_bot] using hbot
49     simp [he]
50   have htop : fixed R D F ρ 0 = ⊤ := by
51     rw [fixed_zero]
52     exact (PaperXI.NormalInertia.fixed_top_iff_le_kernel ρ
53       (degree (residue R D) F).ker).2 (by rw [hI]; exact bot_le)
54   rw [artin, tame_swan_zero R D F ρ ht]
55   unfold codimension
56   rw [htop]
57   simp
58 
59 end PaperXI.ValuationConductor
60 
61 namespace PaperXI.FiniteUnramifiedWeil
62 
63 open PaperXI.ResidueWeil
64 open ValuativeRel
65 
66 variable (K : Type*) [Field K] [ValuativeRel K] [UniformSpace K]
67   [IsUniformAddGroup K] [IsNonarchimedeanLocalField K]
68 variable (s : Type*) [Field s] [Algebra 𝓀[K] s]
69   [FiniteDimensional 𝓀[K] s]
70 variable {V : Type*} [AddCommGroup V] [Module ℂ V]
71 
72 /-- The fixed-space defect at inertia for the finite unramified model. -/
73 def inertiaCodimension [FiniteDimensional ℂ V]
74     (ρ : Representation ℂ (UnramifiedWeil K s) V) : ℕ :=
75   Module.finrank ℂ V - Module.finrank ℂ
76     (Representation.invariants (ρ.comp (Inertia K s).subtype))
77 
78 /-- There are no positive-depth ramification contributions in the finite
79 unramified model. -/
80 def swanConductorExponent
81     (_ρ : Representation ℂ (UnramifiedWeil K s) V) : ℝ := 0
82 
83 /-- Artin exponent in the unramified fixed-space specialization. -/
84 def artinConductorExponent [FiniteDimensional ℂ V]
85     (ρ : Representation ℂ (UnramifiedWeil K s) V) : ℝ :=
86   (inertiaCodimension K s ρ : ℝ) + swanConductorExponent K s ρ
87 
88 /-- Trivial model inertia makes the inertia codimension zero. -/
89 theorem inertiaCodimension_eq_zero [FiniteDimensional ℂ V]
90     (ρ : Representation ℂ (UnramifiedWeil K s) V) :
91     inertiaCodimension K s ρ = 0 := by
92   unfold inertiaCodimension
93   rw [inertia_invariants_eq_top K s ρ]
94   simp
95 
96 @[simp]
97 theorem swanConductorExponent_eq_zero
98     (ρ : Representation ℂ (UnramifiedWeil K s) V) :
99     swanConductorExponent K s ρ = 0 := rfl
100 
101 /-- Every finite-dimensional representation of the finite unramified model has
102 conductor exponent zero in this specialization. -/
103 theorem artinConductorExponent_eq_zero [FiniteDimensional ℂ V]
104     (ρ : Representation ℂ (UnramifiedWeil K s) V) :
105     artinConductorExponent K s ρ = 0 := by
106   rw [artinConductorExponent, inertiaCodimension_eq_zero]
107   simp
108 
109 end PaperXI.FiniteUnramifiedWeil

Back to source controls