QuadraticLocalArithmetic.lean

1 import PaperX.QuadraticLocalCompletion
2 import PaperX.PadicQuadraticSplitting
3 import PaperX.QuadraticGaloisInertia
4 
5 /-! Explicit local arithmetic conditions and their simultaneous completion.
6 The arithmetic prime is independent of the coefficient prime. -/
7 set_option autoImplicit false
8 noncomputable section
9 namespace PaperX.QuadraticLocalArithmetic
10 open PaperX.QuadraticGalois PaperX.QuadraticGaloisPackets
11 open PaperX.QuadraticLocalGalois PaperX.QuadraticLocalPackets
12 open PaperX.QuadraticLocalCompletion PaperX.QuadraticArithmeticCompletion
13 open PaperX.QuadraticGaloisInertia PaperX.PadicQuadraticSplitting
14 
15 variable (p : ℕ) [Fact p.Prime]
16 variable {B : Type*} [CommRing B]
17 
18 theorem localQuotient_trivial_iff_mod_four :
19     localQuotient ℚ_[p] = 1 ↔ p % 4 = 1 := by
20   rw [localQuotient_trivial_iff, root_iff_mod_four_eq_one]
21 
22 theorem localQuotient_surjective_of_not_split (hp : p % 4 ≠ 1) :
23     Function.Surjective (localQuotient ℚ_[p]) :=
24   localQuotient_surjective ℚ_[p] (fun h => hp ((root_iff_mod_four_eq_one p).mp h))
25 
26 theorem locallyTrivial_iff_mod_four (χ : Packet B) :
27     LocallyTrivial ℚ_[p] χ ↔ p % 4 = 1 ∨ χ = ofRoot (oneRoot B) := by
28   rw [locallyTrivial_iff, root_iff_mod_four_eq_one]
29 
30 theorem nonsplit_localCharacter_injective (hp : p % 4 ≠ 1) :
31     Function.Injective (localCharacter ℚ_[p] (B := B)) :=
32   localCharacter_injective ℚ_[p] (fun h => hp ((root_iff_mod_four_eq_one p).mp h))
33 
34 /-- The sign character's local behavior is determined at every actual prime. -/
35 theorem sign_locallyTrivial_iff :
36     LocallyTrivial ℚ_[p] (ofRoot (negativeRoot ℤ_[2])) ↔ p % 4 = 1 := by
37   rw [locallyTrivial_iff_mod_four]
38   exact or_iff_left dyadic_packets_distinct.symm
39 
40 /-- Modulo four is sufficient uniformly in the arithmetic prime. -/
41 theorem dyadic_trivial_iff_mod_four (χ : Packet ℤ_[2]) :
42     χ = ofRoot (oneRoot ℤ_[2]) ↔
43       mapPacket (PadicInt.toZModPow 2 : ℤ_[2] →+* ZMod 4) χ =
44         ofRoot (oneRoot (ZMod 4)) := by
45   constructor
46   · rintro rfl
47     exact mapPacket_oneRoot _
48   · intro h
49     rcases dyadic_packet_classification χ with hχ | hχ
50     · exact hχ
51     · have hn := dyadic_packets_separated_mod_four
52       rw [mapPacket_oneRoot] at hn
53       exact False.elim (hn (hχ ▸ h).symm)
54 
55 theorem dyadic_local_detection_mod_four (χ : Packet ℤ_[2]) :
56     LocallyTrivial ℚ_[p] χ ↔
57       LocallyTrivial ℚ_[p]
58         (mapPacket (PadicInt.toZModPow 2 : ℤ_[2] →+* ZMod 4) χ) := by
59   rw [locallyTrivial_iff_mod_four, locallyTrivial_iff_mod_four,
60     dyadic_trivial_iff_mod_four]
61   rfl
62 
63 theorem sign_not_locallyTrivial_three :
64     ¬ LocallyTrivial ℚ_[3] (ofRoot (negativeRoot ℤ_[2])) := by
65   rw [sign_locallyTrivial_iff]
66   decide +kernel
67 
68 theorem sign_not_locallyTrivial_two :
69     ¬ LocallyTrivial ℚ_[2] (ofRoot (negativeRoot ℤ_[2])) := by
70   rw [sign_locallyTrivial_iff]
71   decide +kernel
72 
73 /-- Residual local triviality is insufficient in dyadic coefficient characteristic. -/
74 theorem sign_residual_locallyTrivial_three :
75     LocallyTrivial ℚ_[3]
76       (mapPacket (PadicInt.toZMod : ℤ_[2] →+* ZMod 2)
77         (ofRoot (negativeRoot ℤ_[2]))) := by
78   rw [← dyadic_packets_same_residual, mapPacket_oneRoot]
79   exact oneRoot_locallyTrivial ℚ_[3]
80 
81 local instance : Fact (Nat.Prime 5) := ⟨by decide⟩
82 
83 /-- A split place does not distinguish the two distinct global characters. -/
84 theorem sign_locallyTrivial_five :
85     LocallyTrivial ℚ_[5] (ofRoot (negativeRoot ℤ_[2])) := by
86   rw [sign_locallyTrivial_iff]
87 
88 /-- Actual odd-prime inertia triviality is weaker than local triviality. -/
89 theorem sign_inertiaTrivial_three : InertiaTrivial 3 (ofRoot (negativeRoot ℤ_[2])) :=
90   inertiaTrivial_of_odd 3 (by decide) _
91 
92 variable {R : Type} [CommRing R] (I : Ideal R)
93 variable {S : Type*} (prime : S → ℕ) [∀ s, Fact (prime s).Prime]
94 
95 /-- The finite conditions are explicit arithmetic equations. Their limit satisfies
96 all selected local restrictions and every odd-prime valuation inertia condition. -/
97 theorem arithmetic_local_completion_iff [IsAdicComplete I R] [TopologicalSpace R]
98     (C : Conditions I) (finite : ∀ k, Finite (R ⧸ I ^ (k + 1))) :
99     (∃ χ : Packet R, Continuous χ.val ∧ Realizes I C χ ∧
100       (∀ s, LocallyTrivial ℚ_[prime s] χ) ∧
101       (∀ (l : ℕ) (hl : Fact l.Prime), l ≠ 2 → @InertiaTrivial l hl R _ χ)) ↔
102       ∀ k, ∃ χ, C.allowed k χ ∧
103         ∀ s, prime s % 4 = 1 ∨ χ = ofRoot (oneRoot (R ⧸ I ^ (k + 1))) := by
104   constructor
105   · rintro ⟨χ, hc, hC, hL, _⟩
106     have h := (local_completion_iff I (fun s => ℚ_[prime s]) C finite).mp
107       ⟨χ, hc, hC, hL⟩
108     intro k
109     obtain ⟨ψ, hψ, hloc⟩ := h k
110     exact ⟨ψ, hψ, fun s => (locallyTrivial_iff_mod_four (prime s) ψ).mp (hloc s)⟩
111   · intro h
112     have ho : ∀ k, ∃ χ, C.allowed k χ ∧ ∀ s, LocallyTrivial ℚ_[prime s] χ := by
113       intro k
114       obtain ⟨ψ, hψ, hloc⟩ := h k
115       exact ⟨ψ, hψ, fun s => (locallyTrivial_iff_mod_four (prime s) ψ).mpr (hloc s)⟩
116     obtain ⟨χ, hc, hC, hL⟩ :=
117       exists_local_realization I (fun s => ℚ_[prime s]) C finite ho
118     exact ⟨χ, hc, hC, hL, fun l hl hodd => @inertiaTrivial_of_odd l hl R _ hodd χ⟩
119 
120 end PaperX.QuadraticLocalArithmetic

Back to source controls