DyadicAffine.lean

1 import Mathlib.Algebra.Module.ZMod
2 import Mathlib.Tactic
3 
4 /-! Paper XI, Proposition 13.2: the affine space of refinements of a fixed
5 bilinear form over the field with two elements. No nondegeneracy is required. -/
6 set_option autoImplicit false
7 noncomputable section
8 namespace PaperXI.DyadicAffine
9 
10 variable {V : Type*} [AddCommGroup V] [Module (ZMod 2) V]
11 
12 /-- A quadratic refinement is specified by its actual polar identity. -/
13 structure Refinement (b : V →ₗ[ZMod 2] V →ₗ[ZMod 2] ZMod 2) where
14   value : V → ZMod 2
15   polar : ∀ x y, value (x + y) = value x + value y + b x y
16 
17 variable {b : V →ₗ[ZMod 2] V →ₗ[ZMod 2] ZMod 2}
18 
19 @[ext] theorem Refinement.ext {q r : Refinement b}
20     (h : ∀ x, q.value x = r.value x) : q = r := by
21   cases q
22   cases r
23   simp_all [mk.injEq, funext_iff]
24 
25 @[simp] theorem Refinement.value_zero (q : Refinement b) : q.value 0 = 0 := by
26   have h := q.polar 0 0
27   simp only [map_zero, add_zero] at h
28   exact (add_eq_left.mp h.symm)
29 
30 /-- Subtracting two refinements cancels their common polar form. -/
31 theorem difference_add (q r : Refinement b) (x y : V) :
32     q.value (x + y) - r.value (x + y) =
33       (q.value x - r.value x) + (q.value y - r.value y) := by
34   rw [q.polar, r.polar]
35   ring
36 
37 /-- Additivity over the prime field gives an actual linear functional. -/
38 def linearDifference (q r : Refinement b) : V →ₗ[ZMod 2] ZMod 2 :=
39   ({ toFun := fun x => q.value x - r.value x
40      map_zero' := by simp
41      map_add' := difference_add q r } : V →+ ZMod 2).toZModLinearMap 2
42 
43 @[simp] theorem linearDifference_apply (q r : Refinement b) (x : V) :
44     linearDifference q r x = q.value x - r.value x := rfl
45 
46 /-- Every linear functional can be added to a refinement. -/
47 def addLinear (q : Refinement b) (l : V →ₗ[ZMod 2] ZMod 2) : Refinement b where
48   value x := q.value x + l x
49   polar x y := by
50     rw [q.polar, map_add]
51     ring
52 
53 @[simp] theorem addLinear_apply (q : Refinement b) (l : V →ₗ[ZMod 2] ZMod 2)
54     (x : V) : (addLinear q l).value x = q.value x + l x := rfl
55 
56 @[simp] theorem addLinear_linearDifference (q r : Refinement b) :
57     addLinear r (linearDifference q r) = q := by
58   ext x
59   simp
60 
61 @[simp] theorem linearDifference_addLinear (q : Refinement b)
62     (l : V →ₗ[ZMod 2] ZMod 2) : linearDifference (addLinear q l) q = l := by
63   ext x
64   simp
65 
66 /-- Choosing one refinement identifies all refinements with the dual space. -/
67 def refinementEquiv (q₀ : Refinement b) :
68     Refinement b ≃ (V →ₗ[ZMod 2] ZMod 2) where
69   toFun q := linearDifference q q₀
70   invFun l := addLinear q₀ l
71   left_inv := fun q => addLinear_linearDifference q q₀
72   right_inv := linearDifference_addLinear q₀
73 
74 theorem exists_unique_linear_difference (q q₀ : Refinement b) :
75     ∃! l : V →ₗ[ZMod 2] ZMod 2, addLinear q₀ l = q := by
76   refine ⟨linearDifference q q₀, addLinear_linearDifference q q₀, ?_⟩
77   intro l hl
78   have h := congrArg (fun r => linearDifference r q₀) hl
79   simpa using h
80 
81 end PaperXI.DyadicAffine

Back to source controls