ReleaseResultantIntegralPackets.lean

1 import KomorebiVerification.PaperII.ReleaseResultantPackets
2 
3 set_option autoImplicit false
4 noncomputable section
5 
6 namespace Komorebi.PaperII.ReleaseResultantIntegralPackets
7 
8 open Polynomial ResultantSeparation ReleaseResultantPolynomial ReleaseResultantPackets
9 open scoped TensorProduct
10 
11 universe u v w z
12 variable {R : Type u} {K : Type v} {L : Type w} {ι : Type z}
13 variable [CommRing R] [Field K] [Algebra R K] [AddCommGroup L] [Module R L]
14 variable [Module.Free R L] [Module.Finite R L] [Fintype ι] [DecidableEq ι]
15 
16 /-- The several-packet theorem retains the integral resultant of each pair,
17 the actual tensor-extended operator, and the actual image lattice. -/
18 theorem integral_spectral_packets_exist (A : Module.End R L) (f : ι → R[X])
19     (hf : ∀ i, (f i).Monic)
20     (hc : Pairwise fun i j =>
21       IsCoprime ((f i).map (algebraMap R K)) ((f j).map (algebraMap R K)))
22     (hchar : A.charpoly = ∏ i, f i) :
23     ∃ E : ι → Module.End K (K ⊗[R] L),
24       (∀ i, E i * E i = E i) ∧
25       (∀ i, LinearMap.range (E i) =
26         LinearMap.ker (aeval (A.baseChange K) ((f i).map (algebraMap R K)))) ∧
27       (∑ i, E i) = 1 ∧
28       (∀ i j, i ≠ j → E i * E j = 0) ∧
29       ∀ i x, x ∈ tensorLattice (K := K) (R := R) (L := L) →
30         (algebraMap R K ((f i).resultant (∏ j ∈ Finset.univ.erase i, f j)) • E i) x ∈
31           tensorLattice (K := K) (R := R) (L := L) := by
32   let g (i : ι) : R[X] := ∏ j ∈ Finset.univ.erase i, f j
33   let fK (i : ι) : K[X] := (f i).map (algebraMap R K)
34   have hg (i : ι) : (g i).Monic := monic_prod_of_monic _ _ (fun j _ => hf j)
35   have hmapg (i : ι) : (g i).map (algebraMap R K) = complementaryFactor fK i := by
36     simp [g, complementaryFactor, fK, Polynomial.map_prod]
37   have hcop (i : ι) : IsCoprime ((f i).map (algebraMap R K))
38       ((g i).map (algebraMap R K)) := by
39     rw [hmapg]
40     exact coprime_complement fK hc i
41   have hfact (i : ι) : A.charpoly = f i * g i := by
42     rw [hchar]
43     exact (Finset.mul_prod_erase _ _ (Finset.mem_univ i)).symm
44   have hex (i : ι) := integral_resultant_projector A (f i) (g i) (hf i) (hg i)
45     (hcop i) (hfact i)
46   choose u v hb cert hidem hrange hker hcompl hclear using hex
47   let E (i : ι) := separator (algebraMap R K ((f i).resultant (g i)))
48     (aeval (A.baseChange K) ((v i).map (algebraMap R K)))
49     (aeval (A.baseChange K) ((g i).map (algebraMap R K)))
50   have hcharK : (A.baseChange K).charpoly = ∏ i, fK i := by
51     simp only [LinearMap.charpoly_baseChange, hchar, Polynomial.map_prod, fK]
52   have hfix (i : ι) (x : K ⊗[R] L)
53       (hx : x ∈ LinearMap.ker (aeval (A.baseChange K) (fK i))) : E i x = x :=
54     separator_apply_of_mem_ker_F (cert i) hx
55   have hzero (i j : ι) (hij : i ≠ j) (x : K ⊗[R] L)
56       (hx : x ∈ LinearMap.ker (aeval (A.baseChange K) (fK j))) : E i x = 0 := by
57     apply separator_apply_of_mem_ker_G
58     rw [hmapg]
59     exact kernel_le_of_dvd (A.baseChange K) (factor_dvd_other_complement fK hij) hx
60   have hassemble := assemble_projectors (A.baseChange K) fK hc hcharK E hrange hfix hzero
61   exact ⟨E, hidem, hrange, hassemble.1, hassemble.2, hclear⟩
62 
63 end Komorebi.PaperII.ReleaseResultantIntegralPackets

Back to source controls