QuadraticGalois.lean

1 import PaperX.ArithmeticCertificateExample
2 import Mathlib.Topology.Algebra.Group.Units
3 
4 /-! The actual quadratic Galois quotient and characters trivial on its kernel.
5 The kernel is defined by its action on a square root of minus one.
6 No claim about arithmetic inertia or period invariants is made here. -/
7 set_option autoImplicit false
8 noncomputable section
9 
10 namespace PaperX.QuadraticGalois
11 
12 open PaperX.CompletionExamples PaperX.ArithmeticCertificateExample
13 
14 abbrev quotientMap : Field.absoluteGaloisGroup ℚ →* C2 := absoluteQuadraticCharacter
15 
16 theorem quotientMap_surjective : Function.Surjective quotientMap := by
17   intro g
18   have hc : ∀ a : C2, a = 1 ∨ a = generator := by decide +kernel
19   rcases hc g with rfl | rfl
20   · exact ⟨1, map_one quotientMap⟩
21   · exact quadraticCharacter_hits_generator
22 
23 theorem quotientMap_eq_one_iff (σ : Field.absoluteGaloisGroup ℚ) :
24     quotientMap σ = 1 ↔ (show GQ from σ) imaginary = imaginary := by
25   have hg : generator ≠ (1 : C2) := by decide +kernel
26   change quadraticValue (show GQ from σ) = 1 ↔ (show GQ from σ) imaginary = imaginary
27   by_cases h : (show GQ from σ) imaginary = imaginary
28   · simp [quadraticValue, h]
29   · simp [quadraticValue, h, hg]
30 
31 /-- These are actual Galois characters trivial on the specified arithmetic kernel. -/
32 def Packet (B : Type*) [CommRing B] :=
33   {χ : Field.absoluteGaloisGroup ℚ →* Bˣ // quotientMap.ker ≤ χ.ker}
34 
35 variable {B C : Type*} [CommRing B] [CommRing C]
36 
37 /-- Descent is derived from the actual surjective quotient, not supplied as an input. -/
38 def descentEquiv : Packet B ≃ (C2 →* Bˣ) :=
39   quotientMap.liftOfSurjective quotientMap_surjective
40 
41 @[simp] theorem descent_comp (χ : Packet B) :
42     (descentEquiv χ).comp quotientMap = χ.val :=
43   congrArg Subtype.val (descentEquiv.left_inv χ)
44 
45 @[simp] theorem descent_symm_val (ψ : C2 →* Bˣ) :
46     (descentEquiv.symm ψ).val = ψ.comp quotientMap := rfl
47 
48 theorem packet_continuous [TopologicalSpace B] (χ : Packet B) : Continuous χ.val := by
49   rw [← descent_comp χ]
50   exact (continuous_of_discreteTopology (f := descentEquiv χ)).comp
51     absoluteQuadraticCharacter_continuous
52 
53 theorem packet_finite_image (χ : Packet B) : Set.Finite (Set.range χ.val) := by
54   apply (Set.finite_range (descentEquiv χ)).subset
55   rintro _ ⟨σ, rfl⟩
56   exact ⟨quotientMap σ, congrArg (fun ψ : Field.absoluteGaloisGroup ℚ →* Bˣ => ψ σ)
57     (descent_comp χ)⟩
58 
59 def mapPacket (f : B →+* C) (χ : Packet B) : Packet C :=
60   ⟨(Units.map f.toMonoidHom).comp χ.val, by
61     intro σ hσ
62     change Units.map f.toMonoidHom (χ.val σ) = 1
63     rw [show χ.val σ = 1 from χ.property hσ, map_one]⟩
64 
65 @[simp] theorem mapPacket_apply (f : B →+* C) (χ : Packet B)
66     (σ : Field.absoluteGaloisGroup ℚ) :
67     ↑((mapPacket f χ).val σ) = f (χ.val σ) := rfl
68 
69 theorem mapPacket_id (χ : Packet B) : mapPacket (RingHom.id B) χ = χ := by
70   apply Subtype.ext
71   ext σ
72   rfl
73 
74 theorem mapPacket_comp {D : Type*} [CommRing D]
75     (f : B →+* C) (g : C →+* D) (χ : Packet B) :
76     mapPacket g (mapPacket f χ) = mapPacket (g.comp f) χ := by
77   apply Subtype.ext
78   ext σ
79   rfl
80 
81 theorem descent_map (f : B →+* C) (χ : Packet B) :
82     descentEquiv (mapPacket f χ) = (Units.map f.toMonoidHom).comp (descentEquiv χ) := by
83   apply MonoidHom.ext
84   intro g
85   obtain ⟨σ, rfl⟩ := quotientMap_surjective g
86   have h₁ := congrArg (fun ψ : Field.absoluteGaloisGroup ℚ →* Cˣ => ψ σ)
87     (descent_comp (mapPacket f χ))
88   have h₂ := congrArg (fun ψ : Field.absoluteGaloisGroup ℚ →* Bˣ => ψ σ)
89     (descent_comp χ)
90   change descentEquiv (mapPacket f χ) (quotientMap σ) =
91     Units.map f.toMonoidHom (descentEquiv χ (quotientMap σ))
92   rw [show descentEquiv (mapPacket f χ) (quotientMap σ) = (mapPacket f χ).val σ from h₁,
93     show descentEquiv χ (quotientMap σ) = χ.val σ from h₂]
94   rfl
95 
96 end PaperX.QuadraticGalois

Back to source controls