Partial fraction decomposition

Stream: general

[Daniel Weber]

I know there are some results about partial fraction decomposition in file#Mathlib/Algebra/Polynomial/PartialFractions, but I need something stronger. I'm not sure about a nice way to state it, though. Currently I have

import Mathlib

set_option autoImplicit false

open Polynomial algebraMap

namespace PartialFraction

variable (R : Type) [CommRing R] [IsDomain R] [DecidableEq R]
variable (K : Type) [Field K] [Algebra R[X] K] [IsFractionRing R[X] K] [DecidableEq K]

noncomputable instance (n : ℕ) : Zero {p : R[X] // p.degree < n} where
  zero := ⟨0, (degree_zero (R := R)).symm ▸ WithBot.bot_lt_coe n⟩

noncomputable instance (n : ℕ) : Add {p : R[X] // p.degree < n} where
  add (x y) := ⟨x + y, Polynomial.degree_add_le x.1 y.1 |>.trans_lt <| max_lt x.2 y.2⟩

noncomputable instance (n : ℕ) : Neg {p : R[X] // p.degree < n} where
  neg (x) := ⟨-x, (degree_neg x.1).symm ▸ x.2⟩

noncomputable instance (n : ℕ) : AddCommGroup {p : R[X] // p.degree < n} where
  add_assoc (_ _ _) := Subtype.ext <| add_assoc ..
  add_comm (_ _) := Subtype.ext <| add_comm ..
  add_zero (_) := Subtype.ext <| add_zero _
  zero_add (_) := Subtype.ext <| zero_add _
  nsmul := nsmulRec
  zsmul := zsmulRec
  add_left_neg (_) := Subtype.ext <| add_left_neg _

@[norm_cast]
lemma degRes.coe_add (n : ℕ) (x y : {p : R[X] // p.degree < n}) : ((x + y : {p : R[X] // p.degree < n}) : R[X]) = (x : R[X]) + (y : R[X]) := by
  rfl

noncomputable def partialFracEquiv :
    R[X] × (Π₀ h : {p : R[X] // Irreducible p} × ℕ+, {q : R[X] // q.degree < h.1.val.natDegree}) ≃+ K where
  toFun (h) := h.1 + h.2.sum fun h q ↦ q.val / (h.1.val ^ h.2.val : K)
  invFun := sorry
  left_inv := sorry
  right_inv := sorry
  map_add' (x y) := by
    dsimp only [Equiv.toFun_as_coe, Equiv.coe_fn_mk, Prod.fst_add, Prod.snd_add]
    rw [DFinsupp.sum_add_index]
    · push_cast
      abel
    · intro
      simp only [_root_.div_eq_zero_iff, pow_eq_zero_iff', ne_eq]
      left
      norm_cast
    · intros
      push_cast
      apply add_div

I'm ok with the sorrys, I'll be able to fill them, but the statement is quite ugly. Is there a better way to state this, without so many subtypes?

[Kim Morrison]

Wouldn't it be better to build an AddSubgroup R[X] for the bounded degree polynomials, rather than the subtype?

[Daniel Weber]

Kim Morrison said:

Wouldn't it be better to build an AddSubgroup R[X] for the bounded degree polynomials, rather than the subtype?

Sounds like a good idea, thanks

[Kim Morrison]

Why are you using Π₀ rather than just say a Finset of tuples?

[Kim Morrison]

Before embarking on the \equiv you should give a name to the LHS, and define the functions in each direction as separate declarations.

[Daniel Weber]

Kim Morrison said:

Why are you using Π₀ rather than just say a Finset of tuples?

In a Finset of tuples I don't think I get addition for free

[Daniel Weber]

Maybe this could be better stated as a docs#Basis ? EDIT: no, that wouldn't work, as the coefficients are restricted. But it can still be a linear equivalence