div — Mathlib

English

Given a finite set B of mv polynomials whose leading coefficients are units, any polynomial f can be written as a finite linear combination of the polynomials in B plus a remainder r with controlled degrees, i.e., f = sum_b b g_b + r with suitable g_b and r obeying degree and support restrictions.

Русский

Дано множество B mv-полиномов с единичными ведущими коэффициентами; любой f можно разложить как линейную комбинацию элементов B плюс остаток r с ограниченными степенями и поддержкой.

LaTeX

$$$\\exists g : B \\to_0 \\mathrm{MvPolynomial}_{\\sigma,R},\\; \\exists r : \\mathrm{MvPolynomial}_{\\sigma,R},\\ f = \\sum_{b \\in B} b \\cdot g(b) + r \\\\ ∧\\ (\\forall b, m.deg(b) \\cdot g(b) \\preceq_m m.\\deg f) \\∧ (\\forall c \\in r.\\mathrm{support}, \\forall b, b \\in B, \\neg (m.\\deg b \\le c))$$$

Lean4

/-- Division by a family of multivariate polynomials
whose leading coefficients are invertible with respect to a monomial order -/
theorem div {ι : Type*} {b : ι → MvPolynomial σ R} (hb : ∀ i, IsUnit (m.leadingCoeff (b i))) (f : MvPolynomial σ R) :
    ∃ (g : ι →₀ (MvPolynomial σ R)) (r : MvPolynomial σ R),
      f = Finsupp.linearCombination _ b g + r ∧
        (∀ i, m.degree (b i * (g i)) ≼[m] m.degree f) ∧ (∀ c ∈ r.support, ∀ i, ¬(m.degree (b i) ≤ c)) :=
  by
  by_cases hb' : ∃ i, m.degree (b i) = 0
  · obtain ⟨i, hb0⟩ := hb'
    use Finsupp.single i ((hb i).unit⁻¹ • f), 0
    constructor
    · simp only [Finsupp.linearCombination_single, smul_eq_mul, add_zero]
      simp only [smul_mul_assoc, ← smul_eq_iff_eq_inv_smul, Units.smul_isUnit]
      nth_rewrite 2 [eq_C_of_degree_eq_zero hb0]
      rw [mul_comm, smul_eq_C_mul]
    constructor
    · intro j
      by_cases hj : j = i
      · apply le_trans degree_mul_le
        simp only [hj, hb0, Finsupp.single_eq_same, zero_add]
        apply le_of_eq
        simp only [EmbeddingLike.apply_eq_iff_eq]
        apply degree_smul (Units.isRegular _)
      · simp only [Finsupp.single_eq_of_ne hj, mul_zero, degree_zero, map_zero]
        apply bot_le
    · simp
  push_neg at hb'
  by_cases hf0 : f = 0
  · refine ⟨0, 0, by simp [hf0], ?_, by simp⟩
    intro b
    simp only [Finsupp.coe_zero, Pi.zero_apply, mul_zero, degree_zero, map_zero]
    exact bot_le
  by_cases hf : ∃ i, m.degree (b i) ≤ m.degree f
  · obtain ⟨i, hf⟩ := hf
    have deg_reduce : m.degree (m.reduce (hb i) f) ≺[m] m.degree f :=
      by
      apply degree_reduce_lt (hb i) hf
      intro hf0'
      apply hb' i
      simpa [hf0'] using hf
    obtain ⟨g', r', H'⟩ := div hb (m.reduce (hb i) f)
    use g' + Finsupp.single i (monomial (m.degree f - m.degree (b i)) ((hb i).unit⁻¹ * m.leadingCoeff f))
    use r'
    constructor
    · rw [map_add, add_assoc, add_comm _ r', ← add_assoc, ← H'.1]
      simp [reduce]
    constructor
    · rintro j
      simp only [Finsupp.coe_add, Pi.add_apply]
      rw [mul_add]
      apply le_trans degree_add_le
      simp only [sup_le_iff]
      constructor
      · exact le_trans (H'.2.1 _) (le_of_lt deg_reduce)
      ·
        classical
        rw [Finsupp.single_apply]
        split_ifs with hc
        · apply le_trans degree_mul_le
          simp only [map_add]
          apply le_of_le_of_eq (add_le_add_left (degree_monomial_le _) _)
          simp only [← hc]
          rw [← map_add, m.toSyn.injective.eq_iff]
          rw [add_tsub_cancel_of_le]
          exact hf
        · simp only [mul_zero, degree_zero, map_zero]
          exact bot_le
    · exact H'.2.2
  · push_neg at hf
    suffices
      ∃ (g' : ι →₀ MvPolynomial σ R),
        ∃ r',
          (m.subLTerm f = Finsupp.linearCombination (MvPolynomial σ R) b g' + r') ∧
            (∀ i, m.degree ((b i) * (g' i)) ≼[m] m.degree (m.subLTerm f)) ∧ (∀ c ∈ r'.support, ∀ i, ¬m.degree (b i) ≤ c)
      by
      obtain ⟨g', r', H'⟩ := this
      use g', r' + monomial (m.degree f) (m.leadingCoeff f)
      constructor
      · simp [← add_assoc, ← H'.1, subLTerm]
      constructor
      · exact fun b ↦ le_trans (H'.2.1 b) (degree_sub_LTerm_le f)
      · intro c hc i
        by_cases hc' : c ∈ r'.support
        · exact H'.2.2 c hc' i
        · convert hf i
          classical
          have := MvPolynomial.support_add hc
          rw [Finset.mem_union, Classical.or_iff_not_imp_left] at this
          simpa only [Finset.mem_singleton] using support_monomial_subset (this hc')
    by_cases hf'0 : m.subLTerm f = 0
    · refine ⟨0, 0, by simp [hf'0], ?_, by simp⟩
      intro b
      simp only [Finsupp.coe_zero, Pi.zero_apply, mul_zero, degree_zero, map_zero]
      exact bot_le
    · exact (div hb) (m.subLTerm f)
termination_by WellFounded.wrap ((isWellFounded_iff m.syn fun x x_1 ↦ x < x_1).mp m.wf) (m.toSyn (m.degree f))
decreasing_by
  · exact deg_reduce
  · apply degree_sub_LTerm_lt
    intro hf0
    apply hf'0
    simp only [subLTerm, sub_eq_zero]
    nth_rewrite 1 [eq_C_of_degree_eq_zero hf0, hf0]
    simp

Похожие утверждения