ResidueProjectors.lean

1 import KomorebiVerification.FibreRefinement
2 
3 /-!
4 # Residue-class projectors and exact refinement
5 
6 This file turns the constructive fibre masks from `Komorebi.Packet` into
7 genuine linear endomorphisms on sequences indexed by `Nat`.  It then proves
8 the arithmetic compatibility needed to refine residue classes modulo `N`
9 into residue classes modulo `N * M`.
10 -/
11 
12 set_option autoImplicit false
13 
14 namespace Komorebi
15 namespace Residue
16 
17 universe u v
18 
19 /-- The address of a natural number in its residue class modulo a positive
20 modulus. -/
21 def residueAddress (N : Nat) (hN : 0 < N) : Nat → Fin N :=
22   fun n => ⟨n % N, Nat.mod_lt n hN⟩
23 
24 /-- The finer residue address modulo `N * M`. -/
25 def fineAddress (N M : Nat) (hN : 0 < N) (hM : 0 < M) : Nat → Fin (N * M) :=
26   residueAddress (N * M) (Nat.mul_pos hN hM)
27 
28 /-- Forget the fine component of a residue modulo `N * M`, retaining only
29 its residue modulo `N`. -/
30 def mergeAddress (N M : Nat) (hN : 0 < N) : Fin (N * M) → Fin N :=
31   fun s => ⟨s.val % N, Nat.mod_lt s.val hN⟩
32 
33 /-- Reducing modulo `N * M` and then modulo `N` agrees with reducing directly
34 modulo `N`.  This is the arithmetic input to projector refinement. -/
35 theorem merge_fineAddress
36     (N M : Nat) (hN : 0 < N) (hM : 0 < M) :
37     mergeAddress N M hN ∘ fineAddress N M hN hM = residueAddress N hN := by
38   funext n
39   apply Fin.ext
40   exact Nat.mod_mul_right_mod n N M
41 
42 /-- Function-level residue refinement, obtained from the independent modular
43 arithmetic lemma and the pointwise fibre decomposition. -/
44 theorem residueFibre_refinement
45     {A : Type v} [AddCommMonoid A]
46     (N M : Nat) (hN : 0 < N) (hM : 0 < M)
47     (r : Fin N) (x : Nat → A) :
48     Packet.fibreProj (residueAddress N hN) r x =
49       ∑ s : Fin (N * M),
50         if mergeAddress N M hN s = r then
51           Packet.fibreProj (fineAddress N M hN hM) s x
52         else 0 := by
53   rw [← merge_fineAddress N M hN hM]
54   change
55     Packet.fibreProj
56         (fun n => mergeAddress N M hN (fineAddress N M hN hM n)) r x = _
57   exact Packet.fibreProj_refinement
58     (fineAddress N M hN hM) (mergeAddress N M hN) r x
59 
60 /-- The residue mask as an actual linear endomorphism of `A`-valued
61 sequences. -/
62 def residueProj
63     {R : Type u} {A : Type v}
64     [Semiring R] [AddCommMonoid A] [Module R A]
65     (N : Nat) (hN : 0 < N) (r : Fin N) : Module.End R (Nat → A) :=
66   Packet.fibreLinearProj (R := R) (M := A) (residueAddress N hN) r
67 
68 @[simp] theorem residueProj_apply
69     {R : Type u} {A : Type v}
70     [Semiring R] [AddCommMonoid A] [Module R A]
71     (N : Nat) (hN : 0 < N) (r : Fin N) (x : Nat → A) :
72     residueProj (R := R) (A := A) N hN r x =
73       Packet.fibreProj (residueAddress N hN) r x := rfl
74 
75 /-- Exact refinement of a coarse residue projector into all fine residue
76 projectors lying above it. -/
77 theorem residueProj_refinement
78     {R : Type u} {A : Type v}
79     [Semiring R] [AddCommMonoid A] [Module R A]
80     (N M : Nat) (hN : 0 < N) (hM : 0 < M) (r : Fin N) :
81     residueProj (R := R) (A := A) N hN r =
82       ∑ s : Fin (N * M),
83         if mergeAddress N M hN s = r then
84           residueProj (R := R) (A := A) (N * M) (Nat.mul_pos hN hM) s
85         else 0 := by
86   change
87     Packet.fibreLinearProj (R := R) (M := A) (residueAddress N hN) r = _
88   rw [← merge_fineAddress N M hN hM]
89   change
90     Packet.fibreLinearProj (R := R) (M := A)
91         (fun n => mergeAddress N M hN (fineAddress N M hN hM n)) r =
92       ∑ s : Fin (N * M),
93         if mergeAddress N M hN s = r then
94           Packet.fibreLinearProj (R := R) (M := A)
95             (fineAddress N M hN hM) s
96         else 0
97   exact Packet.fibreLinearProj_refinement
98     (fineAddress N M hN hM) (mergeAddress N M hN) r
99 
100 #print axioms merge_fineAddress
101 #print axioms residueFibre_refinement
102 #print axioms residueProj_refinement
103 
104 end Residue
105 end Komorebi

Back to source controls