ReleaseTransferMultigraded.lean

1 import KomorebiVerification.PaperII.ReleaseTransferScalar
2 import Mathlib.Data.Finsupp.Weight
3 import Mathlib.RingTheory.MvPowerSeries.Inverse
4 
5 /-! Exact multigraded walks and rationality. Each edge has a nonzero finitely
6 supported natural exponent vector. Total degree provides a finiteness bound but
7 the coefficient model retains the full exponent vector, not its specialization.
8 -/
9 set_option autoImplicit false
10 open scoped BigOperators
11 
12 noncomputable section
13 
14 namespace Komorebi.PaperII.ReleaseTransferMultigraded
15 open TransferZeta TransferZeta.PositiveWeightedMultigraph
16 universe u v w z
17 variable {V : Type u} {E : Type v} {σ : Type w} {R : Type z}
18 
19 structure Graph (V : Type u) (E : Type v) (σ : Type w) where
20   source : E → V
21   target : E → V
22   weight : E → (σ →₀ ℕ)
23   weight_ne_zero : ∀ e, weight e ≠ 0
24 
25 variable (G : Graph V E σ)
26 
27 def natGraph : PositiveWeightedMultigraph V E where
28   source := G.source
29   target := G.target
30   weight := fun e ↦ (G.weight e).degree
31   weight_pos := fun e ↦ Nat.pos_of_ne_zero (fun h ↦
32     G.weight_ne_zero e ((Finsupp.degree_eq_zero_iff _).mp h))
33 
34 def vectorWeight (es : List E) : σ →₀ ℕ := (es.map G.weight).sum
35 
36 @[simp] theorem vectorWeight_nil : vectorWeight G [] = 0 := rfl
37 @[simp] theorem vectorWeight_cons (e : E) (es : List E) :
38     vectorWeight G (e :: es) = G.weight e + vectorWeight G es := rfl
39 
40 theorem degree_vectorWeight (es : List E) :
41     (vectorWeight G es).degree = (natGraph G).pathWeight es := by
42   induction es with
43   | nil => simp [vectorWeight]
44   | cons e es ih => simp [vectorWeight_cons, map_add, ih, natGraph, pathWeight]
45 
46 abbrev ExactWalk (s t : V) (n : σ →₀ ℕ) :=
47   {es : List E // (natGraph G).IsWalk s t es ∧ vectorWeight G es = n}
48 
49 noncomputable instance [Fintype E] [DecidableEq V] (s t : V) (n : σ →₀ ℕ) :
50     Fintype (ExactWalk G s t n) :=
51   Fintype.ofInjective (fun x : ExactWalk G s t n ↦
52     (⟨x.val, x.property.1, by rw [← degree_vectorWeight, x.property.2]⟩ :
53       (natGraph G).ExactWalk s t n.degree)) (by
54         intro x y h
55         exact Subtype.ext (congrArg (fun z : (natGraph G).ExactWalk s t n.degree ↦ z.val) h))
56 
57 abbrev EmptyWalk (s t : V) (n : σ →₀ ℕ) :=
58   {_x : Unit // s = t ∧ n = 0}
59 
60 abbrev FirstTail (s t : V) (n : σ →₀ ℕ) :=
61   Σ e : E, {_x : ExactWalk G (G.target e) t (n - G.weight e) //
62     G.source e = s ∧ G.weight e ≤ n}
63 
64 def firstEdgeEquiv (s t : V) (n : σ →₀ ℕ) :
65     ExactWalk G s t n ≃ EmptyWalk s t n ⊕ FirstTail G s t n where
66   toFun x := by
67     rcases x with ⟨es, hw, hn⟩
68     cases es with
69     | nil => exact Sum.inl ⟨(), hw, hn.symm⟩
70     | cons e es =>
71       have he : G.weight e + vectorWeight G es = n := hn
72       have hle : G.weight e ≤ n := by rw [← he]; exact le_self_add
73       have hrest : vectorWeight G es = n - G.weight e :=
74         eq_tsub_of_add_eq (by simpa [add_comm] using he)
75       exact Sum.inr ⟨e, ⟨⟨es, hw.2, hrest⟩, hw.1, hle⟩⟩
76   invFun x := by
77     rcases x with h | ⟨e, ⟨⟨es, hw, hn⟩, hs, hle⟩⟩
78     · exact ⟨[], h.property.1, h.property.2.symm⟩
79     · exact ⟨e :: es, ⟨hs, hw⟩, by
80         rw [vectorWeight_cons, hn, add_tsub_cancel_of_le hle]⟩
81   left_inv x := by
82     rcases x with ⟨es, hw, hn⟩
83     cases es <;> rfl
84   right_inv x := by
85     rcases x with h | ⟨e, ⟨⟨es, hw, hn⟩, hs, hle⟩⟩
86     · rfl
87     · rfl
88 
89 variable [Fintype E] [DecidableEq V] [DecidableEq σ] [CommRing R]
90 variable (m : E → R)
91 
92 noncomputable def coefficient (s t : V) (n : σ →₀ ℕ) : R :=
93   ∑ x : ExactWalk G s t n, ReleaseTransferScalar.walkMultiplicity m x.val
94 
95 theorem coefficient_firstEdge (s t : V) (n : σ →₀ ℕ) :
96     coefficient G m s t n = (if s = t ∧ n = 0 then 1 else 0) +
97       ∑ e : E, if G.source e = s ∧ G.weight e ≤ n then
98         m e * coefficient G m (G.target e) t (n - G.weight e) else 0 := by
99   classical
100   let f : EmptyWalk s t n ⊕ FirstTail G s t n → R :=
101     Sum.elim (fun _ ↦ 1)
102       (fun x ↦ m x.1 * ReleaseTransferScalar.walkMultiplicity m x.2.val.val)
103   have hfirst : coefficient G m s t n = ∑ x, f x := by
104     apply Fintype.sum_equiv (firstEdgeEquiv G s t n)
105     intro x
106     rcases x with ⟨es, hw, hn⟩
107     cases es <;> rfl
108   rw [hfirst, Fintype.sum_sum_type]
109   change (∑ _x : EmptyWalk s t n, (1 : R)) +
110     (∑ x : FirstTail G s t n, m x.1 * ReleaseTransferScalar.walkMultiplicity m x.2.val.val) = _
111   have hempty : (∑ _x : EmptyWalk s t n, (1 : R)) =
112       if s = t ∧ n = 0 then 1 else 0 := by
113     by_cases h : s = t ∧ n = 0 <;> simp [EmptyWalk, h]
114   rw [hempty]
115   congr 1
116   rw [Fintype.sum_sigma]
117   apply Finset.sum_congr rfl
118   intro e _
119   by_cases h : G.source e = s ∧ G.weight e ≤ n
120   · rw [ite_eq_left h, coefficient, Finset.mul_sum]
121     apply Fintype.sum_equiv (Equiv.subtypeUnivEquiv fun _ ↦ h)
122     intro x
123     rfl
124   · rw [ite_eq_right h]
125     apply Finset.sum_eq_zero
126     intro x _
127     exact False.elim (h x.property)
128 
129 end Komorebi.PaperII.ReleaseTransferMultigraded

Back to source controls