ValuationTameEndpoint.lean

1 import PaperXI.ValuationConductor
2 import Mathlib.FieldTheory.Finite.Basic
3 import Mathlib.RingTheory.DiscreteValuationRing.Basic
4 
5 /-! Actual valuation-ring specialization with a constructed geometric residue
6 Frobenius. The finite residue-base embedding remains declared. There is no
7 claimed identification with an absolute Weil group or extension-independent
8 arithmetic conductor. -/
9 set_option autoImplicit false
10 noncomputable section
11 namespace PaperXI.ValuationTameEndpoint
12 open PaperXI.ResidueWeil PaperXI.ValuationConductor PaperXI.ValuationRamification
13 
14 variable (k : Type*) [Field k] [Fintype k]
15 variable (K : Type*) {L : Type*} [Field K] [Field L] [Algebra K L]
16 variable (A : ValuationSubring L) [Algebra k (IsLocalRing.ResidueField A)]
17   [Algebra.IsAlgebraic k (IsLocalRing.ResidueField A)]
18 
19 /-- Inverse of the actual q-power residue automorphism, q = card k. -/
20 def geometricFrobenius : RingAut (IsLocalRing.ResidueField A) :=
21   (FiniteField.frobeniusAlgEquivOfAlgebraic k (IsLocalRing.ResidueField A)).symm.toRingEquiv
22 
23 /-- The convention is fixed by its q-power identity, not an arbitrary scalar label. -/
24 theorem geometric_power (x : IsLocalRing.ResidueField A) :
25     (geometricFrobenius k A x) ^ Fintype.card k = x :=
26   (FiniteField.frobeniusAlgEquivOfAlgebraic k (IsLocalRing.ResidueField A)).apply_symm_apply x
27 
28 abbrev WeilPullback := valuationGroup K A (geometricFrobenius k A)
29 
30 def inertiaIdentification :
31     (degree (residueAction K A) (geometricFrobenius k A)).ker ≃* A.inertiaSubgroup K :=
32   valuationInertiaEquiv K A (geometricFrobenius k A)
33 
34 variable {V : Type*} [AddCommGroup V] [Module ℂ V] [FiniteDimensional ℂ V]
35 
36 /-- Source-facing arithmetic-ring endpoint. All groups and weights come from A;
37 the hypothesis is trivial action of the first actual congruence subgroup. -/
38 theorem conductor [IsDiscreteValuationRing A] [Finite (A.decompositionSubgroup K)]
39     (ρ : Representation ℂ (WeilPullback k K A) V) [Representation.IsIrreducible ρ]
40     (ht : ∀ g : lower A (A.decompositionSubgroup K) 1,
41       ρ (lift A (A.decompositionSubgroup K) (geometricFrobenius k A) 1 g) = 1)
42     (hdim : 1 < Module.finrank ℂ V) :
43     fixed A (A.decompositionSubgroup K) (geometricFrobenius k A) ρ 0 = ⊥ ∧
44     swan A (A.decompositionSubgroup K) (geometricFrobenius k A) ρ = 0 ∧
45     artin A (A.decompositionSubgroup K) (geometricFrobenius k A) ρ =
46       (Module.finrank ℂ V : ℝ) ∧
47     Summable (summand A (A.decompositionSubgroup K) (geometricFrobenius k A) ρ) := by
48   obtain ⟨hf, hs, ha⟩ := tame_irreducible_dimension A (A.decompositionSubgroup K)
49     (geometricFrobenius k A) ρ ht hdim
50   exact ⟨hf, hs, ha, summable_summands A (A.decompositionSubgroup K) (geometricFrobenius k A) ρ⟩
51 
52 end PaperXI.ValuationTameEndpoint

Back to source controls