Irreducibility of linear and quadratic polynomials

• MvPolynomial.irreducible_of_totalDegree_eq_one: a multivariate polynomial of totalDegree one is irreducible if its coefficients are relatively prime.

• For c : n →₀ R, MvPolynomial.sumSMulX c is the linear polynomial $\sum_i c_i X_i$ of $R[X_1\dots,X_n]$.

• MvPolynomial.irreducible_sumSMulX : if the support of c is nontrivial, if R is a domain, and if the only common divisors to all c i are units, then MvPolynomial.sumSMulX c is irreducible.

• For c : n →₀ R, MvPolynomial.sumXSMulY c is the quadratic polynomial $\sum_i c_i X_i Y_i$ of $R[X_1\dots,X_n,Y_1,\dots,Y_n]$. It is constructed as an object of MvPolynomial (n ⊕ n) R, the first component of n ⊕ n represents the X indeterminates, and the second component represents the Y indeterminates.

• MvPolynomial.irreducible_sumSMulXSMulY : if the support of c is nontrivial, the ring R is a domain, and the only divisors common to all c i are units, then MvPolynomial.sumSMulXSMulY c is irreducible.

TODO

• Treat the case of diagonal quadratic polynomials, $ \sum c_i X_i ^ 2$. For irreducibility, one will need that there are at least 3 nonzero values of c, and that the only common divisors to all c i are units.

• Addition of quadratic polynomial of both kinds are relevant too.

• Prove, over a field, that a polynomial of degree at most 2 whose quadratic part has rank at least 3 is irreducible.

• Cases of ranks 1 and 2 can be treated as well, but the answer depends on the terms of degree 0 and 1. Eg, $X^2-Y$ is irreducible, but $X^2$, $X^2-1$, $X^2-Y^2$ are not. And $X^2+Y^2$ is irreducible over the reals but not over the complex numbers.

theorem MvPolynomial.irreducible_mul_X_add {n : Type u_3} {R : Type u_4} [CommRing R] [IsDomain R] (f g : MvPolynomial n R) (i : n) (hf0 : f ≠ 0) (hif : i ∉ f.vars) (hig : i ∉ g.vars) (h : IsRelPrime f g) : Irreducible (f * X i + g)

theorem MvPolynomial.irreducible_of_disjoint_support {n : Type u_1} {R : Type u_2} [CommRing R] [IsDomain R] {f : MvPolynomial n R} (nontrivial : f.support.Nontrivial) {d : n →₀ ℕ} (hd : d ∈ f.support) {i : n} (hdi : d i = 1) (disjoint : (↑f.support).PairwiseDisjoint Finsupp.support) (isPrimitive : ∀ (r : R), (∀ (d : n →₀ ℕ), r ∣ coeff d f) → IsUnit r) : Irreducible f

A multivariate polynomial f whose support is nontrivial, such that some variable i appears with exponent 1 in one nontrivial monomial, whose monomials have disjoint supports, and which is primitive, is irreducible.

The quadratic polynomial $$\sum_{i=1}^n X_i Y_i$$.

theorem MvPolynomial.irreducible_of_totalDegree_eq_one {n : Type u_1} {R : Type u_2} [CommRing R] [IsDomain R] {p : MvPolynomial n R} (hp : p.totalDegree = 1) (hp' : ∀ (x : R), (∀ (i : n →₀ ℕ), x ∣ coeff i p) → IsUnit x) : Irreducible p

noncomputable def MvPolynomial.sumSMulX {n : Type u_1} {R : Type u_2} [CommRing R] : (n →₀ R) →ₗ[R] MvPolynomial n R

The linear polynomial $$\sum_i c_i X_i$$.

Equations

• MvPolynomial.sumSMulX = Finsupp.linearCombination R MvPolynomial.X

theorem MvPolynomial.coeff_sumSMulX {n : Type u_1} {R : Type u_2} [CommRing R] (c : n →₀ R) (i : n) : coeff (Finsupp.single i 1) (sumSMulX c) = c i

theorem MvPolynomial.irreducible_sumSMulX {n : Type u_1} {R : Type u_2} [CommRing R] (c : n →₀ R) [IsDomain R] (hc_nonempty : c.support.Nonempty) (hc_gcd : ∀ (r : R), (∀ (i : n), r ∣ c i) → IsUnit r) : Irreducible (sumSMulX c)

noncomputable def MvPolynomial.sumSMulXSMulY {n : Type u_1} {R : Type u_2} [CommRing R] : (n →₀ R) →ₗ[R] MvPolynomial (n ⊕ n) R

The quadratic polynomial $$\sum_i c_i X_i Y_i$$.

Equations

• MvPolynomial.sumSMulXSMulY = Finsupp.linearCombination R fun (i : n) => MvPolynomial.X (Sum.inl i) * MvPolynomial.X (Sum.inr i)

theorem MvPolynomial.irreducible_sumSMulXSMulY {n : Type u_1} {R : Type u_2} [CommRing R] (c : n →₀ R) [IsDomain R] (hc : c.support.Nontrivial) (h_dvd : ∀ (r : R), (∀ (i : n), r ∣ c i) → IsUnit r) : Irreducible (sumSMulXSMulY c)