mv_polynomial.coeff_mul

mv_polynomial_coeff_mul.lean

/-
Copyright (c) 2019 Johan Commelin. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Johan Commelin, Kenny Lau
-/

import data.finsupp order.complete_lattice algebra.ordered_group data.mv_polynomial

namespace eq
variables {α : Type*} {a b : α}

@[reducible] def lhs (h : a = b) : α := a

@[reducible] def rhs (h : a = b) : α := b

end eq

section

set_option old_structure_cmd true

class canonically_ordered_cancel_monoid (α : Type*) extends
  ordered_cancel_comm_monoid α, canonically_ordered_monoid α.

instance : canonically_ordered_cancel_monoid ℕ :=
{ ..nat.canonically_ordered_comm_semiring,
  ..nat.decidable_linear_ordered_cancel_comm_monoid }

end

namespace multiset
variables {α : Type*} [decidable_eq α]

def to_finsupp (s : multiset α) : α →₀ ℕ :=
{ support := s.to_finset,
  to_fun := λ a, s.count a,
  mem_support_to_fun := λ a,
  begin
    rw mem_to_finset,
    convert not_iff_not_of_iff (count_eq_zero.symm),
    rw not_not
  end }

@[simp] lemma to_finsupp_support (s : multiset α) :
  s.to_finsupp.support = s.to_finset := rfl

@[simp] lemma to_finsupp_apply (s : multiset α) (a : α) :
  s.to_finsupp a = s.count a := rfl

@[simp] lemma to_finsupp_zero :
  to_finsupp (0 : multiset α) = 0 :=
finsupp.ext $ λ a, count_zero a

@[simp] lemma to_finsupp_add (s t : multiset α) :
  to_finsupp (s + t) = to_finsupp s + to_finsupp t :=
finsupp.ext $ λ a, count_add a s t

namespace to_finsupp

instance : is_add_monoid_hom (to_finsupp : multiset α → α →₀ ℕ) :=
{ map_zero := to_finsupp_zero,
  map_add  := to_finsupp_add }

end to_finsupp

@[simp] lemma to_finsupp_to_multiset (s : multiset α) :
  s.to_finsupp.to_multiset = s :=
ext.2 $ λ a, by rw [finsupp.count_to_multiset, to_finsupp_apply]

end multiset

namespace finsupp
variables {σ : Type*} {α : Type*} [decidable_eq σ]

instance [preorder α] [has_zero α] : preorder (σ →₀ α) :=
{ le := λ f g, ∀ s, f s ≤ g s,
  le_refl := λ f s, le_refl _,
  le_trans := λ f g h Hfg Hgh s, le_trans (Hfg s) (Hgh s) }

instance [partial_order α] [has_zero α] : partial_order (σ →₀ α) :=
{ le_antisymm := λ f g hfg hgf, finsupp.ext $ λ s, le_antisymm (hfg s) (hgf s),
  .. finsupp.preorder }

instance [ordered_cancel_comm_monoid α] [decidable_eq α] :
  add_left_cancel_semigroup (σ →₀ α) :=
{ add_left_cancel := λ a b c h, finsupp.ext $ λ s,
  by { rw finsupp.ext_iff at h, exact add_left_cancel (h s) },
  .. finsupp.add_monoid }

instance [ordered_cancel_comm_monoid α] [decidable_eq α] :
  add_right_cancel_semigroup (σ →₀ α) :=
{ add_right_cancel := λ a b c h, finsupp.ext $ λ s,
  by { rw finsupp.ext_iff at h, exact add_right_cancel (h s) },
  .. finsupp.add_monoid }

instance [ordered_cancel_comm_monoid α] [decidable_eq α] :
  ordered_cancel_comm_monoid (σ →₀ α) :=
{ add_le_add_left := λ a b h c s, add_le_add_left (h s) (c s),
  le_of_add_le_add_left := λ a b c h s, le_of_add_le_add_left (h s),
  .. finsupp.add_comm_monoid, .. finsupp.partial_order,
  .. finsupp.add_left_cancel_semigroup, .. finsupp.add_right_cancel_semigroup }

attribute [simp] to_multiset_zero to_multiset_add

@[simp] lemma to_multiset_to_finsupp (f : σ →₀ ℕ) :
  f.to_multiset.to_finsupp = f :=
ext $ λ s, by rw [multiset.to_finsupp_apply, count_to_multiset]

def diagonal (f : σ →₀ ℕ) : finset ((σ →₀ ℕ) × (σ →₀ ℕ)) :=
((multiset.diagonal f.to_multiset).map (prod.map multiset.to_finsupp multiset.to_finsupp)).to_finset

lemma mem_diagonal {f : σ →₀ ℕ} {p : (σ →₀ ℕ) × (σ →₀ ℕ)} :
  p ∈ diagonal f ↔ p.1 + p.2 = f :=
begin
  erw [multiset.mem_to_finset, multiset.mem_map],
  split,
  { rintros ⟨⟨a, b⟩, h, rfl⟩,
    rw multiset.mem_diagonal at h,
    simpa using congr_arg multiset.to_finsupp h },
  { intro h,
    refine ⟨⟨p.1.to_multiset, p.2.to_multiset⟩, _, _⟩,
    { simpa using congr_arg to_multiset h },
    { rw [prod.map, to_multiset_to_finsupp, to_multiset_to_finsupp, prod.mk.eta] } }
end

@[simp] lemma diagonal_zero : diagonal (0 : σ →₀ ℕ) = {(0,0)} := rfl

end finsupp

namespace mv_polynomial
open finsupp
variables {σ : Type*} {α : Type*} [decidable_eq σ] [decidable_eq α] [comm_semiring α]

lemma coeff_mul (φ ψ : mv_polynomial σ α) :
  ∀ n, coeff n (φ * ψ) = finset.sum (finsupp.diagonal n) (λ p, coeff p.1 φ * coeff p.2 ψ) :=
begin
  apply mv_polynomial.induction_on φ; clear φ,
  { apply mv_polynomial.induction_on ψ,
    { intros a b n, rw [← C_mul, coeff_C],
      split_ifs,
      { subst n, simp },
      { rw finset.sum_eq_zero, intros p hp,
        simp only [coeff_C],
        rw mem_diagonal at hp,
        split_ifs with h₁ h₂; try {simp * at *; done},
        { rw [← h₁, ← h₂, zero_add] at hp, contradiction } } },
    { intros p q hp hq a, specialize hp a, specialize hq a,
      simp [coeff_C_mul, coeff_add, mul_add, finset.sum_add_distrib, *] at * },
    { intros φ s hφ a n,
      rw [coeff_C_mul],
      have : ((0 : σ →₀ ℕ), n) ∈ diagonal n := by simp [mem_diagonal],
      rw [← finset.insert_erase this, finset.sum_insert (finset.not_mem_erase _ _),
          finset.sum_eq_zero, add_zero],
      { refl },
      { rintros ⟨i,j⟩ h,
        rw [finset.mem_erase, mem_diagonal] at h, cases h with h₁ h₂,
        by_cases H : 0 = i, { subst i, simp * at * },
        rw [coeff_C, if_neg H, zero_mul] } } },
  { intros p q hp hq n,
    rw [add_mul, coeff_add, hp, hq, ← finset.sum_add_distrib],
    apply finset.sum_congr rfl,
    intros m hm, rw [coeff_add, add_mul] },
  { intros φ s hφ n,
    conv_lhs { rw [mul_assoc, mul_comm (X s), ← mul_assoc] },
    rw coeff_mul_X',
    split_ifs,
    { symmetry,
      let T : finset (_ × _) := (diagonal n).filter (λ p, p.1 s > 0),
      have : T ⊆ diagonal n := finset.filter_subset _,
      rw [hφ, ← finset.sum_sdiff this, finset.sum_eq_zero, zero_add],
      { symmetry,
        apply finset.sum_bij (λ (p : _ × _) hp, (p.1 + single s 1, p.2)),
        { rintros ⟨i,j⟩ hij, rw [mem_diagonal] at hij,
          rw [finset.mem_filter, mem_diagonal], dsimp at *,
          split,
          { rw [add_right_comm, hij_1],
            ext t, by_cases hst : s = t,
            { subst t, apply nat.sub_add_cancel, rw [single_apply, if_pos rfl],
              apply nat.pos_of_ne_zero, rwa mem_support_iff at h },
            { change _ - _ + _ = _, simp [single_apply, hst] } },
          { apply nat.add_pos_right, rw [single_apply, if_pos rfl], exact nat.one_pos } },
        { rintros ⟨i,j⟩ hij, rw coeff_mul_X', split_ifs with H,
          { congr' 2, ext t, exact (nat.add_sub_cancel _ _).symm },
          { exfalso, apply H, rw [mem_support_iff, add_apply, single_apply, if_pos rfl],
            exact nat.succ_ne_zero _ } },
        { rintros ⟨i,j⟩ ⟨k,l⟩ hij hkl, rw [prod.mk.inj_iff, add_right_inj, ← prod.mk.inj_iff],
          exact id },
        { rintros ⟨i,j⟩ hij, rw finset.mem_filter at hij, cases hij with h₁ h₂,
          refine ⟨(i - single s 1, j), _, _⟩,
          { rw mem_diagonal at h₁ ⊢, rw ← h₁, ext t, by_cases hst: s = t,
            { subst t, apply (nat.sub_add_comm _).symm,
              rwa [single_apply, if_pos rfl] },
            { apply (nat.sub_add_comm _).symm,
              simp [single_apply, hst] } },
          { congr, ext t, by_cases hst: s = t,
            { subst t, apply (nat.sub_add_cancel _).symm, rwa [single_apply, if_pos rfl] },
            { change _ = _ - _ + _, simp [single_apply, hst] } } } },
      { rintros ⟨i,j⟩ hij, rw finset.mem_sdiff at hij, cases hij with h₁ h₂,
        rw coeff_mul_X', split_ifs with H,
        { exfalso, apply h₂, rw finset.mem_filter, refine ⟨h₁, nat.pos_of_ne_zero _⟩,
          rwa mem_support_iff at H },
        { exact zero_mul _ } } },
    { rw finset.sum_eq_zero,
      rintros ⟨i,j⟩ hij,
      rw [coeff_mul_X', if_neg, zero_mul],
      intro H, apply h,
      rw mem_support_iff at H ⊢,
      rw mem_diagonal at hij,
      rw ← hij, simp * at * } }
end