• API
• FAQ
• Tools
• Archive
SHARE
TWEET

# Untitled

a guest Jul 24th, 2019 64 Never
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
1. import data.finsupp order.complete_lattice algebra.ordered_group data.mv_polynomial
2. import algebra.order_functions
3.
4. namespace multiset
5. variables {α : Type*} [decidable_eq α]
6.
7. def to_finsupp (s : multiset α) : α →₀ ℕ :=
8. { support := s.to_finset,
9.   to_fun := λ a, s.count a,
10.   mem_support_to_fun := λ a,
11.   begin
12.     rw mem_to_finset,
13.     convert not_iff_not_of_iff (count_eq_zero.symm),
14.     rw not_not
15.   end }
16.
17. @[simp] lemma to_finsupp_support (s : multiset α) :
18.   s.to_finsupp.support = s.to_finset := rfl
19.
20. @[simp] lemma to_finsupp_apply (s : multiset α) (a : α) :
21.   s.to_finsupp a = s.count a := rfl
22.
23. @[simp] lemma to_finsupp_zero :
24.   to_finsupp (0 : multiset α) = 0 :=
25. finsupp.ext \$ λ a, count_zero a
26.
27. @[simp] lemma to_finsupp_add (s t : multiset α) :
28.   to_finsupp (s + t) = to_finsupp s + to_finsupp t :=
29. finsupp.ext \$ λ a, count_add a s t
30.
31. namespace to_finsupp
32.
33. instance : is_add_monoid_hom (to_finsupp : multiset α → α →₀ ℕ) :=
34. { map_zero := to_finsupp_zero,
36.
37. end to_finsupp
38.
39. @[simp] lemma to_finsupp_to_multiset (s : multiset α) :
40.   s.to_finsupp.to_multiset = s :=
41. ext.2 \$ λ a, by rw [finsupp.count_to_multiset, to_finsupp_apply]
42.
43. end multiset
44.
45. namespace finsupp
46. variables {σ : Type*} {α : Type*} [decidable_eq σ]
47.
48. instance [preorder α] [has_zero α] : preorder (σ →₀ α) :=
49. { le := λ f g, ∀ s, f s ≤ g s,
50.   le_refl := λ f s, le_refl _,
51.   le_trans := λ f g h Hfg Hgh s, le_trans (Hfg s) (Hgh s) }
52.
53. instance [partial_order α] [has_zero α] : partial_order (σ →₀ α) :=
54. { le_antisymm := λ f g hfg hgf, finsupp.ext \$ λ s, le_antisymm (hfg s) (hgf s),
55.   .. finsupp.preorder }
56.
57. instance [ordered_cancel_comm_monoid α] [decidable_eq α] :
58.   add_left_cancel_semigroup (σ →₀ α) :=
59. { add_left_cancel := λ a b c h, finsupp.ext \$ λ s,
60.   by { rw finsupp.ext_iff at h, exact add_left_cancel (h s) },
62.
63. instance [ordered_cancel_comm_monoid α] [decidable_eq α] :
64.   add_right_cancel_semigroup (σ →₀ α) :=
65. { add_right_cancel := λ a b c h, finsupp.ext \$ λ s,
66.   by { rw finsupp.ext_iff at h, exact add_right_cancel (h s) },
68.
69. instance [ordered_cancel_comm_monoid α] [decidable_eq α] :
70.   ordered_cancel_comm_monoid (σ →₀ α) :=
75.
77.
78. @[simp] lemma to_multiset_to_finsupp (f : σ →₀ ℕ) :
79.   f.to_multiset.to_finsupp = f :=
80. ext \$ λ s, by rw [multiset.to_finsupp_apply, count_to_multiset]
81.
82. def diagonal (f : σ →₀ ℕ) : finset ((σ →₀ ℕ) × (σ →₀ ℕ)) :=
83. ((multiset.diagonal f.to_multiset).map (prod.map multiset.to_finsupp multiset.to_finsupp)).to_finset
84.
85. lemma mem_diagonal {f : σ →₀ ℕ} {p : (σ →₀ ℕ) × (σ →₀ ℕ)} :
86.   p ∈ diagonal f ↔ p.1 + p.2 = f :=
87. begin
88.   erw [multiset.mem_to_finset, multiset.mem_map],
89.   split,
90.   { rintros ⟨⟨a, b⟩, h, rfl⟩,
91.     rw multiset.mem_diagonal at h,
92.     simpa using congr_arg multiset.to_finsupp h },
93.   { intro h,
94.     refine ⟨⟨p.1.to_multiset, p.2.to_multiset⟩, _, _⟩,
95.     { simpa using congr_arg to_multiset h },
96.     { rw [prod.map, to_multiset_to_finsupp, to_multiset_to_finsupp, prod.mk.eta] } }
97. end
98.
99. lemma swap_mem_diagonal {n : σ →₀ ℕ} {f} (hf : f ∈ diagonal n) : f.swap ∈ diagonal n :=
100. by simpa [mem_diagonal, add_comm] using hf
101.
102. @[simp] lemma diagonal_zero : diagonal (0 : σ →₀ ℕ) = {(0,0)} := rfl
103.
104. lemma to_multiset_strict_mono : strict_mono (@to_multiset σ _) :=
105. λ m n h,
106. begin
107.   rw lt_iff_le_and_ne at h ⊢, cases h with h₁ h₂,
108.   split,
109.   { rw multiset.le_iff_count, intro s, rw [count_to_multiset, count_to_multiset], exact h₁ s },
110.   { intro H, apply h₂, replace H := congr_arg multiset.to_finsupp H, simpa using H }
111. end
112.
113. lemma sum_lt_of_lt (m n : σ →₀ ℕ) (h : m < n) :
114.   m.sum (λ _, id) < n.sum (λ _, id) :=
115. begin
116.   rw [← card_to_multiset, ← card_to_multiset],
117.   apply multiset.card_lt_of_lt,
118.   exact to_multiset_strict_mono _ _ h
119. end
120.
121. variable (σ)
122.
123. def lt_wf : well_founded (@has_lt.lt (σ →₀ ℕ) _) :=
124. subrelation.wf (sum_lt_of_lt) \$ inv_image.wf _ nat.lt_wf
125.
126. -- instance : has_well_founded (σ →₀ ℕ) :=
127. -- { r := (<),
128. --   wf := lt_wf σ }
129.
130. end finsupp
131.
132. /-- Multivariate power series, where `σ` is the index set of the variables
133. and `α` is the coefficient ring.-/
134. def mv_power_series (σ : Type*) (α : Type*) := (σ →₀ ℕ) → α
135.
136. namespace mv_power_series
137. open finsupp
138. variables {σ : Type*} {α : Type*} [decidable_eq σ]
139.
140. def coeff (n : σ →₀ ℕ) (φ : mv_power_series σ α) := φ n
141.
142. @[extensionality] lemma ext {φ ψ : mv_power_series σ α} (h : ∀ n, coeff n φ = coeff n ψ) : φ = ψ :=
143. funext h
144.
145. lemma ext_iff {φ ψ : mv_power_series σ α} : φ = ψ ↔ (∀ n, coeff n φ = coeff n ψ) :=
146. ⟨λ h n, congr_arg (coeff n) h, ext⟩
147.
148. variables [comm_semiring α]
149.
150. def monomial (n : σ →₀ ℕ) (a : α) : mv_power_series σ α := λ m, if m = n then a else 0
151.
152. lemma coeff_monomial (m n : σ →₀ ℕ) (a : α) :
153.   coeff m (monomial n a) = if m = n then a else 0 := rfl
154.
155. @[simp] lemma coeff_monomial' (n : σ →₀ ℕ) (a : α) :
156.   coeff n (monomial n a) = a := if_pos rfl
157.
158. def C (a : α) : mv_power_series σ α := monomial 0 a
159.
160. lemma coeff_C (n : σ →₀ ℕ) (a : α) :
161.   coeff n (C a : mv_power_series σ α) = if n = 0 then a else 0 := rfl
162.
163. @[simp] lemma coeff_C_zero (a : α) : coeff 0 (C a : mv_power_series σ α) = a :=
164. coeff_monomial' 0 a
165.
166. @[simp] lemma monomial_zero (a : α) : (monomial 0 a : mv_power_series σ α) = C a := rfl
167.
168. def X (s : σ) : mv_power_series σ α := monomial (single s 1) 1
169.
170. lemma coeff_X (n : σ →₀ ℕ) (s : σ) :
171.   coeff n (X s : mv_power_series σ α) = if n = (single s 1) then 1 else 0 := rfl
172.
173. lemma coeff_X' (s t : σ) :
174.   coeff (single t 1) (X s : mv_power_series σ α) = if t = s then 1 else 0 :=
175. if h : t = s then by simp [h, coeff_X] else
176. begin
177.   rw [coeff_X, if_neg h],
178.   split_ifs with H,
179.   { have := @finsupp.single_apply σ ℕ _ _ _ t s 1,
180.     rw [if_neg h, H, finsupp.single_apply, if_pos rfl] at this,
181.     exfalso, exact one_ne_zero this, },
182.   { refl }
183. end
184.
185. @[simp] lemma coeff_X'' (s : σ) :
186.   coeff (single s 1) (X s : mv_power_series σ α) = 1 :=
187. by rw [coeff_X', if_pos rfl]
188.
189. section ring
190. variables (σ) (α) (n : σ →₀ ℕ) (φ ψ : mv_power_series σ α)
191.
192. def zero : mv_power_series σ α := λ n, 0
193.
194. instance : has_zero (mv_power_series σ α) := ⟨zero σ α⟩
195.
196. @[simp] lemma coeff_zero : coeff n (0 : mv_power_series σ α) = 0 := rfl
197.
198. @[simp] lemma C_zero : (C 0 : mv_power_series σ α) = 0 :=
199. ext \$ λ n, if h : n = 0 then by simp [h] else by rw [coeff_C, if_neg h, coeff_zero]
200.
201. def one : mv_power_series σ α := C 1
202.
203. instance : has_one (mv_power_series σ α) := ⟨one σ α⟩
204.
205. @[simp] lemma coeff_one :
206.   coeff n (1 : mv_power_series σ α) = if n = 0 then 1 else 0 := rfl
207.
208. @[simp] lemma coeff_one_zero : coeff 0 (1 : mv_power_series σ α) = 1 :=
209. coeff_C_zero 1
210.
211. @[simp] lemma C_one : (C 1 : mv_power_series σ α) = 1 := rfl
212.
213. def add (φ ψ : mv_power_series σ α) : mv_power_series σ α :=
214. λ n, coeff n φ + coeff n ψ
215.
217.
218. variables {σ α}
219.
220. @[simp] lemma coeff_add : coeff n (φ + ψ) = coeff n φ + coeff n ψ := rfl
221.
222. @[simp] lemma zero_add : (0 : mv_power_series σ α) + φ = φ := ext \$ λ n, zero_add _
223.
224. @[simp] lemma add_zero : φ + 0 = φ := ext \$ λ n, add_zero _
225.
226. lemma add_comm : φ + ψ = ψ + φ := ext \$ λ n, add_comm _ _
227.
228. lemma add_assoc (φ₁ φ₂ φ₃ : mv_power_series σ α) :
229.   (φ₁ + φ₂) + φ₃ = φ₁ + (φ₂ + φ₃) :=
230. ext \$ λ n, by simp
231.
232. @[simp] lemma monomial_add (n : σ →₀ ℕ) (a b : α) :
233.   (monomial n (a + b) : mv_power_series σ α) = monomial n a + monomial n b :=
234. ext \$ λ m, if h : m = n then by simp [h] else by simp [coeff_monomial, if_neg h]
235.
236. @[simp] lemma C_add (a b : α) : (C (a + b) : mv_power_series σ α) = C a + C b :=
238.
239. variables (σ α)
240.
241. def mul (φ ψ : mv_power_series σ α) : mv_power_series σ α :=
242. λ n, (finsupp.diagonal n).sum (λ p, coeff p.1 φ * coeff p.2 ψ)
243. instance : has_mul (mv_power_series σ α) := ⟨mul σ α⟩
244.
245. variables {σ α}
246.
247. lemma coeff_mul :
248.   coeff n (φ * ψ) = (finsupp.diagonal n).sum (λ p, coeff p.1 φ * coeff p.2 ψ) := rfl
249.
250. @[simp] lemma C_mul (a b : α) : (C (a * b) : mv_power_series σ α) = C a * C b :=
251. ext \$ λ n,
252. begin
253.   rw [coeff_C, coeff_mul],
254.   split_ifs,
255.   { subst n, erw [diagonal_zero, finset.sum_singleton, coeff_C_zero, coeff_C_zero] },
256.   { rw finset.sum_eq_zero,
257.     rintros ⟨i,j⟩ hij,
258.     rw mem_diagonal at hij, rw [coeff_C, coeff_C],
259.     split_ifs; try {simp * at *; done} }
260. end
261.
262. @[simp] lemma zero_mul : (0 : mv_power_series σ α) * φ = 0 :=
263. ext \$ λ n, by simp [coeff_mul]
264.
265. @[simp] lemma mul_zero : φ * 0 = 0 :=
266. ext \$ λ n, by simp [coeff_mul]
267.
268. lemma mul_comm : φ * ψ = ψ * φ :=
269. ext \$ λ n, finset.sum_bij (λ p hp, p.swap)
270.   (λ p hp, swap_mem_diagonal hp)
271.   (λ p hp, mul_comm _ _)
272.   (λ p q hp hq H, by simpa using congr_arg prod.swap H)
273.   (λ p hp, ⟨p.swap, swap_mem_diagonal hp, p.swap_swap.symm⟩)
274.
275. @[simp] lemma one_mul : (1 : mv_power_series σ α) * φ = φ :=
276. ext \$ λ n,
277. begin
278.   have H : ((0 : σ →₀ ℕ), n) ∈ (diagonal n) := by simp [mem_diagonal],
279.   rw [coeff_mul, ← finset.insert_erase H, finset.sum_insert (finset.not_mem_erase _ _),
281.   rintros ⟨i,j⟩ hij,
282.   rw [finset.mem_erase, mem_diagonal] at hij,
283.   rw [coeff_one, if_neg, _root_.zero_mul],
284.   intro H, apply hij.1, simp * at *
285. end
286.
287. @[simp] lemma mul_one : φ * 1 = φ :=
288. by rw [mul_comm, one_mul]
289.
290. lemma mul_add (φ₁ φ₂ φ₃ : mv_power_series σ α) :
291.   φ₁ * (φ₂ + φ₃) = φ₁ * φ₂ + φ₁ * φ₃ :=
293.
294. lemma add_mul (φ₁ φ₂ φ₃ : mv_power_series σ α) :
295.   (φ₁ + φ₂) * φ₃ = φ₁ * φ₃ + φ₂ * φ₃ :=
297.
298. lemma mul_assoc (φ₁ φ₂ φ₃ : mv_power_series σ α) :
299.   (φ₁ * φ₂) * φ₃ = φ₁ * (φ₂ * φ₃) :=
300. ext \$ λ n,
301. begin
302.   simp only [coeff_mul],
303.   have := @finset.sum_sigma ((σ →₀ ℕ) × (σ →₀ ℕ)) α _ _ (diagonal n)
304.     (λ p, diagonal (p.1)) (λ x, coeff x.2.1 φ₁ * coeff x.2.2 φ₂ * coeff x.1.2 φ₃),
305.   convert this.symm using 1; clear this,
306.   { apply finset.sum_congr rfl,
307.     intros p hp, exact finset.sum_mul },
308.   have := @finset.sum_sigma ((σ →₀ ℕ) × (σ →₀ ℕ)) α _ _ (diagonal n)
309.     (λ p, diagonal (p.2)) (λ x, coeff x.1.1 φ₁ * (coeff x.2.1 φ₂ * coeff x.2.2 φ₃)),
310.   convert this.symm using 1; clear this,
311.   { apply finset.sum_congr rfl, intros p hp, rw finset.mul_sum },
312.   apply finset.sum_bij,
313.   swap 5,
314.   { rintros ⟨⟨i,j⟩, ⟨k,l⟩⟩ H, exact ⟨(k, l+j), (l, j)⟩ },
315.   { rintros ⟨⟨i,j⟩, ⟨k,l⟩⟩ H, simp only [finset.mem_sigma, mem_diagonal] at H ⊢, finish },
316.   { rintros ⟨⟨i,j⟩, ⟨k,l⟩⟩ H, rw mul_assoc },
317.   { rintros ⟨⟨a,b⟩, ⟨c,d⟩⟩ ⟨⟨i,j⟩, ⟨k,l⟩⟩ H₁ H₂,
318.     simp only [finset.mem_sigma, mem_diagonal,
319.       and_imp, prod.mk.inj_iff, add_comm, heq_iff_eq] at H₁ H₂ ⊢,
320.     finish },
321.   { rintros ⟨⟨i,j⟩, ⟨k,l⟩⟩ H, refine ⟨⟨(i+k, l), (i, k)⟩, _, _⟩;
322.     { simp only [finset.mem_sigma, mem_diagonal] at H ⊢, finish } }
323. end
324.
325. instance : comm_semiring (mv_power_series σ α) :=
326. { mul_one := mul_one,
327.   one_mul := one_mul,
332.   mul_assoc := mul_assoc,
333.   mul_zero := mul_zero,
334.   zero_mul := zero_mul,
335.   mul_comm := mul_comm,
338.   .. mv_power_series.has_zero σ α,
339.   .. mv_power_series.has_one σ α,
341.   .. mv_power_series.has_mul σ α }
342.
343. instance C.is_semiring_hom : is_semiring_hom (C : α → mv_power_series σ α) :=
344. { map_zero := C_zero _ _,
345.   map_one := C_one _ _,
347.   map_mul := C_mul }
348.
349. instance coeff.is_add_monoid_hom : is_add_monoid_hom (coeff n : mv_power_series σ α → α) :=
350. { map_zero := coeff_zero _ _ _,
352.
353. instance : semimodule α (mv_power_series σ α) :=
354. { smul := λ a φ, C a * φ,
355.   one_smul := λ φ, one_mul _,
356.   mul_smul := λ a b φ, by simp only [C_mul, mul_assoc],
358.   smul_zero := λ a, mul_zero _,
360.   zero_smul := λ φ, by simp only [zero_mul, C_zero] }
361.
362. end ring
363.
364. -- TODO(jmc): once adic topology lands, show that this is complete
365.
366. end mv_power_series
367.
368. namespace mv_power_series
369. variables {σ : Type*} {α : Type*} [decidable_eq σ] [comm_ring α]
370.
371. protected def neg (φ : mv_power_series σ α) : mv_power_series σ α := λ n, - coeff n φ
372.
373. instance : has_neg (mv_power_series σ α) := ⟨mv_power_series.neg⟩
374.
375. @[simp] lemma coeff_neg (φ : mv_power_series σ α) (n) : coeff n (- φ) = - coeff n φ := rfl
376.
377. lemma add_left_neg (φ : mv_power_series σ α) : (-φ) + φ = 0 :=
379.
380. instance : comm_ring (mv_power_series σ α) :=
382.   .. mv_power_series.has_neg, .. mv_power_series.comm_semiring }
383.
384. instance C.is_ring_hom : is_ring_hom (C : α → mv_power_series σ α) :=
385. { map_one := C_one _ _,
387.   map_mul := C_mul }
388.
389. instance coeff.is_add_group_hom (n : σ →₀ ℕ) :
390.   is_add_group_hom (coeff n : mv_power_series σ α → α) :=
392.
393. instance : module α (mv_power_series σ α) :=
394. { ..mv_power_series.semimodule }
395.
396. def inv_of_unit (φ : mv_power_series σ α) (u : units α) (h : coeff 0 φ = u) : mv_power_series σ α
397. | n := if n = 0 then ↑u⁻¹ else
398. - ↑u⁻¹ * finset.sum (n.diagonal) (λ (x : (σ →₀ ℕ) × (σ →₀ ℕ)),
399.     if h : x.1 < n then inv_of_unit x.1 * coeff x.2 φ else 0)
400. using_well_founded { rel_tac := λ _ _, `[exact ⟨_, finsupp.lt_wf σ⟩] }
401.
402. end mv_power_series
RAW Paste Data
We use cookies for various purposes including analytics. By continuing to use Pastebin, you agree to our use of cookies as described in the Cookies Policy.

Top