QuadraticArithmeticCompletion.lean

1 import PaperX.QuadraticGaloisPackets
2 import PaperX.QuadraticRootCompletion
3 
4 /-! Completion of actual quadratic Galois packets.  The finite objects are
5 characters of the absolute Galois group, with a fixed arithmetic kernel.
6 The coordinate interpretation, compatibility, and continuity are proved. -/
7 set_option autoImplicit false
8 noncomputable section
9 namespace PaperX.QuadraticArithmeticCompletion
10 
11 open PaperX.QuadraticAlgebra PaperX.QuadraticGalois PaperX.QuadraticGaloisPackets
12 variable {R : Type} [CommRing R] (I : Ideal R)
13 
14 @[ext] structure Family where
15   values : (n : ℕ) → Packet (R ⧸ I ^ n)
16   compatible : ∀ {m n : ℕ} (h : m ≤ n),
17     mapPacket (Ideal.Quotient.factorPow I h) (values n) = values m
18 
19 def reduce (χ : Packet R) : Family I where
20   values n := mapPacket (Ideal.Quotient.mk (I ^ n)) χ
21   compatible := by
22     intro m n h
23     apply Subtype.ext
24     ext σ
25     change Ideal.Quotient.factorPow I h (Ideal.Quotient.mk (I ^ n) (χ.val σ)) =
26       Ideal.Quotient.mk (I ^ m) (χ.val σ)
27     simp
28 
29 def rootFamily (x : Family I) : QuadraticRootCompletion.Family I where
30   values n := rootOf (x.values n)
31   compatible := by
32     intro m n h
33     rw [← rootOf_natural, x.compatible h]
34 
35 def reconstruct [IsAdicComplete I R] (x : Family I) : Packet R :=
36   ofRoot (QuadraticRootCompletion.reconstruct I (rootFamily I x))
37 
38 theorem reconstruct_reduces [IsAdicComplete I R] (x : Family I) (n : ℕ) :
39     mapPacket (Ideal.Quotient.mk (I ^ n)) (reconstruct I x) = x.values n := by
40   rw [reconstruct, ofRoot_natural, QuadraticRootCompletion.reconstruct_reduces]
41   exact ofRoot_rootOf (x.values n)
42 
43 theorem packet_ext [IsHausdorff I R] {χ ψ : Packet R}
44     (h : ∀ n, mapPacket (Ideal.Quotient.mk (I ^ n)) χ =
45       mapPacket (Ideal.Quotient.mk (I ^ n)) ψ) : χ = ψ := by
46   have H : rootOf χ = rootOf ψ := by
47     apply QuadraticRootCompletion.root_ext I
48     intro n
49     simpa only [rootOf_natural] using congrArg rootOf (h n)
50   simpa only [ofRoot_rootOf] using congrArg ofRoot H
51 
52 theorem reconstruct_unique [IsAdicComplete I R] (x : Family I) (χ : Packet R)
53     (h : ∀ n, mapPacket (Ideal.Quotient.mk (I ^ n)) χ = x.values n) :
54     χ = reconstruct I x := by
55   apply packet_ext I
56   intro n
57   rw [h n, reconstruct_reduces]
58 
59 theorem reconstruct_reduce [IsAdicComplete I R] (χ : Packet R) :
60     reconstruct I (reduce I χ) = χ :=
61   (reconstruct_unique I (reduce I χ) χ (fun _ => rfl)).symm
62 
63 theorem reduce_reconstruct [IsAdicComplete I R] (x : Family I) :
64     reduce I (reconstruct I x) = x := by
65   apply Family.ext
66   funext n
67   exact reconstruct_reduces I x n
68 
69 /-- The inverse-limit equivalence is about actual arithmetic characters. -/
70 def reconstructionEquiv [IsAdicComplete I R] : Packet R ≃ Family I where
71   toFun := reduce I
72   invFun := reconstruct I
73   left_inv := reconstruct_reduce I
74   right_inv := reduce_reconstruct I
75 
76 /-- The coefficient-preserving coordinate-ring interpretation is retained. -/
77 def pointReconstructionEquiv [IsAdicComplete I R] :
78     (CoordinateRing R →ₐ[R] R) ≃ Family I :=
79   (pointPacketEquiv R).trans (reconstructionEquiv I)
80 
81 theorem reconstructed_continuous [IsAdicComplete I R] [TopologicalSpace R]
82     (x : Family I) : Continuous (reconstruct I x).val :=
83   packet_continuous (reconstruct I x)
84 
85 /-- Allowed objects at precision k+1 are actual Galois characters. -/
86 structure Conditions where
87   allowed : (k : ℕ) → Packet (R ⧸ I ^ (k + 1)) → Prop
88   downward : ∀ {j k : ℕ} (h : j ≤ k) χ, allowed k χ →
89     allowed j (mapPacket (Ideal.Quotient.factorPow I (Nat.add_le_add_right h 1)) χ)
90 
91 def rootConditions (C : Conditions I) : QuadraticRootCompletion.Conditions I where
92   allowed k x := C.allowed k (ofRoot x)
93   downward := by
94     intro j k h x hx
95     have H := C.downward h (ofRoot x) hx
96     rwa [ofRoot_natural] at H
97 
98 def Realizes (C : Conditions I) (χ : Packet R) : Prop :=
99   ∀ k, C.allowed k (mapPacket (Ideal.Quotient.mk (I ^ (k + 1))) χ)
100 
101 /-- No coherent choices of finite characters and no surjective transitions are assumed. -/
102 theorem exists_realization [IsAdicComplete I R] [TopologicalSpace R]
103     (C : Conditions I) (finite : ∀ k, Finite (R ⧸ I ^ (k + 1)))
104     (occupied : ∀ k, ∃ χ, C.allowed k χ) :
105     ∃ χ : Packet R, Continuous χ.val ∧ Realizes I C χ := by
106   have ho : ∀ k, ∃ x, (rootConditions I C).allowed k x := by
107     intro k
108     obtain ⟨χ, hχ⟩ := occupied k
109     refine ⟨rootOf χ, ?_⟩
110     change C.allowed k (ofRoot (rootOf χ))
111     rwa [ofRoot_rootOf]
112   obtain ⟨x, hx⟩ := (QuadraticRootCompletion.realization_iff_of_finite_quotients I
113     (rootConditions I C) finite).mpr ho
114   refine ⟨ofRoot x, packet_continuous _, ?_⟩
115   intro k
116   have h := hx k
117   change C.allowed k (ofRoot (mapRoot (Ideal.Quotient.mk (I ^ (k + 1))) x)) at h
118   rwa [← ofRoot_natural] at h
119 
120 theorem arithmetic_completion_iff [IsAdicComplete I R] [TopologicalSpace R]
121     (C : Conditions I) (finite : ∀ k, Finite (R ⧸ I ^ (k + 1))) :
122     (∃ χ : Packet R, Continuous χ.val ∧ Realizes I C χ) ↔
123       ∀ k, ∃ χ, C.allowed k χ := by
124   constructor
125   · rintro ⟨χ, _, hχ⟩ k
126     exact ⟨mapPacket (Ideal.Quotient.mk (I ^ (k + 1))) χ, hχ k⟩
127   · exact exists_realization I C finite
128 
129 /-- In the actual dyadic coefficient ring the arithmetic completion is one of two packets. -/
130 theorem dyadic_completion (C : Conditions (R := ℤ_[2]) (IsLocalRing.maximalIdeal ℤ_[2]))
131     (occupied : ∀ k, ∃ χ, C.allowed k χ) :
132     ∃ χ : Packet ℤ_[2], Continuous χ.val ∧
133       Realizes (IsLocalRing.maximalIdeal ℤ_[2]) C χ ∧
134       (χ = ofRoot (oneRoot ℤ_[2]) ∨ χ = ofRoot (negativeRoot ℤ_[2])) := by
135   let I := IsLocalRing.maximalIdeal ℤ_[2]
136   have hfinite : ∀ k, Finite (ℤ_[2] ⧸ I ^ (k + 1)) := by
137     intro k
138     let : Finite (ℤ_[2] ⧸ I) :=
139       Finite.of_equiv (ZMod 2) (PadicInt.residueField (p := 2)).symm.toEquiv
140     exact Ideal.finite_quotient_pow (IsNoetherian.noetherian I) (k + 1)
141   obtain ⟨χ, hc, hχ⟩ := exists_realization I C hfinite occupied
142   exact ⟨χ, hc, hχ, dyadic_packet_classification χ⟩
143 
144 end PaperX.QuadraticArithmeticCompletion

Back to source controls