Documentation

Mathlib.RingTheory.MvPolynomial.Homogeneous

Homogeneous polynomials #

A multivariate polynomial φ is homogeneous of degree n if all monomials occurring in φ have degree n.

Main definitions/lemmas #

def MvPolynomial.degree {σ : Type u_1} (d : σ →₀ ) :

The degree of a monomial.

Equations
Instances For
    def MvPolynomial.IsHomogeneous {σ : Type u_1} {R : Type u_3} [CommSemiring R] (φ : MvPolynomial σ R) (n : ) :

    A multivariate polynomial φ is homogeneous of degree n if all monomials occurring in φ have degree n.

    Equations
    Instances For
      theorem MvPolynomial.weightedTotalDegree_one {σ : Type u_1} {R : Type u_3} [CommSemiring R] (φ : MvPolynomial σ R) :

      The submodule of homogeneous MvPolynomials of degree n.

      Equations
      Instances For
        @[simp]
        theorem MvPolynomial.mem_homogeneousSubmodule {σ : Type u_1} {R : Type u_3} [CommSemiring R] (n : ) (p : MvPolynomial σ R) :
        p MvPolynomial.homogeneousSubmodule σ R n p.IsHomogeneous n

        While equal, the former has a convenient definitional reduction.

        theorem MvPolynomial.isHomogeneous_monomial {σ : Type u_1} {R : Type u_3} [CommSemiring R] {d : σ →₀ } (r : R) {n : } (hn : MvPolynomial.degree d = n) :
        ((MvPolynomial.monomial d) r).IsHomogeneous n
        theorem MvPolynomial.totalDegree_zero_iff_isHomogeneous (σ : Type u_1) {R : Type u_3} [CommSemiring R] {p : MvPolynomial σ R} :
        p.totalDegree = 0 p.IsHomogeneous 0
        theorem MvPolynomial.isHomogeneous_of_totalDegree_zero (σ : Type u_1) {R : Type u_3} [CommSemiring R] {p : MvPolynomial σ R} :
        p.totalDegree = 0p.IsHomogeneous 0

        Alias of the forward direction of MvPolynomial.totalDegree_zero_iff_isHomogeneous.

        theorem MvPolynomial.isHomogeneous_C (σ : Type u_1) {R : Type u_3} [CommSemiring R] (r : R) :
        (MvPolynomial.C r).IsHomogeneous 0
        theorem MvPolynomial.isHomogeneous_X {σ : Type u_1} (R : Type u_3) [CommSemiring R] (i : σ) :
        (MvPolynomial.X i).IsHomogeneous 1
        theorem MvPolynomial.IsHomogeneous.coeff_eq_zero {σ : Type u_1} {R : Type u_3} [CommSemiring R] {φ : MvPolynomial σ R} {n : } (hφ : φ.IsHomogeneous n) {d : σ →₀ } (hd : MvPolynomial.degree d n) :
        theorem MvPolynomial.IsHomogeneous.inj_right {σ : Type u_1} {R : Type u_3} [CommSemiring R] {φ : MvPolynomial σ R} {m : } {n : } (hm : φ.IsHomogeneous m) (hn : φ.IsHomogeneous n) (hφ : φ 0) :
        m = n
        theorem MvPolynomial.IsHomogeneous.add {σ : Type u_1} {R : Type u_3} [CommSemiring R] {φ : MvPolynomial σ R} {ψ : MvPolynomial σ R} {n : } (hφ : φ.IsHomogeneous n) (hψ : ψ.IsHomogeneous n) :
        (φ + ψ).IsHomogeneous n
        theorem MvPolynomial.IsHomogeneous.sum {σ : Type u_1} {R : Type u_3} [CommSemiring R] {ι : Type u_5} (s : Finset ι) (φ : ιMvPolynomial σ R) (n : ) (h : is, (φ i).IsHomogeneous n) :
        (is, φ i).IsHomogeneous n
        theorem MvPolynomial.IsHomogeneous.mul {σ : Type u_1} {R : Type u_3} [CommSemiring R] {φ : MvPolynomial σ R} {ψ : MvPolynomial σ R} {m : } {n : } (hφ : φ.IsHomogeneous m) (hψ : ψ.IsHomogeneous n) :
        (φ * ψ).IsHomogeneous (m + n)
        theorem MvPolynomial.IsHomogeneous.prod {σ : Type u_1} {R : Type u_3} [CommSemiring R] {ι : Type u_5} (s : Finset ι) (φ : ιMvPolynomial σ R) (n : ι) (h : is, (φ i).IsHomogeneous (n i)) :
        (is, φ i).IsHomogeneous (is, n i)
        theorem MvPolynomial.IsHomogeneous.C_mul {σ : Type u_1} {R : Type u_3} [CommSemiring R] {φ : MvPolynomial σ R} {m : } (hφ : φ.IsHomogeneous m) (r : R) :
        (MvPolynomial.C r * φ).IsHomogeneous m
        theorem MvPolynomial.isHomogeneous_C_mul_X {σ : Type u_1} {R : Type u_3} [CommSemiring R] (r : R) (i : σ) :
        (MvPolynomial.C r * MvPolynomial.X i).IsHomogeneous 1
        @[deprecated MvPolynomial.isHomogeneous_C_mul_X]
        theorem MvPolynomial.C_mul_X {σ : Type u_1} {R : Type u_3} [CommSemiring R] (r : R) (i : σ) :
        (MvPolynomial.C r * MvPolynomial.X i).IsHomogeneous 1

        Alias of MvPolynomial.isHomogeneous_C_mul_X.

        theorem MvPolynomial.IsHomogeneous.pow {σ : Type u_1} {R : Type u_3} [CommSemiring R] {φ : MvPolynomial σ R} {m : } (hφ : φ.IsHomogeneous m) (n : ) :
        (φ ^ n).IsHomogeneous (m * n)
        theorem MvPolynomial.isHomogeneous_X_pow {σ : Type u_1} {R : Type u_3} [CommSemiring R] (i : σ) (n : ) :
        (MvPolynomial.X i ^ n).IsHomogeneous n
        theorem MvPolynomial.isHomogeneous_C_mul_X_pow {σ : Type u_1} {R : Type u_3} [CommSemiring R] (r : R) (i : σ) (n : ) :
        (MvPolynomial.C r * MvPolynomial.X i ^ n).IsHomogeneous n
        theorem MvPolynomial.IsHomogeneous.eval₂ {σ : Type u_1} {τ : Type u_2} {R : Type u_3} {S : Type u_4} [CommSemiring R] [CommSemiring S] {φ : MvPolynomial σ R} {m : } {n : } (hφ : φ.IsHomogeneous m) (f : R →+* MvPolynomial τ S) (g : σMvPolynomial τ S) (hf : ∀ (r : R), (f r).IsHomogeneous 0) (hg : ∀ (i : σ), (g i).IsHomogeneous n) :
        (MvPolynomial.eval₂ f g φ).IsHomogeneous (n * m)
        theorem MvPolynomial.IsHomogeneous.map {σ : Type u_1} {R : Type u_3} {S : Type u_4} [CommSemiring R] [CommSemiring S] {φ : MvPolynomial σ R} {n : } (hφ : φ.IsHomogeneous n) (f : R →+* S) :
        ((MvPolynomial.map f) φ).IsHomogeneous n
        theorem MvPolynomial.IsHomogeneous.aeval {σ : Type u_1} {τ : Type u_2} {R : Type u_3} {S : Type u_4} [CommSemiring R] [CommSemiring S] {φ : MvPolynomial σ R} {m : } {n : } [Algebra R S] (hφ : φ.IsHomogeneous m) (g : σMvPolynomial τ S) (hg : ∀ (i : σ), (g i).IsHomogeneous n) :
        ((MvPolynomial.aeval g) φ).IsHomogeneous (n * m)
        theorem MvPolynomial.IsHomogeneous.neg {R : Type u_5} {σ : Type u_6} [CommRing R] {φ : MvPolynomial σ R} {n : } (hφ : φ.IsHomogeneous n) :
        (-φ).IsHomogeneous n
        theorem MvPolynomial.IsHomogeneous.sub {R : Type u_5} {σ : Type u_6} [CommRing R] {φ : MvPolynomial σ R} {ψ : MvPolynomial σ R} {n : } (hφ : φ.IsHomogeneous n) (hψ : ψ.IsHomogeneous n) :
        (φ - ψ).IsHomogeneous n
        theorem MvPolynomial.IsHomogeneous.totalDegree_le {σ : Type u_1} {R : Type u_3} [CommSemiring R] {φ : MvPolynomial σ R} {n : } (hφ : φ.IsHomogeneous n) :
        φ.totalDegree n

        The homogeneous degree bounds the total degree.

        See also MvPolynomial.IsHomogeneous.totalDegree when φ is non-zero.

        theorem MvPolynomial.IsHomogeneous.totalDegree {σ : Type u_1} {R : Type u_3} [CommSemiring R] {φ : MvPolynomial σ R} {n : } (hφ : φ.IsHomogeneous n) (h : φ 0) :
        φ.totalDegree = n
        theorem MvPolynomial.IsHomogeneous.rename_isHomogeneous {σ : Type u_1} {τ : Type u_2} {R : Type u_3} [CommSemiring R] {φ : MvPolynomial σ R} {n : } {f : στ} (h : φ.IsHomogeneous n) :
        ((MvPolynomial.rename f) φ).IsHomogeneous n
        theorem MvPolynomial.IsHomogeneous.rename_isHomogeneous_iff {σ : Type u_1} {τ : Type u_2} {R : Type u_3} [CommSemiring R] {φ : MvPolynomial σ R} {n : } {f : στ} (hf : Function.Injective f) :
        ((MvPolynomial.rename f) φ).IsHomogeneous n φ.IsHomogeneous n
        theorem MvPolynomial.IsHomogeneous.finSuccEquiv_coeff_isHomogeneous {R : Type u_3} [CommSemiring R] {N : } {φ : MvPolynomial (Fin (N + 1)) R} {n : } (hφ : φ.IsHomogeneous n) (i : ) (j : ) (h : i + j = n) :
        (((MvPolynomial.finSuccEquiv R N) φ).coeff i).IsHomogeneous j
        theorem MvPolynomial.IsHomogeneous.coeff_isHomogeneous_of_optionEquivLeft_symm {σ : Type u_1} {R : Type u_3} [CommSemiring R] {n : } [hσ : Finite σ] {p : Polynomial (MvPolynomial σ R)} (hp : ((MvPolynomial.optionEquivLeft R σ).symm p).IsHomogeneous n) (i : ) (j : ) (h : i + j = n) :
        (p.coeff i).IsHomogeneous j
        theorem MvPolynomial.IsHomogeneous.eq_zero_of_forall_eval_eq_zero_of_le_card {R : Type u_5} {σ : Type u_6} [CommRing R] [IsDomain R] {F : MvPolynomial σ R} {n : } (hF : F.IsHomogeneous n) (h : ∀ (r : σR), (MvPolynomial.eval r) F = 0) (hnR : n Cardinal.mk R) :
        F = 0

        See MvPolynomial.IsHomogeneous.eq_zero_of_forall_eval_eq_zero for a version that assumes Infinite R.

        theorem MvPolynomial.IsHomogeneous.funext_of_le_card {R : Type u_5} {σ : Type u_6} [CommRing R] [IsDomain R] {F : MvPolynomial σ R} {G : MvPolynomial σ R} {n : } (hF : F.IsHomogeneous n) (hG : G.IsHomogeneous n) (h : ∀ (r : σR), (MvPolynomial.eval r) F = (MvPolynomial.eval r) G) (hnR : n Cardinal.mk R) :
        F = G

        See MvPolynomial.IsHomogeneous.funext for a version that assumes Infinite R.

        theorem MvPolynomial.IsHomogeneous.eq_zero_of_forall_eval_eq_zero {R : Type u_5} {σ : Type u_6} [CommRing R] [IsDomain R] [Infinite R] {F : MvPolynomial σ R} {n : } (hF : F.IsHomogeneous n) (h : ∀ (r : σR), (MvPolynomial.eval r) F = 0) :
        F = 0

        See MvPolynomial.IsHomogeneous.eq_zero_of_forall_eval_eq_zero_of_le_card for a version that assumes n ≤ #R.

        theorem MvPolynomial.IsHomogeneous.funext {R : Type u_5} {σ : Type u_6} [CommRing R] [IsDomain R] [Infinite R] {F : MvPolynomial σ R} {G : MvPolynomial σ R} {n : } (hF : F.IsHomogeneous n) (hG : G.IsHomogeneous n) (h : ∀ (r : σR), (MvPolynomial.eval r) F = (MvPolynomial.eval r) G) :
        F = G

        See MvPolynomial.IsHomogeneous.funext_of_le_card for a version that assumes n ≤ #R.

        The homogeneous submodules form a graded ring. This instance is used by DirectSum.commSemiring and DirectSum.algebra.

        Equations
        • =

        homogeneousComponent n φ is the part of φ that is homogeneous of degree n. See sum_homogeneousComponent for the statement that φ is equal to the sum of all its homogeneous components.

        Equations
        Instances For
          theorem MvPolynomial.homogeneousComponent_isHomogeneous {σ : Type u_1} {R : Type u_3} [CommSemiring R] (n : ) (φ : MvPolynomial σ R) :
          ((MvPolynomial.homogeneousComponent n) φ).IsHomogeneous n
          @[simp]
          theorem MvPolynomial.homogeneousComponent_zero {σ : Type u_1} {R : Type u_3} [CommSemiring R] (φ : MvPolynomial σ R) :
          @[simp]
          theorem MvPolynomial.homogeneousComponent_C_mul {σ : Type u_1} {R : Type u_3} [CommSemiring R] (φ : MvPolynomial σ R) (n : ) (r : R) :
          (MvPolynomial.homogeneousComponent n) (MvPolynomial.C r * φ) = MvPolynomial.C r * (MvPolynomial.homogeneousComponent n) φ
          theorem MvPolynomial.homogeneousComponent_eq_zero' {σ : Type u_1} {R : Type u_3} [CommSemiring R] (n : ) (φ : MvPolynomial σ R) (h : dφ.support, MvPolynomial.degree d n) :
          theorem MvPolynomial.homogeneousComponent_eq_zero {σ : Type u_1} {R : Type u_3} [CommSemiring R] (n : ) (φ : MvPolynomial σ R) (h : φ.totalDegree < n) :
          theorem MvPolynomial.sum_homogeneousComponent {σ : Type u_1} {R : Type u_3} [CommSemiring R] (φ : MvPolynomial σ R) :
          iFinset.range (φ.totalDegree + 1), (MvPolynomial.homogeneousComponent i) φ = φ