MvPolynomial_relation_mem_span_of_forall_isHomogeneous_mem_span.lean

theorem decompose_eq (q : MvPolynomial (Fin (n + 1)) L) (d : ℕ) :
    (DirectSum.decompose (homogeneousSubmodule (Fin (n + 1)) L) q d : MvPolynomial (Fin (n + 1)) L)
      =
      homogeneousComponent d q

theorem homogeneousComponent_mul_add {G : MvPolynomial (Fin (n + 1)) L} {m : ℕ} (hG :
  G.IsHomogeneous m)
    (a : MvPolynomial (Fin (n + 1)) L) (d : ℕ) :
    homogeneousComponent (m + d) (a * G) = homogeneousComponent d a * G

theorem exists_eq_sum_X_mul (k : ℕ) (g : MvPolynomial (Fin (n + 1)) L) (hg : g.IsHomogeneous (k +
  1)) :
    ∃ q : Fin (n + 1) → MvPolynomial (Fin (n + 1)) L, (∀ i, (q i).IsHomogeneous k) ∧ g = ∑ i, X i *
      q i

theorem exists_eq_sum_mul_of_span {N q : ℕ} (u : Fin N → MvPolynomial (Fin (n + 1)) L)
    (hspan : ∀ w : MvPolynomial (Fin (n + 1)) L, w.IsHomogeneous q → w ∈ Submodule.span L
      (Set.range u)) :
    ∀ (p : ℕ) (w : MvPolynomial (Fin (n + 1)) L), w.IsHomogeneous (q + p) →
      ∃ d : Fin N → MvPolynomial (Fin (n + 1)) L, (∀ j, (d j).IsHomogeneous p) ∧ w = ∑ j, d j * u j
  | 0, w, hw => by
      obtain ⟨κ, hκ⟩ := (Submodule.mem_span_range_iff_exists_fun L).mp (hspan w hw)
      refine ⟨fun j => C (κ j), fun j => isHomogeneous_C _ _, ?_⟩
      rw [← hκ]; exact Finset.sum_congr rfl fun j _ => by rw [smul_eq_C_mul]
  | p + 1, w, hw => by
      obtain ⟨r, hr, rfl⟩ := exists_eq_sum_X_mul (q + p) w hw
      have ih := fun i => exists_eq_sum_mul_of_span u hspan p (r i) (hr i)
      choose d hd hrd using ih
      refine ⟨fun j => ∑ i, X i * d i j, fun j => IsHomogeneous.sum _ _ _ fun i _ => ?_, ?_⟩
      · have := (isHomogeneous_X L i).mul (hd i j); rwa [Nat.add_comm 1 p] at this
      · calc ∑ i, X i * r i = ∑ i, ∑ j, X i * d i j * u j := Finset.sum_congr rfl fun i _ => by
              rw [hrd i, Finset.mul_sum]; exact Finset.sum_congr rfl fun j _ => by rw [mul_assoc]
          _ = ∑ j, (∑ i, X i * d i j) * u j := by
              rw [Finset.sum_comm]; exact Finset.sum_congr rfl fun j _ => by rw [Finset.sum_mul]

theorem sum_sum_eq_zero_of_alternating {M : Type} [AddCommGroup M] {N : ℕ} (f : Fin N → Fin N → M)
    (hskew : ∀ ν μ, f ν μ = -f μ ν) (hdiag : ∀ ν, f ν ν = 0) : ∑ ν, ∑ μ, f ν μ = 0

theorem main (m g : ℕ) (F : Fin g → MvPolynomial (Fin (n + 1)) L) (hF : ∀ i, (F i).IsHomogeneous m)
    (hspan : ∀ w : MvPolynomial (Fin (n + 1)) L, w.IsHomogeneous m → w ∈ Submodule.span L
      (Set.range F)) :
    ∀ (d : ℕ) (c : Fin g → MvPolynomial (Fin (n + 1)) L), (∀ i, (c i).IsHomogeneous d) →
      ∑ i, c i * F i = 0 →
      c ∈ Submodule.span (MvPolynomial (Fin (n + 1)) L)
        {l : Fin g → MvPolynomial (Fin (n + 1)) L | (∃ d' ≤ 1, ∀ i, (l i).IsHomogeneous d') ∧ ∑ i,
          l i * F i = 0}

theorem _root_.MvPolynomial.relation_mem_span_of_forall_isHomogeneous_mem_span
    (n m g : ℕ) (K : Type) [Field K] (F : Fin g → MvPolynomial (Fin (n + 1)) K)
    (hF : ∀ i, (F i).IsHomogeneous m)
    (hspan : ∀ w : MvPolynomial (Fin (n + 1)) K, w.IsHomogeneous m → w ∈ Submodule.span K
      (Set.range F))
    (d : ℕ) (c : Fin g → MvPolynomial (Fin (n + 1)) K) (hc : ∀ i, (c i).IsHomogeneous d)
    (hcF : ∑ i, c i * F i = 0) :
    c ∈ Submodule.span (MvPolynomial (Fin (n + 1)) K)
      {l : Fin g → MvPolynomial (Fin (n + 1)) K |
        (∃ d' ≤ 1, ∀ i, (l i).IsHomogeneous d') ∧ ∑ i, l i * F i = 0}