QuadraticLocalPackets.lean

1 import PaperX.QuadraticLocalGalois
2 import PaperX.QuadraticGaloisPackets
3 
4 /-! Actual restriction of the fixed global arithmetic packet.  A local condition
5 is triviality after the field-induced absolute-Galois-group map.  Its arithmetic
6 description is proved, and is valid over arbitrary commutative coefficient rings. -/
7 set_option autoImplicit false
8 noncomputable section
9 namespace PaperX.QuadraticLocalPackets
10 
11 open PaperX.QuadraticGalois PaperX.QuadraticGaloisPackets
12 open PaperX.QuadraticLocalGalois
13 
14 variable (K : Type*) [Field K] [CharZero K]
15 variable {B C : Type*} [CommRing B] [CommRing C]
16 
17 def localCharacter (χ : Packet B) : Field.absoluteGaloisGroup K →* Bˣ :=
18   χ.val.comp (restriction K).toMonoidHom
19 
20 def LocallyTrivial (χ : Packet B) : Prop := localCharacter K χ = 1
21 
22 theorem localCharacter_descent (χ : Packet B) :
23     localCharacter K χ = (descentEquiv χ).comp (localQuotient K) := by
24   rw [localCharacter, ← descent_comp χ]
25   rfl
26 
27 theorem localCharacter_continuous [TopologicalSpace B] (χ : Packet B) :
28     Continuous (localCharacter K χ) :=
29   (packet_continuous χ).comp (restriction K).continuous
30 
31 theorem localCharacter_natural (f : B →+* C) (χ : Packet B) :
32     localCharacter K (mapPacket f χ) =
33       (Units.map f.toMonoidHom).comp (localCharacter K χ) := rfl
34 
35 theorem locallyTrivial_map (f : B →+* C) (χ : Packet B)
36     (h : LocallyTrivial K χ) : LocallyTrivial K (mapPacket f χ) := by
37   change localCharacter K (mapPacket f χ) = 1
38   rw [localCharacter_natural, show localCharacter K χ = 1 from h]
39   ext σ
40   exact map_one _
41 
42 theorem mapPacket_oneRoot (f : B →+* C) :
43     mapPacket f (ofRoot (oneRoot B)) = ofRoot (oneRoot C) := by
44   rw [ofRoot_natural]
45   apply congrArg ofRoot
46   apply Subtype.ext
47   exact map_one f
48 
49 theorem oneRoot_locallyTrivial : LocallyTrivial K (ofRoot (oneRoot B)) := by
50   change (ofRoot (oneRoot B)).val.comp (restriction K).toMonoidHom = 1
51   rw [oneRoot_character]
52   rfl
53 
54 theorem locallyTrivial_of_square (h : ∃ x : K, x ^ 2 = -1) (χ : Packet B) :
55     LocallyTrivial K χ := by
56   change localCharacter K χ = 1
57   rw [localCharacter_descent, (localQuotient_trivial_iff K).mpr h]
58   apply MonoidHom.ext
59   intro σ
60   exact map_one (descentEquiv χ)
61 
62 /-- A nonsplit field sees the entire fixed global quadratic packet. -/
63 theorem localCharacter_injective (h : ¬ ∃ x : K, x ^ 2 = -1) :
64     Function.Injective (localCharacter K (B := B)) := by
65   intro χ ψ heq
66   apply descentEquiv.injective
67   apply MonoidHom.ext
68   intro c
69   obtain ⟨σ, rfl⟩ := localQuotient_surjective K h c
70   have H := congrArg (fun f : Field.absoluteGaloisGroup K →* Bˣ => f σ) heq
71   simpa only [localCharacter_descent, MonoidHom.comp_apply] using H
72 
73 /-- The local condition is an actual arithmetic disjunction, with no reducedness,
74 domain, or characteristic restriction on the coefficient ring. -/
75 theorem locallyTrivial_iff (χ : Packet B) :
76     LocallyTrivial K χ ↔ (∃ x : K, x ^ 2 = -1) ∨ χ = ofRoot (oneRoot B) := by
77   constructor
78   · intro hχ
79     by_cases hK : ∃ x : K, x ^ 2 = -1
80     · exact Or.inl hK
81     · right
82       apply localCharacter_injective K hK
83       exact hχ.trans (oneRoot_locallyTrivial K).symm
84   · rintro (hK | rfl)
85     · exact locallyTrivial_of_square K hK χ
86     · exact oneRoot_locallyTrivial K
87 
88 theorem locallyTrivial_iff_oneRoot (h : ¬ ∃ x : K, x ^ 2 = -1) (χ : Packet B) :
89     LocallyTrivial K χ ↔ χ = ofRoot (oneRoot B) := by
90   rw [locallyTrivial_iff]
91   exact or_iff_right h
92 
93 end PaperX.QuadraticLocalPackets

Back to source controls