Cocycle.lean

1 import RealizationBoundaries.Sections
2 import Mathlib.Tactic.Abel
3 
4 /-! # Finite cocycles and a certified normal-form addition law -/
5 set_option autoImplicit false
6 noncomputable section
7 namespace RealizationBoundaries
8 
9 /-- The actual defect in the infinite ambient product. -/
10 def sectionDefect (S : Set Prime) (r t : ℚ) : Ambient :=
11   rationalSection S r + rationalSection S t - rationalSection S (r + t)
12 
13 /-- The support bound is about the infinite object, not a finite-array simulation. -/
14 theorem sectionDefect_support (S : Set Prime) (r t : ℚ) :
15     support (sectionDefect S r t) ⊆ exceptional (r.den * t.den) := by
16   classical
17   intro p hp
18   by_contra hn
19   have hn' : ¬ p.val ∣ r.den * t.den := hn
20   have hr : (r.den : Coordinate p) ≠ 0 :=
21     (coordinate_cast_eq_zero _ p).not.mpr (fun h => hn' (dvd_mul_of_dvd_left h _))
22   have ht : (t.den : Coordinate p) ≠ 0 :=
23     (coordinate_cast_eq_zero _ p).not.mpr (fun h => hn' (dvd_mul_of_dvd_right h _))
24   apply hp
25   change rationalSection S r p + rationalSection S t p - rationalSection S (r+t) p = 0
26   by_cases hs : p ∈ S
27   · simp only [rationalSection, hs, ite_true]
28     rw [Rat.cast_add_of_ne_zero hr ht, sub_self]
29   · simp [rationalSection, hs]
30 
31 theorem sectionDefect_finite (S : Set Prime) (r t : ℚ) :
32     sectionDefect S r t ∈ finiteSupport :=
33   (exceptional_finite (Nat.mul_pos r.den_pos t.den_pos)).subset
34     (sectionDefect_support S r t)
35 
36 /-- Only after the support theorem is proved do we package the defect as an element of D. -/
37 def cocycle (S : Set Prime) (r t : ℚ) : finiteSupport :=
38   ⟨sectionDefect S r t, sectionDefect_finite S r t⟩
39 
40 @[simp] theorem cocycle_zero (S : Set Prime) (r : ℚ) : cocycle S r 0 = 0 := by
41   apply Subtype.ext
42   simp [cocycle, sectionDefect]
43 
44 theorem cocycle_symmetric (S : Set Prime) (r t : ℚ) : cocycle S r t = cocycle S t r := by
45   apply Subtype.ext
46   simp only [cocycle, sectionDefect]
47   rw [add_comm r t, add_comm (rationalSection S r) (rationalSection S t)]
48 
49 @[simp] theorem cocycle_neg (S : Set Prime) (r : ℚ) : cocycle S r (-r) = 0 := by
50   apply Subtype.ext
51   simp [cocycle, sectionDefect]
52 
53 /-- The cocycle identity, for all rational triples and every infinite selector. -/
54 theorem cocycle_identity (S : Set Prime) (r t v : ℚ) :
55     cocycle S r t + cocycle S (r+t) v = cocycle S t v + cocycle S r (t+v) := by
56   apply Subtype.ext
57   change sectionDefect S r t + sectionDefect S (r+t) v =
58     sectionDefect S t v + sectionDefect S r (t+v)
59   simp only [sectionDefect, add_assoc]
60   abel
61 
62 /-- Pair names are kept separate from the usual split-product addition on ℚ × D. -/
63 def normalAdd (S : Set Prime) (x y : ℚ × finiteSupport) : ℚ × finiteSupport :=
64   (x.1+y.1, x.2+y.2+cocycle S x.1 y.1)
65 
66 def normalEvaluate (S : Set Prime) (x : ℚ × finiteSupport) : selectorGroup S :=
67   ⟨rationalSection S x.1 + x.2.val,
68     (selectorGroup S).add_mem (rationalSection_mem S x.1)
69       (finiteSupport_le_preimage (selectorLine S) x.2.property)⟩
70 
71 theorem normalEvaluate_add (S : Set Prime) (x y : ℚ × finiteSupport) :
72     normalEvaluate S (normalAdd S x y) = normalEvaluate S x + normalEvaluate S y := by
73   apply Subtype.ext
74   change rationalSection S (x.1+y.1) +
75       (x.2.val+y.2.val+sectionDefect S x.1 y.1) =
76     (rationalSection S x.1+x.2.val)+(rationalSection S y.1+y.2.val)
77   simp only [sectionDefect]
78   abel
79 
80 theorem normalEvaluate_bijective {S : Set Prime} (hS : S.Infinite) :
81     Function.Bijective (normalEvaluate S) := by
82   constructor
83   · intro x y h
84     obtain ⟨hr, hd⟩ := normalForm_unique hS x.1 y.1 x.2 y.2 (congrArg Subtype.val h)
85     exact Prod.ext hr hd
86   · intro x
87     obtain ⟨r, d, h⟩ := normalForm_exists S x
88     exact ⟨(r,d), Subtype.ext h.symm⟩
89 
90 /-- A bijection with the actual subgroup, accompanied by the exact addition law above. -/
91 def normalFormEquiv {S : Set Prime} (hS : S.Infinite) :
92     (ℚ × finiteSupport) ≃ selectorGroup S := Equiv.ofBijective _ (normalEvaluate_bijective hS)
93 
94 theorem normalAdd_assoc (S : Set Prime) (x y z : ℚ × finiteSupport) :
95     normalAdd S (normalAdd S x y) z = normalAdd S x (normalAdd S y z) := by
96   apply Prod.ext
97   · exact add_assoc _ _ _
98   · change (x.2+y.2+cocycle S x.1 y.1)+z.2+cocycle S (x.1+y.1) z.1 =
99       x.2+(y.2+z.2+cocycle S y.1 z.1)+cocycle S x.1 (y.1+z.1)
100     have h := cocycle_identity S x.1 y.1 z.1
101     calc
102       _ = x.2+y.2+z.2+(cocycle S x.1 y.1+cocycle S (x.1+y.1) z.1) := by abel
103       _ = x.2+y.2+z.2+(cocycle S y.1 z.1+cocycle S x.1 (y.1+z.1)) := by rw [h]
104       _ = _ := by abel
105 
106 theorem normalAdd_comm (S : Set Prime) (x y : ℚ × finiteSupport) :
107     normalAdd S x y = normalAdd S y x := by
108   apply Prod.ext
109   · exact add_comm _ _
110   · change x.2+y.2+cocycle S x.1 y.1 = y.2+x.2+cocycle S y.1 x.1
111     rw [cocycle_symmetric S x.1 y.1, add_comm x.2 y.2]
112 
113 theorem normalAdd_zero (S : Set Prime) (x : ℚ × finiteSupport) :
114     normalAdd S x (0,0) = x := by
115   simp [normalAdd]
116 
117 theorem normalAdd_inverse (S : Set Prime) (x : ℚ × finiteSupport) :
118     normalAdd S x (-x.1,-x.2) = (0,0) := by
119   simp [normalAdd]
120 
121 /-- The finite correction cannot be removed by any function into D on a nonzero rational line. -/
122 theorem cocycle_not_removable {S : Set Prime} (hS : S.Infinite) :
123     ¬ ∃ b : ℚ → finiteSupport,
124       ∀ r t : ℚ, cocycle S r t + b r + b t - b (r+t) = 0 := by
125   rintro ⟨b, hb⟩
126   let f : ℚ →+ Ambient := AddMonoidHom.mk'
127     (fun r => rationalSection S r + (b r).val) (by
128       intro r t
129       have h := congrArg Subtype.val (hb r t)
130       change sectionDefect S r t + (b r).val + (b t).val - (b (r+t)).val = 0 at h
131       change rationalSection S (r+t)+(b (r+t)).val =
132         (rationalSection S r+(b r).val)+(rationalSection S t+(b t).val)
133       symm
134       apply sub_eq_zero.mp
135       calc
136         _ = sectionDefect S r t + (b r).val + (b t).val - (b (r+t)).val := by
137           simp only [sectionDefect]
138           abel
139         _ = 0 := h)
140   have hf : f = 0 := rational_hom_zero ℚ f
141   have hzero : quotientMap (f 1) = 0 := by simp [hf]
142   have hq : quotientMap (f 1) = quotientMap (indicator S) := by
143     change quotientMap (rationalSection S 1 + (b 1).val) = _
144     simp [(quotientMap_eq_zero_iff _).mpr (b 1).property]
145   exact indicator_tail_ne_zero hS (hq.symm.trans hzero)
146 
147 end RealizationBoundaries

Back to source controls