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.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 : d.degree = n) :
      ((MvPolynomial.monomial d) r).IsHomogeneous n
      theorem MvPolynomial.totalDegree_eq_zero_iff (σ : Type u_1) {R : Type u_3} [CommSemiring R] (p : MvPolynomial σ R) :
      p.totalDegree = 0 mp.support, ∀ (x : σ), m x = 0
      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 : d.degree 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.coeff_homogeneousComponent {σ : Type u_1} {R : Type u_3} [CommSemiring R] (n : ) (φ : MvPolynomial σ R) (d : σ →₀ ) :
        theorem MvPolynomial.homogeneousComponent_apply {σ : Type u_1} {R : Type u_3} [CommSemiring R] (n : ) (φ : MvPolynomial σ R) :
        (MvPolynomial.homogeneousComponent n) φ = dFinset.filter (fun (d : σ →₀ ) => d.degree = n) φ.support, (MvPolynomial.monomial d) (MvPolynomial.coeff d φ)
        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, d.degree 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) φ = φ
        theorem MvPolynomial.homogeneousComponent_of_mem {σ : Type u_1} {R : Type u_3} [CommSemiring R] {m : } {n : } {p : MvPolynomial σ R} (h : p MvPolynomial.homogeneousSubmodule σ R n) :
        (MvPolynomial.homogeneousComponent m) p = if m = n then p else 0

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

        @[reducible, inline]

        The decomposition of MvPolynomial σ R into homogeneous submodules.

        Equations
        Instances For
          @[reducible, inline]

          MvPolynomial σ R as a graded algebra, graded by the degree. We do not make this a global instance because one may want to consider a different graded algebra structure on MvPolynomial σ R, induced by another weight function. To make it a local instance, you may use attribute [local instance] MvPolynomial.gradedAlgebra.

          Equations
          Instances For
            theorem MvPolynomial.decomposition.decompose'_eq {σ : Type u_1} {R : Type u_3} [CommSemiring R] :
            DirectSum.Decomposition.decompose' = fun (φ : MvPolynomial σ R) => (DirectSum.mk (fun (i : ) => (MvPolynomial.homogeneousSubmodule σ R i)) (Finset.image Finsupp.degree φ.support)) fun (m : (Finset.image Finsupp.degree φ.support)) => (MvPolynomial.homogeneousComponent m) φ,