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,
  35.   map_add  := to_finsupp_add }
  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) },
  61.   .. finsupp.add_monoid }
  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) },
  67.   .. finsupp.add_monoid }
  68.  
  69. instance [ordered_cancel_comm_monoid α] [decidable_eq α] :
  70.   ordered_cancel_comm_monoid (σ →₀ α) :=
  71. { add_le_add_left := λ a b h c s, add_le_add_left (h s) (c s),
  72.   le_of_add_le_add_left := λ a b c h s, le_of_add_le_add_left (h s),
  73.   .. finsupp.add_comm_monoid, .. finsupp.partial_order,
  74.   .. finsupp.add_left_cancel_semigroup, .. finsupp.add_right_cancel_semigroup }
  75.  
  76. attribute [simp] to_multiset_zero to_multiset_add
  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.  
  216. instance : has_add (mv_power_series σ α) := ⟨add σ α⟩
  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 :=
  237. monomial_add 0 a 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 _ _),
  280.     coeff_one_zero, one_mul, finset.sum_eq_zero, _root_.add_zero],
  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.   φ₁ * (φ₂ + φ₃) = φ₁ * φ₂ + φ₁ * φ₃ :=
  292. ext $ λ n, by simp only [coeff_mul, coeff_add, mul_add, finset.sum_add_distrib]
  293.  
  294. lemma add_mul (φ₁ φ₂ φ₃ : mv_power_series σ α) :
  295.   (φ₁ + φ₂) * φ₃ = φ₁ * φ₃ + φ₂ * φ₃ :=
  296. ext $ λ n, by simp only [coeff_mul, coeff_add, add_mul, finset.sum_add_distrib]
  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,
  328.   add_assoc := add_assoc,
  329.   zero_add := zero_add,
  330.   add_zero := add_zero,
  331.   add_comm := add_comm,
  332.   mul_assoc := mul_assoc,
  333.   mul_zero := mul_zero,
  334.   zero_mul := zero_mul,
  335.   mul_comm := mul_comm,
  336.   left_distrib := mul_add,
  337.   right_distrib := add_mul,
  338.   .. mv_power_series.has_zero σ α,
  339.   .. mv_power_series.has_one σ α,
  340.   .. mv_power_series.has_add σ α,
  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 _ _,
  346.   map_add := C_add,
  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 _ _ _,
  351.   map_add := coeff_add n }
  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],
  357.   smul_add := λ a φ ψ, mul_add _ _ _,
  358.   smul_zero := λ a, mul_zero _,
  359.   add_smul := λ a b φ, by simp only [C_add, add_mul],
  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 :=
  378. ext $ λ n, by rw [coeff_add, coeff_zero, coeff_neg, add_left_neg]
  379.  
  380. instance : comm_ring (mv_power_series σ α) :=
  381. { add_left_neg := add_left_neg,
  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 _ _,
  386.   map_add := C_add,
  387.   map_mul := C_mul }
  388.  
  389. instance coeff.is_add_group_hom (n : σ →₀ ℕ) :
  390.   is_add_group_hom (coeff n : mv_power_series σ α → α) :=
  391. { map_add := coeff_add n }
  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. OK, I Understand
 
Top