ReleaseCoordinatesResidue.lean

1 import KomorebiVerification.PaperII.ResidueFourierCRT
2 import KomorebiVerification.PaperII.CommonRefinement
3 
4 /-! Actual residue packet families, onto parent maps, and formal-series coordinates. -/
5 set_option autoImplicit false
6 noncomputable section
7 namespace Komorebi.Residue
8 open Komorebi.Foundation Komorebi.PaperII.NestedRefinement
9 universe u v
10 variable {R : Type u} {A : Type v}
11 
12 /-- Residue selectors packaged as a complete family on all coefficient sequences. -/
13 def residueFamily [Semiring R] [AddCommMonoid A] [Module R A]
14     (N : Nat) (hN : 0 < N) : LinearProjectorFamily R (Nat → A) (Fin N) :=
15   Packet.fibreLinearProjectorFamily (residueAddress N hN)
16 
17 theorem residueProj_nonzero [Semiring R] [AddCommMonoid A] [Module R A] [Nontrivial A]
18     (N : Nat) (hN : 0 < N) (j : Fin N) :
19     residueProj (R := R) (A := A) N hN j ≠ 0 := by
20   obtain ⟨a, ha⟩ := exists_ne (0 : A)
21   intro hz
22   have hj : residueAddress N hN j.val = j := Fin.ext (Nat.mod_eq_of_lt j.isLt)
23   have h := congrArg (fun f : Module.End R (Nat → A) => f (fun _ => a) j.val) hz
24   have : a = 0 := by simpa [residueProj_apply, Packet.fibreProj, hj] using h
25   exact ha this
26 
27 theorem residueFamily_nonzero [Semiring R] [AddCommMonoid A] [Module R A] [Nontrivial A]
28     (N : Nat) (hN : 0 < N) :
29     Komorebi.PaperII.CommonRefinement.Nonzero (residueFamily (R := R) (A := A) N hN) :=
30   residueProj_nonzero N hN
31 
32 /-- The actual parent for arbitrary positive divisible moduli. -/
33 def divisorParent (N M : Nat) (hN : 0 < N) : Fin M → Fin N :=
34   fun s => ⟨s.val % N, Nat.mod_lt s.val hN⟩
35 
36 theorem divisorParent_surjective (N M : Nat) (hN : 0 < N) (hM : 0 < M)
37     (hdiv : N ∣ M) : Function.Surjective (divisorParent N M hN) := by
38   intro j
39   refine ⟨⟨j.val, lt_of_lt_of_le j.isLt (Nat.le_of_dvd hM hdiv)⟩, ?_⟩
40   exact Fin.ext (Nat.mod_eq_of_lt j.isLt)
41 
42 theorem divisorParent_address (N M : Nat) (hN : 0 < N) (hM : 0 < M)
43     (hdiv : N ∣ M) :
44     divisorParent N M hN ∘ residueAddress M hM = residueAddress N hN := by
45   funext n
46   exact Fin.ext (Nat.mod_mod_of_dvd n hdiv)
47 
48 /-- The manuscript divisibility refinement, with an explicitly onto parent. -/
49 theorem residueFamily_refines [Semiring R] [AddCommMonoid A] [Module R A]
50     (N M : Nat) (hN : 0 < N) (hM : 0 < M) (hdiv : N ∣ M) :
51     Refines (residueFamily (R := R) (A := A) N hN)
52       (residueFamily (R := R) (A := A) M hM) (divisorParent N M hN) := by
53   classical
54   refine ⟨divisorParent_surjective N M hN hM hdiv, ?_⟩
55   intro j
56   change Packet.fibreLinearProj (R := R) (M := A) (residueAddress N hN) j = _
57   rw [← divisorParent_address N M hN hM hdiv]
58   have h := Packet.fibreLinearProj_refinement (R := R) (M := A)
59     (residueAddress M hM) (divisorParent N M hN) j
60   rw [children, Finset.sum_filter]
61   trans (∑ c : Fin M, if divisorParent N M hN c = j then
62     Packet.fibreLinearProj (R := R) (M := A) (residueAddress M hM) c else 0)
63   · exact h
64   · apply Finset.sum_congr rfl
65     intro c _
66     by_cases hc : divisorParent N M hN c = j <;>
67       simp [hc, residueFamily, Packet.fibreLinearProjectorFamily]
68 
69 /-- Coefficients and the power-series constructor are inverse linear maps. -/
70 def coefficientEquiv [Semiring R] : PowerSeries R ≃ₗ[R] (Nat → R) where
71   toFun f n := PowerSeries.coeff n f
72   invFun := PowerSeries.mk
73   left_inv f := by ext n; simp
74   right_inv x := by funext n; simp
75   map_add' f g := by funext n; exact map_add (PowerSeries.coeff n) f g
76   map_smul' c f := by funext n; exact map_smul (PowerSeries.coeff n) c f
77 
78 @[simp] theorem coefficientEquiv_apply [Semiring R] (f : PowerSeries R) (n : Nat) :
79     coefficientEquiv f n = PowerSeries.coeff n f := rfl
80 
81 /-- A series residue projector, expressed through its actual coefficient mask. -/
82 def seriesResidueProj [Semiring R] (N : Nat) (hN : 0 < N) (j : Fin N) :
83     Module.End R (PowerSeries R) :=
84   coefficientEquiv.symm.toLinearMap.comp
85     ((residueProj (R := R) (A := R) N hN j).comp coefficientEquiv.toLinearMap)
86 
87 @[simp] theorem seriesResidueProj_coeff [Semiring R]
88     (N : Nat) (hN : 0 < N) (j : Fin N) (f : PowerSeries R) (n : Nat) :
89     PowerSeries.coeff n (seriesResidueProj N hN j f) =
90       if residueAddress N hN n = j then PowerSeries.coeff n f else 0 := by
91   simp [seriesResidueProj, coefficientEquiv, residueProj_apply, Packet.fibreProj]
92 
93 @[simp] theorem coefficient_seriesResidueProj [Semiring R]
94     (N : Nat) (hN : 0 < N) (j : Fin N) (f : PowerSeries R) :
95     coefficientEquiv (seriesResidueProj N hN j f) =
96       residueProj (R := R) (A := R) N hN j (coefficientEquiv f) := by
97   simp [seriesResidueProj]
98 
99 /-- The formal-series family carries the exact selector axioms. -/
100 def seriesResidueFamily [Semiring R] (N : Nat) (hN : 0 < N) :
101     LinearProjectorFamily R (PowerSeries R) (Fin N) where
102   proj := seriesResidueProj N hN
103   idempotent j f := by
104     apply coefficientEquiv.injective
105     simp only [coefficient_seriesResidueProj]
106     exact (residueFamily (R := R) (A := R) N hN).idempotent j _
107   orthogonal := by
108     intro i j hij f
109     apply coefficientEquiv.injective
110     simp only [coefficient_seriesResidueProj, map_zero]
111     exact (residueFamily (R := R) (A := R) N hN).orthogonal hij _
112   complete f := by
113     apply coefficientEquiv.injective
114     simp only [map_sum, coefficient_seriesResidueProj]
115     exact (residueFamily (R := R) (A := R) N hN).complete _
116 
117 theorem seriesResidueProj_nonzero [Semiring R] [Nontrivial R]
118     (N : Nat) (hN : 0 < N) (j : Fin N) :
119     seriesResidueProj (R := R) N hN j ≠ 0 := by
120   intro hz
121   apply residueProj_nonzero (R := R) (A := R) N hN j
122   ext x n
123   have h := congrArg (fun T : Module.End R (PowerSeries R) =>
124     coefficientEquiv (T (coefficientEquiv.symm x)) n) hz
125   simpa only [coefficient_seriesResidueProj, LinearEquiv.apply_symm_apply,
126     LinearMap.zero_apply, map_zero, Pi.zero_apply] using h
127 
128 theorem seriesResidueFamily_refines [Semiring R]
129     (N M : Nat) (hN : 0 < N) (hM : 0 < M) (hdiv : N ∣ M) :
130     Refines (seriesResidueFamily (R := R) N hN) (seriesResidueFamily M hM)
131       (divisorParent N M hN) := by
132   refine ⟨divisorParent_surjective N M hN hM hdiv, ?_⟩
133   intro j
134   ext f n
135   have h := LinearMap.congr_fun
136     ((residueFamily_refines (R := R) (A := R) N M hN hM hdiv).coarse_eq_sum_children j)
137     (coefficientEquiv f)
138   have hh := congrFun h n
139   simpa [seriesResidueFamily, LinearMap.sum_apply, ← coefficientEquiv_apply,
140     coefficient_seriesResidueProj, map_sum, residueFamily,
141     Packet.fibreLinearProjectorFamily, residueProj] using hh
142 
143 /-- The exact CRT selector identity on formal series, not merely coefficient sequences. -/
144 theorem seriesResidueProj_crt [Semiring R]
145     (m n : Nat) (hm : 0 < m) (hn : 0 < n) (hc : m.Coprime n)
146     (s : Fin (m * n)) :
147     (seriesResidueProj (R := R) m hm (crtComponents m n hm hn s).1).comp
148         (seriesResidueProj n hn (crtComponents m n hm hn s).2) =
149       seriesResidueProj (m * n) (Nat.mul_pos hm hn) s := by
150   apply LinearMap.ext
151   intro f
152   apply coefficientEquiv.injective
153   simp only [LinearMap.comp_apply, coefficient_seriesResidueProj]
154   exact LinearMap.congr_fun (residueProj_crt (R := R) (A := R) m n hm hn hc s) _
155 
156 end Komorebi.Residue
157 #print axioms Komorebi.Residue.residueFamily_refines
158 #print axioms Komorebi.Residue.seriesResidueFamily_refines
159 #print axioms Komorebi.Residue.seriesResidueProj_crt

Back to source controls