ReleaseTransferMultigradedRational.lean

1 import KomorebiVerification.PaperII.ReleaseTransferMultigraded
2 /-! Determinant-adjugate identity for the independently defined multigraded
3 semantic walk series, including arbitrary scalar edge and endpoint weights. -/
4 set_option autoImplicit false
5 open scoped BigOperators
6 
7 namespace Komorebi.PaperII.ReleaseTransferMultigraded
8 universe u v w z
9 variable {V : Type u} {E : Type v} {σ : Type w} {R : Type z}
10 variable [Fintype E] [Fintype V] [DecidableEq V] [DecidableEq σ] [CommRing R]
11 variable (G : Graph V E σ) (m : E → R)
12 
13 noncomputable def series (s t : V) : MvPowerSeries σ R := coefficient G m s t
14 
15 omit [Fintype V] [DecidableEq σ] in
16 @[simp] theorem coeff_series (s t : V) (n : σ →₀ ℕ) :
17     MvPowerSeries.coeff n (series G m s t) = coefficient G m s t n := rfl
18 
19 noncomputable def adjacency : Matrix V V (MvPolynomial σ R) :=
20   fun i j ↦ ∑ e : E, if G.source e = i ∧ G.target e = j then
21     MvPolynomial.monomial (G.weight e) (m e) else 0
22 
23 omit [Fintype V] in
24 theorem adjacency_constantCoeff_zero (i j : V) :
25     MvPolynomial.constantCoeff (adjacency G m i j) = 0 := by
26   classical
27   rw [adjacency, map_sum]
28   apply Finset.sum_eq_zero
29   intro e _
30   by_cases h : G.source e = i ∧ G.target e = j <;>
31     simp [h, MvPolynomial.constantCoeff_monomial, G.weight_ne_zero e]
32 
33 noncomputable def adjacencySeries : Matrix V V (MvPowerSeries σ R) :=
34   MvPolynomial.coeToMvPowerSeries.ringHom.mapMatrix (adjacency G m)
35 
36 noncomputable def seriesMatrix : Matrix V V (MvPowerSeries σ R) := fun s t ↦ series G m s t
37 
38 omit [DecidableEq σ] in
39 theorem adjacencySeries_mul_seriesMatrix_apply (s t : V) :
40     (adjacencySeries G m * seriesMatrix G m) s t =
41       ∑ e : E, if G.source e = s then
42         MvPowerSeries.monomial (G.weight e) (m e) * series G m (G.target e) t else 0 := by
43   classical
44   have hadj (i j : V) : adjacencySeries G m i j =
45       ∑ e : E, if G.source e = i ∧ G.target e = j then
46         MvPowerSeries.monomial (G.weight e) (m e) else 0 := by
47     rw [adjacencySeries, RingHom.mapMatrix_apply, Matrix.map_apply, adjacency, map_sum]
48     apply Finset.sum_congr rfl
49     intro e _
50     by_cases h : G.source e = i ∧ G.target e = j <;> simp [h]
51   rw [Matrix.mul_apply]
52   simp_rw [hadj, Finset.sum_mul]
53   rw [Finset.sum_comm]
54   apply Finset.sum_congr rfl
55   intro e _
56   by_cases hs : G.source e = s
57   · simp [hs, seriesMatrix]
58   · simp [hs]
59 
60 omit [DecidableEq σ] in
61 theorem coeff_adjacency_mul_series (s t : V) (n : σ →₀ ℕ) :
62     MvPowerSeries.coeff n ((adjacencySeries G m * seriesMatrix G m) s t) =
63       ∑ e : E, if G.source e = s ∧ G.weight e ≤ n then
64         m e * coefficient G m (G.target e) t (n - G.weight e) else 0 := by
65   classical
66   rw [adjacencySeries_mul_seriesMatrix_apply, map_sum]
67   apply Finset.sum_congr rfl
68   intro e _
69   by_cases hs : G.source e = s
70   · simp [hs, MvPowerSeries.coeff_monomial_mul]
71   · simp [hs]
72 
73 theorem seriesMatrix_eq_one_add_adjacency_mul :
74     seriesMatrix G m = 1 + adjacencySeries G m * seriesMatrix G m := by
75   ext s t n
76   change MvPowerSeries.coeff n (series G m s t) =
77     MvPowerSeries.coeff n ((1 : Matrix V V (MvPowerSeries σ R)) s t +
78       (adjacencySeries G m * seriesMatrix G m) s t)
79   rw [coeff_series, map_add, coeff_adjacency_mul_series]
80   have hrec := coefficient_firstEdge G m s t n
81   by_cases hst : s = t
82   · subst t
83     by_cases hn : n = 0 <;> simpa [Matrix.one_apply, MvPowerSeries.coeff_one, hn] using hrec
84   · simpa [Matrix.one_apply, MvPowerSeries.coeff_one, hst] using hrec
85 
86 noncomputable def transfer : Matrix V V (MvPolynomial σ R) := 1 - adjacency G m
87 noncomputable def denominator : MvPolynomial σ R := Matrix.det (transfer G m)
88 noncomputable def denominatorInverse : MvPowerSeries σ R :=
89   MvPowerSeries.invOfUnit (denominator G m : MvPowerSeries σ R) (1 : Rˣ)
90 
91 theorem denominator_constantCoeff : MvPolynomial.constantCoeff (denominator G m) = 1 := by
92   rw [denominator, RingHom.map_det]
93   have h : MvPolynomial.constantCoeff.mapMatrix (transfer G m) = (1 : Matrix V V R) := by
94     ext i j
95     by_cases hij : i = j <;>
96       simp [transfer, RingHom.mapMatrix_apply, Matrix.map_apply,
97         adjacency_constantCoeff_zero, Matrix.one_apply, hij]
98   rw [h, Matrix.det_one]
99 
100 theorem denominator_series_constantCoeff :
101     MvPowerSeries.constantCoeff (denominator G m : MvPowerSeries σ R) = 1 := by
102   rw [← MvPowerSeries.coeff_zero_eq_constantCoeff_apply, MvPolynomial.coeff_coe,
103     ← MvPolynomial.constantCoeff_eq, denominator_constantCoeff]
104 
105 theorem denominator_mul_inverse :
106     (denominator G m : MvPowerSeries σ R) * denominatorInverse G m = 1 := by
107   exact MvPowerSeries.mul_invOfUnit _ _ (denominator_series_constantCoeff G m)
108 
109 theorem denominator_inverse_mul :
110     denominatorInverse G m * (denominator G m : MvPowerSeries σ R) = 1 := by
111   exact MvPowerSeries.invOfUnit_mul _ _ (denominator_series_constantCoeff G m)
112 
113 theorem transfer_mul_seriesMatrix :
114     MvPolynomial.coeToMvPowerSeries.ringHom.mapMatrix (transfer G m) * seriesMatrix G m = 1 := by
115   have ht : MvPolynomial.coeToMvPowerSeries.ringHom.mapMatrix (transfer G m) =
116       1 - adjacencySeries G m := by
117     rw [transfer, adjacencySeries, map_sub, map_one]
118   rw [ht, sub_mul, one_mul]
119   exact sub_eq_iff_eq_add.mpr (seriesMatrix_eq_one_add_adjacency_mul G m)
120 
121 theorem seriesMatrix_eq_rationalMatrix : seriesMatrix G m =
122     ReleaseTransferMatrix.rationalMatrix MvPolynomial.coeToMvPowerSeries.ringHom
123       (transfer G m) (denominatorInverse G m) := by
124   let Z := ReleaseTransferMatrix.rationalMatrix MvPolynomial.coeToMvPowerSeries.ringHom
125     (transfer G m) (denominatorInverse G m)
126   have hleft : Z * MvPolynomial.coeToMvPowerSeries.ringHom.mapMatrix (transfer G m) = 1 :=
127     ReleaseTransferMatrix.rationalMatrix_mul _ _ _ (denominator_inverse_mul G m)
128   calc
129     seriesMatrix G m = 1 * seriesMatrix G m := (one_mul _).symm
130     _ = (Z * MvPolynomial.coeToMvPowerSeries.ringHom.mapMatrix (transfer G m)) *
131       seriesMatrix G m := by rw [hleft]
132     _ = Z * (MvPolynomial.coeToMvPowerSeries.ringHom.mapMatrix (transfer G m) *
133       seriesMatrix G m) := mul_assoc _ _ _
134     _ = Z := by rw [transfer_mul_seriesMatrix, mul_one]
135 
136 theorem denominator_mul_series (s t : V) :
137     (denominator G m : MvPowerSeries σ R) * series G m s t =
138       (Matrix.adjugate (transfer G m) s t : MvPolynomial σ R) := by
139   have h := ReleaseTransferMatrix.denominator_smul_rationalMatrix
140     MvPolynomial.coeToMvPowerSeries.ringHom (transfer G m) (denominatorInverse G m)
141     (denominator_mul_inverse G m)
142   rw [← seriesMatrix_eq_rationalMatrix] at h
143   exact congrFun (congrFun h s) t
144 
145 noncomputable def endpointSeries (u v : V → R) : MvPowerSeries σ R :=
146   ReleaseTransferMatrix.contract (MvPowerSeries.C ∘ u) (seriesMatrix G m) (MvPowerSeries.C ∘ v)
147 
148 noncomputable def endpointNumerator (u v : V → R) : MvPolynomial σ R :=
149   ReleaseTransferMatrix.contract (MvPolynomial.C ∘ u) (Matrix.adjugate (transfer G m))
150     (MvPolynomial.C ∘ v)
151 
152 theorem endpoint_rationality (u v : V → R) :
153     (denominator G m : MvPowerSeries σ R) * endpointSeries G m u v =
154       (endpointNumerator G m u v : MvPowerSeries σ R) := by
155   rw [endpointSeries, seriesMatrix_eq_rationalMatrix]
156   simpa [endpointNumerator, denominator, Function.comp_def] using
157     ReleaseTransferMatrix.rational_endpoint_identity MvPolynomial.coeToMvPowerSeries.ringHom
158       (transfer G m) (denominatorInverse G m) (denominator_mul_inverse G m)
159       (MvPolynomial.C ∘ u) (MvPolynomial.C ∘ v)
160 
161 omit [DecidableEq σ] in
162 theorem endpoint_coeff (u v : V → R) (n : σ →₀ ℕ) :
163     MvPowerSeries.coeff n (endpointSeries G m u v) =
164       ∑ i, ∑ j, u i * coefficient G m i j n * v j := by
165   simp [endpointSeries, ReleaseTransferMatrix.contract, seriesMatrix,
166     map_sum, MvPowerSeries.coeff_C_mul, MvPowerSeries.coeff_mul_C]
167 
168 end Komorebi.PaperII.ReleaseTransferMultigraded

Back to source controls