QuadraticLocalCompletion.lean

1 import PaperX.QuadraticLocalPackets
2 import PaperX.QuadraticArithmeticCompletion
3 
4 /-! Arithmetic local triviality is closed under completion for the fixed global
5 quadratic packet.  The local conditions are actual field-induced restrictions,
6 and their closure is proved rather than assumed. -/
7 set_option autoImplicit false
8 noncomputable section
9 namespace PaperX.QuadraticLocalCompletion
10 
11 open PaperX.QuadraticGalois PaperX.QuadraticGaloisPackets
12 open PaperX.QuadraticLocalPackets
13 open PaperX.QuadraticArithmeticCompletion
14 
15 variable {R : Type} [CommRing R] (I : Ideal R)
16 variable (K : Type*) [Field K] [CharZero K]
17 
18 theorem locallyTrivial_iff_reductions [IsHausdorff I R] (χ : Packet R) :
19     LocallyTrivial K χ ↔
20       ∀ n, LocallyTrivial K (mapPacket (Ideal.Quotient.mk (I ^ n)) χ) := by
21   constructor
22   · intro h n
23     exact locallyTrivial_map K _ χ h
24   · intro h
25     by_cases hK : ∃ x : K, x ^ 2 = -1
26     · exact locallyTrivial_of_square K hK χ
27     · apply (locallyTrivial_iff_oneRoot K hK χ).mpr
28       apply packet_ext I
29       intro n
30       rw [mapPacket_oneRoot]
31       exact (locallyTrivial_iff_oneRoot K hK _).mp (h n)
32 
33 /-- Positive precisions suffice, matching the finite admissible levels. -/
34 theorem locallyTrivial_iff_positive_reductions [IsHausdorff I R] (χ : Packet R) :
35     LocallyTrivial K χ ↔
36       ∀ k, LocallyTrivial K (mapPacket (Ideal.Quotient.mk (I ^ (k + 1))) χ) := by
37   constructor
38   · intro h k
39     exact locallyTrivial_map K _ χ h
40   · intro h
41     apply (locallyTrivial_iff_reductions I K χ).mpr
42     intro n
43     have H := locallyTrivial_map K (Ideal.Quotient.factorPow I (Nat.le_succ n))
44       (mapPacket (Ideal.Quotient.mk (I ^ (n + 1))) χ) (h n)
45     have heq :
46         mapPacket (Ideal.Quotient.factorPow I (Nat.le_succ n))
47           (mapPacket (Ideal.Quotient.mk (I ^ (n + 1))) χ) =
48           mapPacket (Ideal.Quotient.mk (I ^ n)) χ := by
49       apply Subtype.ext
50       ext σ
51       change Ideal.Quotient.factorPow I (Nat.le_succ n)
52           (Ideal.Quotient.mk (I ^ (n + 1)) (χ.val σ)) =
53         Ideal.Quotient.mk (I ^ n) (χ.val σ)
54       simp
55     rwa [heq] at H
56 
57 theorem reconstructed_locallyTrivial [IsAdicComplete I R] (x : Family I)
58     (h : ∀ n, LocallyTrivial K (x.values n)) :
59     LocallyTrivial K (reconstruct I x) := by
60   apply (locallyTrivial_iff_reductions I K _).mpr
61   intro n
62   rw [reconstruct_reduces]
63   exact h n
64 
65 variable {S : Type*} (F : S → Type*) [∀ s, Field (F s)] [∀ s, CharZero (F s)]
66 
67 /-- All specified local fields are imposed simultaneously.  The index set itself
68 need not be finite: it defines a subset of each finite coefficient level. -/
69 def withLocalTriviality (C : Conditions I) : Conditions I where
70   allowed k χ := C.allowed k χ ∧ ∀ s, LocallyTrivial (F s) χ
71   downward := by
72     intro j k hjk χ hχ
73     refine ⟨C.downward hjk χ hχ.1, ?_⟩
74     intro s
75     exact locallyTrivial_map (F s) _ χ (hχ.2 s)
76 
77 theorem realizes_withLocalTriviality_iff [IsHausdorff I R]
78     (C : Conditions I) (χ : Packet R) :
79     Realizes I (withLocalTriviality I F C) χ ↔
80       Realizes I C χ ∧ ∀ s, LocallyTrivial (F s) χ := by
81   constructor
82   · intro h
83     refine ⟨fun k => (h k).1, ?_⟩
84     intro s
85     exact (locallyTrivial_iff_positive_reductions I (F s) χ).mpr
86       (fun k => (h k).2 s)
87   · rintro ⟨hC, hL⟩ k
88     exact ⟨hC k, fun s => locallyTrivial_map (F s) _ χ (hL s)⟩
89 
90 /-- Nonempty admissible finite levels produce an actual global character satisfying
91 every specified field restriction, without preselected coherent characters. -/
92 theorem exists_local_realization [IsAdicComplete I R] [TopologicalSpace R]
93     (C : Conditions I) (finite : ∀ k, Finite (R ⧸ I ^ (k + 1)))
94     (occupied : ∀ k, ∃ χ, C.allowed k χ ∧ ∀ s, LocallyTrivial (F s) χ) :
95     ∃ χ : Packet R, Continuous χ.val ∧ Realizes I C χ ∧
96       ∀ s, LocallyTrivial (F s) χ := by
97   obtain ⟨χ, hc, hχ⟩ := exists_realization I (withLocalTriviality I F C) finite occupied
98   exact ⟨χ, hc, (realizes_withLocalTriviality_iff I F C χ).mp hχ⟩
99 
100 theorem local_completion_iff [IsAdicComplete I R] [TopologicalSpace R]
101     (C : Conditions I) (finite : ∀ k, Finite (R ⧸ I ^ (k + 1))) :
102     (∃ χ : Packet R, Continuous χ.val ∧ Realizes I C χ ∧
103       ∀ s, LocallyTrivial (F s) χ) ↔
104       ∀ k, ∃ χ, C.allowed k χ ∧ ∀ s, LocallyTrivial (F s) χ := by
105   constructor
106   · rintro ⟨χ, _, hC, hL⟩ k
107     exact ⟨mapPacket (Ideal.Quotient.mk (I ^ (k + 1))) χ, hC k,
108       fun s => locallyTrivial_map (F s) _ χ (hL s)⟩
109   · exact exists_local_realization I F C finite
110 
111 /-- One nonsplit field forces the completed member to be globally trivial. -/
112 theorem completion_forced_trivial (s : S) (hs : ¬ ∃ x : F s, x ^ 2 = -1)
113     (χ : Packet R) (hχ : ∀ t, LocallyTrivial (F t) χ) :
114     χ = ofRoot (oneRoot R) :=
115   (locallyTrivial_iff_oneRoot (F s) hs χ).mp (hχ s)
116 
117 end PaperX.QuadraticLocalCompletion

Back to source controls