QuadraticLocalGalois.lean

1 import PaperX.QuadraticGalois
2 import PaperX.GaloisComparisonCompletion
3 
4 /-! The fixed quadratic global quotient restricted to actual absolute Galois
5 groups of characteristic-zero coefficient fields. The field restriction is
6 Mathlib's actual map, including its chosen algebraic-closure embedding. -/
7 set_option autoImplicit false
8 noncomputable section
9 namespace PaperX.QuadraticLocalGalois
10 open PaperX.ArithmeticCertificateExample PaperX.QuadraticGalois
11 open PaperX.CompletionExamples
12 
13 variable (K : Type*) [Field K] [CharZero K]
14 
15 def restriction : Field.absoluteGaloisGroup K →ₜ* Field.absoluteGaloisGroup ℚ :=
16   Field.absoluteGaloisGroup.map (algebraMap ℚ K)
17 
18 def closureEmbedding : Qbar →ₐ[ℚ] AlgebraicClosure K := IsAlgClosed.lift
19 
20 def localRoot : AlgebraicClosure K := closureEmbedding K imaginary
21 
22 def localQuotient : Field.absoluteGaloisGroup K →* C2 :=
23   quotientMap.comp (restriction K).toMonoidHom
24 
25 theorem localRoot_sq : localRoot K ^ 2 = -1 := by
26   rw [localRoot, ← map_pow, imaginary_sq, map_neg, map_one]
27 
28 theorem restriction_commutes (σ : Field.absoluteGaloisGroup K) (x : Qbar) :
29     closureEmbedding K ((show GQ from restriction K σ) x) =
30       (show AlgebraicClosure K ≃ₐ[K] AlgebraicClosure K from σ) (closureEmbedding K x) := by
31   let g : Qbar →ₐ[ℚ] AlgebraicClosure K := IsAlgClosed.lift
32   let : Algebra Qbar (AlgebraicClosure K) := g.toAlgebra
33   exact AlgEquiv.restrictNormal_commutes
34     ((show AlgebraicClosure K ≃ₐ[K] AlgebraicClosure K from σ).restrictScalars ℚ)
35     Qbar x
36 
37 theorem localQuotient_eq_one_iff (σ : Field.absoluteGaloisGroup K) :
38     localQuotient K σ = 1 ↔
39       (show AlgebraicClosure K ≃ₐ[K] AlgebraicClosure K from σ) (localRoot K) = localRoot K := by
40   change quotientMap (restriction K σ) = 1 ↔ _
41   rw [quotientMap_eq_one_iff]
42   constructor
43   · intro h
44     exact (restriction_commutes K σ imaginary).symm.trans (congrArg (closureEmbedding K) h)
45   · intro h
46     apply (closureEmbedding K).injective
47     exact (restriction_commutes K σ imaginary).trans h
48 
49 /-- The chosen image is rational over the local field exactly when minus one is a square. -/
50 theorem localRoot_mem_range_iff :
51     localRoot K ∈ Set.range (algebraMap K (AlgebraicClosure K)) ↔
52       ∃ x : K, x ^ 2 = -1 := by
53   constructor
54   · rintro ⟨x, hx⟩
55     refine ⟨x, (algebraMap K (AlgebraicClosure K)).injective ?_⟩
56     rw [map_pow, hx, localRoot_sq, map_neg, map_one]
57   · rintro ⟨x, hx⟩
58     have hs : localRoot K ^ 2 = (algebraMap K (AlgebraicClosure K) x) ^ 2 := by
59       rw [localRoot_sq, ← map_pow, hx, map_neg, map_one]
60     rcases sq_eq_sq_iff_eq_or_eq_neg.mp hs with h | h
61     · exact ⟨x, h.symm⟩
62     · exact ⟨-x, by rw [map_neg]; exact h.symm⟩
63 
64 /-- A theorem about the actual field-induced Galois restriction map. -/
65 theorem localQuotient_trivial_iff :
66     localQuotient K = 1 ↔ ∃ x : K, x ^ 2 = -1 := by
67   rw [← localRoot_mem_range_iff K,
68     InfiniteGalois.mem_range_algebraMap_iff_fixed (localRoot K)]
69   constructor
70   · intro h σ
71     exact (localQuotient_eq_one_iff K σ).mp
72       (congrArg (fun f : Field.absoluteGaloisGroup K →* C2 => f σ) h)
73   · intro h
74     apply MonoidHom.ext
75     intro σ
76     exact (localQuotient_eq_one_iff K σ).mpr (h σ)
77 
78 theorem localQuotient_hits_generator
79     (h : ¬ ∃ x : K, x ^ 2 = -1) :
80     ∃ σ : Field.absoluteGaloisGroup K, localQuotient K σ = generator := by
81   by_contra hn
82   apply h
83   apply (localQuotient_trivial_iff K).mp
84   apply MonoidHom.ext
85   intro σ
86   have hc : ∀ c : C2, c = 1 ∨ c = generator := by decide +kernel
87   rcases hc (localQuotient K σ) with hσ | hσ
88   · exact hσ
89   · exact False.elim (hn ⟨σ, hσ⟩)
90 
91 theorem localQuotient_surjective
92     (h : ¬ ∃ x : K, x ^ 2 = -1) : Function.Surjective (localQuotient K) := by
93   intro c
94   have hc : ∀ c : C2, c = 1 ∨ c = generator := by decide +kernel
95   rcases hc c with rfl | rfl
96   · exact ⟨1, map_one _⟩
97   · exact localQuotient_hits_generator K h
98 
99 theorem localQuotient_continuous : Continuous (localQuotient K) :=
100   absoluteQuadraticCharacter_continuous.comp (restriction K).continuous
101 
102 /-- Fixing one square root is equivalent to fixing any other choice. -/
103 theorem localQuotient_eq_one_iff_fixed_root (y : AlgebraicClosure K)
104     (hy : y ^ 2 = -1) (σ : Field.absoluteGaloisGroup K) :
105     localQuotient K σ = 1 ↔
106       (show AlgebraicClosure K ≃ₐ[K] AlgebraicClosure K from σ) y = y := by
107   have hs : y ^ 2 = localRoot K ^ 2 := by rw [hy, localRoot_sq]
108   rcases sq_eq_sq_iff_eq_or_eq_neg.mp hs with h | h
109   · rw [h]
110     exact localQuotient_eq_one_iff K σ
111   · rw [h]
112     have hn : (show AlgebraicClosure K ≃ₐ[K] AlgebraicClosure K from σ)
113         (-localRoot K) =
114         -(show AlgebraicClosure K ≃ₐ[K] AlgebraicClosure K from σ) (localRoot K) :=
115       map_neg (show AlgebraicClosure K ≃ₐ[K] AlgebraicClosure K from σ) _
116     rw [hn, neg_inj]
117     exact localQuotient_eq_one_iff K σ
118 
119 theorem restriction_padic (p : ℕ) [Fact p.Prime] :
120     restriction ℚ_[p] = GaloisComparisonCompletion.localRestriction p := rfl
121 
122 end PaperX.QuadraticLocalGalois

Back to source controls