DyadicTorsor.lean

1 import PaperXI.DyadicAffine
2 import Mathlib.Algebra.Torsor.Defs
3 
4 /-! The canonical affine-space structure on a nonempty family of refinements.
5 The action and subtraction are the actual addition and difference of functions. -/
6 set_option autoImplicit false
7 noncomputable section
8 namespace PaperXI.DyadicTorsor
9 open PaperXI.DyadicAffine
10 
11 variable {V : Type*} [AddCommGroup V] [Module (ZMod 2) V]
12 variable {b : V →ₗ[ZMod 2] V →ₗ[ZMod 2] ZMod 2}
13 
14 @[simp] theorem addLinear_zero (q : Refinement b) : addLinear q 0 = q := by
15   ext x
16   simp
17 
18 theorem addLinear_add (q : Refinement b) (l m : V →ₗ[ZMod 2] ZMod 2) :
19     addLinear q (l + m) = addLinear (addLinear q m) l := by
20   ext x
21   simp only [addLinear_apply, LinearMap.add_apply]
22   abel
23 
24 theorem addLinear_injective (q : Refinement b) :
25     Function.Injective (addLinear q) := by
26   intro l m h
27   have h' := congrArg (fun r => linearDifference r q) h
28   simpa only [linearDifference_addLinear] using h'
29 
30 theorem addLinear_free (q : Refinement b) (l : V →ₗ[ZMod 2] ZMod 2) :
31     addLinear q l = q ↔ l = 0 := by
32   constructor
33   · intro h
34     apply addLinear_injective q
35     simpa only [addLinear_zero] using h
36   · intro h
37     rw [h, addLinear_zero]
38 
39 theorem addLinear_transitive (q r : Refinement b) :
40     ∃ l : V →ₗ[ZMod 2] ZMod 2, addLinear q l = r :=
41   ⟨linearDifference r q, addLinear_linearDifference r q⟩
42 
43 /-- The canonical action exists even when the family of refinements is empty. -/
44 instance instAddAction : AddAction (V →ₗ[ZMod 2] ZMod 2) (Refinement b) where
45   vadd l q := addLinear q l
46   add_vadd l m q := addLinear_add q l m
47   zero_vadd := addLinear_zero
48 
49 instance instVSub : VSub (V →ₗ[ZMod 2] ZMod 2) (Refinement b) where
50   vsub := linearDifference
51 
52 /-- A nonempty family of refinements is an affine space over the dual vector
53 space, with no choice of origin used to define either operation. -/
54 instance instAddTorsor [Nonempty (Refinement b)] :
55     AddTorsor (V →ₗ[ZMod 2] ZMod 2) (Refinement b) where
56   vsub_vadd' := addLinear_linearDifference
57   vadd_vsub' l q := linearDifference_addLinear q l
58 
59 /-- A named reference exposes the entire bundled structure to declaration
60 audits, including the canonical action and subtraction instances. -/
61 abbrev canonicalTorsor [Nonempty (Refinement b)] :
62     AddTorsor (V →ₗ[ZMod 2] ZMod 2) (Refinement b) := inferInstance
63 
64 @[simp] theorem vadd_apply (l : V →ₗ[ZMod 2] ZMod 2) (q : Refinement b) (x : V) :
65     (l +ᵥ q).value x = q.value x + l x := rfl
66 
67 @[simp] theorem vsub_apply (q r : Refinement b) (x : V) :
68     (q -ᵥ r : V →ₗ[ZMod 2] ZMod 2) x = q.value x - r.value x := rfl
69 
70 end PaperXI.DyadicTorsor

Back to source controls