QuadraticGaloisInertia.lean

1 import PaperX.QuadraticLocalGalois
2 import PaperX.QuadraticPadicInertia
3 import PaperX.QuadraticLocalPackets
4 
5 /-! Actual inertia restrictions of the fixed global quadratic packet.
6 The quantified inertia groups are the residue-action kernels inside the
7 valuation decomposition groups. Local domination is explicitly inhabited. -/
8 set_option autoImplicit false
9 noncomputable section
10 namespace PaperX.QuadraticGaloisInertia
11 open PaperX.QuadraticGalois PaperX.QuadraticLocalGalois
12 open PaperX.QuadraticPadicInertia PaperX.QuadraticLocalPackets
13 
14 variable (p : ℕ) [Fact p.Prime]
15 variable {B C : Type*} [CommRing B] [CommRing C]
16 
17 /-- The inclusion into the actual local absolute Galois group. -/
18 def decompositionInclusion (A : ValuationSubring (LocalClosure p)) :
19     A.decompositionSubgroup ℚ_[p] →* Field.absoluteGaloisGroup ℚ_[p] :=
20   (A.decompositionSubgroup ℚ_[p]).subtype
21 
22 theorem quotient_on_inertia (hodd : p ≠ 2)
23     (A : ValuationSubring (LocalClosure p))
24     (h : ∀ x : ℤ_[p], integralMap p x ∈ A)
25     (σ : A.decompositionSubgroup ℚ_[p]) (hσ : σ ∈ A.inertiaSubgroup ℚ_[p]) :
26     localQuotient ℚ_[p] (decompositionInclusion p A σ) = 1 :=
27   (localQuotient_eq_one_iff ℚ_[p] _).mpr
28     (inertia_fixes_square_neg_one p hodd A h _ (localRoot_sq ℚ_[p]) σ hσ)
29 
30 theorem packet_on_inertia (hodd : p ≠ 2) (χ : Packet B)
31     (A : ValuationSubring (LocalClosure p))
32     (h : ∀ x : ℤ_[p], integralMap p x ∈ A)
33     (σ : A.decompositionSubgroup ℚ_[p]) (hσ : σ ∈ A.inertiaSubgroup ℚ_[p]) :
34     localCharacter ℚ_[p] χ (decompositionInclusion p A σ) = 1 := by
35   apply χ.property
36   exact quotient_on_inertia p hodd A h σ hσ
37 
38 /-- Triviality on every actual inertia subgroup above the integral coefficient ring. -/
39 def InertiaTrivial (χ : Packet B) : Prop :=
40   ∀ (A : ValuationSubring (LocalClosure p))
41     (_h : ∀ x : ℤ_[p], integralMap p x ∈ A)
42     (σ : A.decompositionSubgroup ℚ_[p]), σ ∈ A.inertiaSubgroup ℚ_[p] →
43       localCharacter ℚ_[p] χ (decompositionInclusion p A σ) = 1
44 
45 theorem inertiaTrivial_of_odd (hodd : p ≠ 2) (χ : Packet B) : InertiaTrivial p χ :=
46   packet_on_inertia p hodd χ
47 
48 theorem inertiaTrivial_map (f : B →+* C) (χ : Packet B)
49     (hχ : InertiaTrivial p χ) : InertiaTrivial p (mapPacket f χ) := by
50   intro A h σ hσ
51   rw [localCharacter_natural, MonoidHom.comp_apply, hχ A h σ hσ, map_one]
52 
53 /-- The inertia statement is nonvacuous: a locally dominating valuation exists. -/
54 theorem exists_dominating_inertia_trivial (hodd : p ≠ 2) :
55     ∃ (A : ValuationSubring (LocalClosure p))
56       (h : ∀ x : ℤ_[p], integralMap p x ∈ A),
57       IsLocalHom ((integralMap p).codRestrict A.toSubring h) ∧
58       ∀ (χ : Packet B) (σ : A.decompositionSubgroup ℚ_[p]),
59         σ ∈ A.inertiaSubgroup ℚ_[p] →
60           localCharacter ℚ_[p] χ (decompositionInclusion p A σ) = 1 := by
61   obtain ⟨A, h, hl⟩ := exists_dominating_valuation p
62   exact ⟨A, h, hl, fun χ σ hσ => packet_on_inertia p hodd χ A h σ hσ⟩
63 
64 end PaperX.QuadraticGaloisInertia

Back to source controls