ReleaseResultantPackets.lean

1 import KomorebiVerification.PaperII.ReleaseResultantPolynomial
2 import Mathlib.RingTheory.Polynomial.Basic
3 import Mathlib.RingTheory.Coprime.Lemmas
4 
5 set_option autoImplicit false
6 noncomputable section
7 
8 namespace Komorebi.PaperII.ReleaseResultantPackets
9 
10 open Polynomial ResultantSeparation ReleaseResultantPolynomial
11 
12 universe u v w
13 variable {K : Type u} {M : Type v} {ι : Type w}
14 variable [Field K] [AddCommGroup M] [Module K M] [Fintype ι] [DecidableEq ι]
15 
16 omit [Fintype ι] in
17 /-- Coprime kernel decomposition, proved for every finite subcollection. -/
18 theorem zero_on_product_kernel (A T : Module.End K M) (f : ι → K[X])
19     (hc : Pairwise fun i j => IsCoprime (f i) (f j))
20     (s : Finset ι)
21     (hT : ∀ i ∈ s, ∀ x ∈ LinearMap.ker (aeval A (f i)), T x = 0) :
22     ∀ x ∈ LinearMap.ker (aeval A (∏ i ∈ s, f i)), T x = 0 := by
23   induction s using Finset.induction_on with
24   | empty =>
25       intro x hx
26       have hx0 : x = 0 := by simpa using hx
27       simp [hx0]
28   | @insert a s ha ih =>
29       have hcop : IsCoprime (f a) (∏ i ∈ s, f i) :=
30         IsCoprime.prod_right fun i hi => hc (by
31           intro h
32           subst i
33           exact ha hi)
34       intro x hx
35       rw [Finset.prod_insert ha,
36         ← Polynomial.sup_ker_aeval_eq_ker_aeval_mul_of_coprime A hcop] at hx
37       obtain ⟨y, hy, z, hz, rfl⟩ := Submodule.mem_sup.mp hx
38       rw [map_add, hT a (Finset.mem_insert_self _ _) y hy,
39         ih (fun i hi => hT i (Finset.mem_insert_of_mem hi)) z hz, add_zero]
40 
41 /-- A map vanishing on every primary packet vanishes on the whole module. -/
42 theorem eq_zero_of_packet_kernels [Module.Free K M] [Module.Finite K M]
43     (A T : Module.End K M) (f : ι → K[X])
44     (hc : Pairwise fun i j => IsCoprime (f i) (f j))
45     (hchar : A.charpoly = ∏ i, f i)
46     (hT : ∀ i, ∀ x ∈ LinearMap.ker (aeval A (f i)), T x = 0) : T = 0 := by
47   ext x
48   apply zero_on_product_kernel A T f hc Finset.univ (fun i _ => hT i) x
49   rw [← hchar, A.aeval_self_charpoly]
50   exact LinearMap.mem_ker.mpr rfl
51 
52 /-- An actual polynomial divisibility witness implies inclusion of evaluated kernels. -/
53 theorem kernel_le_of_dvd (A : Module.End K M) {f g : K[X]} (h : f ∣ g) :
54     LinearMap.ker (aeval A f) ≤ LinearMap.ker (aeval A g) := by
55   obtain ⟨p, rfl⟩ := h
56   intro x hx
57   change aeval A (f * p) x = 0
58   rw [mul_comm, map_mul, Module.End.mul_apply, LinearMap.mem_ker.mp hx, map_zero]
59 
60 def complementaryFactor (f : ι → K[X]) (i : ι) : K[X] :=
61   ∏ j ∈ Finset.univ.erase i, f j
62 
63 theorem factor_mul_complement (f : ι → K[X]) (i : ι) :
64     f i * complementaryFactor f i = ∏ j, f j := by
65   exact Finset.mul_prod_erase _ _ (Finset.mem_univ i)
66 
67 theorem coprime_complement (f : ι → K[X])
68     (hc : Pairwise fun i j => IsCoprime (f i) (f j)) (i : ι) :
69     IsCoprime (f i) (complementaryFactor f i) := by
70   exact IsCoprime.prod_right fun j hj => hc (Finset.mem_erase.mp hj).1.symm
71 
72 theorem factor_dvd_other_complement (f : ι → K[X]) {i j : ι} (hij : i ≠ j) :
73     f j ∣ complementaryFactor f i := by
74   exact Finset.dvd_prod_of_mem _ (Finset.mem_erase.mpr ⟨hij.symm, Finset.mem_univ j⟩)
75 
76 /-- Packet actions plus coprime polynomial decomposition force completeness
77 and orthogonality; these identities are not fields of an input certificate. -/
78 theorem assemble_projectors [Module.Free K M] [Module.Finite K M]
79     (A : Module.End K M) (f : ι → K[X])
80     (hc : Pairwise fun i j => IsCoprime (f i) (f j))
81     (hchar : A.charpoly = ∏ i, f i) (E : ι → Module.End K M)
82     (hrange : ∀ i, LinearMap.range (E i) = LinearMap.ker (aeval A (f i)))
83     (hfix : ∀ i, ∀ x ∈ LinearMap.ker (aeval A (f i)), E i x = x)
84     (hzero : ∀ i j, i ≠ j → ∀ x ∈ LinearMap.ker (aeval A (f j)), E i x = 0) :
85     (∑ i, E i) = 1 ∧ ∀ i j, i ≠ j → E i * E j = 0 := by
86   constructor
87   · apply sub_eq_zero.mp
88     apply eq_zero_of_packet_kernels A _ f hc hchar
89     intro j x hx
90     change (∑ i, E i) x - x = 0
91     rw [LinearMap.sum_apply]
92     have hs : (∑ i, E i x) = E j x := by
93       apply Finset.sum_eq_single j
94       · intro i _ hij
95         exact hzero i j hij x hx
96       · simp
97     rw [hs, hfix j x hx, sub_self]
98   · intro i j hij
99     ext x
100     apply hzero i j hij
101     rw [← hrange j]
102     exact LinearMap.mem_range_self (E j) x
103 
104 /-- Every finite coprime characteristic factorization constructs a complete
105 orthogonal family whose members have exact packet ranges. -/
106 theorem spectral_packets_exist [Module.Free K M] [Module.Finite K M]
107     (A : Module.End K M) (f : ι → K[X]) (hf : ∀ i, (f i).Monic)
108     (hc : Pairwise fun i j => IsCoprime (f i) (f j))
109     (hchar : A.charpoly = ∏ i, f i) :
110     ∃ E : ι → Module.End K M,
111       (∀ i, E i * E i = E i) ∧
112       (∀ i, LinearMap.range (E i) = LinearMap.ker (aeval A (f i))) ∧
113       (∑ i, E i) = 1 ∧ ∀ i j, i ≠ j → E i * E j = 0 := by
114   have hex (i : ι) := resultant_projector_exists A (f i) (complementaryFactor f i)
115     (hf i) (coprime_complement f hc i)
116     (hchar.trans (factor_mul_complement f i).symm)
117   choose u v hb cert hidem using hex
118   let E (i : ι) := separator ((f i).resultant (complementaryFactor f i))
119     (aeval A (v i)) (aeval A (complementaryFactor f i))
120   have hrange (i : ι) : LinearMap.range (E i) = LinearMap.ker (aeval A (f i)) :=
121     separator_range_eq_first_kernel (cert i)
122   have hfix (i : ι) (x : M) (hx : x ∈ LinearMap.ker (aeval A (f i))) : E i x = x :=
123     separator_apply_of_mem_ker_F (cert i) hx
124   have hzero (i j : ι) (hij : i ≠ j) (x : M)
125       (hx : x ∈ LinearMap.ker (aeval A (f j))) : E i x = 0 :=
126     separator_apply_of_mem_ker_G
127       (kernel_le_of_dvd A (factor_dvd_other_complement f hij) hx)
128   exact ⟨E, hidem, hrange, assemble_projectors A f hc hchar E hrange hfix hzero⟩
129 
130 end Komorebi.PaperII.ReleaseResultantPackets

Back to source controls