NormalForms.lean

1 import RealizationBoundaries.Cocycle
2 
3 /-! # A distinct normal-form group, not the split direct-product group -/
4 set_option autoImplicit false
5 noncomputable section
6 namespace RealizationBoundaries
7 
8 /-- A separate type prevents accidental use of the split addition on ℚ × D. -/
9 structure NormalForm (S : Set Prime) where
10   rational : ℚ
11   finite : finiteSupport
12 
13 namespace NormalForm
14 
15 def toPair {S : Set Prime} (x : NormalForm S) : ℚ × finiteSupport :=
16   (x.rational, x.finite)
17 
18 def pairEquiv (S : Set Prime) : NormalForm S ≃ (ℚ × finiteSupport) where
19   toFun := toPair
20   invFun x := ⟨x.1, x.2⟩
21   left_inv _ := rfl
22   right_inv _ := rfl
23 
24 instance (S : Set Prime) : Zero (NormalForm S) := ⟨⟨0,0⟩⟩
25 instance (S : Set Prime) : Add (NormalForm S) :=
26   ⟨fun x y => ⟨x.rational+y.rational, x.finite+y.finite+cocycle S x.rational y.rational⟩⟩
27 instance (S : Set Prime) : Neg (NormalForm S) := ⟨fun x => ⟨-x.rational,-x.finite⟩⟩
28 
29 instance (S : Set Prime) : AddCommGroup (NormalForm S) where
30   nsmul := nsmulRec
31   zsmul := zsmulRec
32   add_assoc x y z := (pairEquiv S).injective (normalAdd_assoc S x.toPair y.toPair z.toPair)
33   add_zero x := (pairEquiv S).injective (normalAdd_zero S x.toPair)
34   zero_add x := (pairEquiv S).injective
35     ((normalAdd_comm S (0,0) x.toPair).trans (normalAdd_zero S x.toPair))
36   neg_add_cancel x := (pairEquiv S).injective
37     ((normalAdd_comm S (-x.rational,-x.finite) x.toPair).trans (normalAdd_inverse S x.toPair))
38   add_comm x y := (pairEquiv S).injective (normalAdd_comm S x.toPair y.toPair)
39 
40 @[simp] theorem toPair_add {S : Set Prime} (x y : NormalForm S) :
41     (x+y).toPair = normalAdd S x.toPair y.toPair := rfl
42 
43 @[simp] theorem rational_add {S : Set Prime} (x y : NormalForm S) :
44     (x+y).rational = x.rational+y.rational := rfl
45 
46 @[simp] theorem finite_add {S : Set Prime} (x y : NormalForm S) :
47     (x+y).finite = x.finite+y.finite+cocycle S x.rational y.rational := rfl
48 
49 /-- The exact group isomorphism from cocycle coordinates to the actual ambient preimage. -/
50 def realizationEquiv {S : Set Prime} (hS : S.Infinite) : NormalForm S ≃+ selectorGroup S where
51   toEquiv := (pairEquiv S).trans (normalFormEquiv hS)
52   map_add' x y := normalEvaluate_add S x.toPair y.toPair
53 
54 @[simp] theorem realizationEquiv_coe {S : Set Prime} (hS : S.Infinite) (x : NormalForm S) :
55     (realizationEquiv hS x).val = rationalSection S x.rational+x.finite.val := rfl
56 
57 end NormalForm
58 end RealizationBoundaries

Back to source controls