Dimension of homogeneous polynomials

The monomial basis of a homogeneous component is indexed by exponent vectors of its degree. For two variables this gives dimension w + 1, used for the scalar-matrix trace on binary forms. Changing the coefficients along a ring homomorphism, TauCeti.mapHomogeneousSubmodule, is semilinear and sends this basis to the monomial basis over the new ring.

instance TauCeti.homogeneousSubmodule_moduleFinite {σ : Type u_1} {R : Type u_2} [CommSemiring R] [Finite σ] (n : ℕ) : Module.Finite R ↥(MvPolynomial.homogeneousSubmodule σ R n)

A homogeneous component in finitely many variables is a finite module.

instance TauCeti.homogeneousSubmodule_moduleFree {σ : Type u_1} {R : Type u_2} [CommSemiring R] (n : ℕ) : Module.Free R ↥(MvPolynomial.homogeneousSubmodule σ R n)

A homogeneous component is a free module, with the monomials of its degree as basis.

@[simp]

theorem TauCeti.coe_basisRestrictSupport_apply {σ : Type u_1} {R : Type u_2} [CommSemiring R] (s : Set (σ →₀ ℕ)) (m : ↑s) : ↑((MvPolynomial.basisRestrictSupport R s) m) = (MvPolynomial.monomial ↑m) 1

The restricted-support basis vector is the monomial indexed by its support element.

noncomputable def TauCeti.homogeneousMonomialBasis {σ : Type u_1} {R : Type u_2} [CommSemiring R] (n : ℕ) : Module.Basis { s : σ →₀ ℕ // Finsupp.degree s = n } R ↥(MvPolynomial.homogeneousSubmodule σ R n)

The monomial basis of a homogeneous component, indexed by exponent vectors of its degree.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.coe_homogeneousMonomialBasis {σ : Type u_1} {R : Type u_2} [CommSemiring R] (n : ℕ) (s : { s : σ →₀ ℕ // Finsupp.degree s = n }) : ↑((homogeneousMonomialBasis n) s) = (MvPolynomial.monomial ↑s) 1

A homogeneous monomial basis vector is the corresponding monomial.

@[simp]

theorem TauCeti.homogeneousMonomialBasis_repr_apply {σ : Type u_1} {R : Type u_2} [CommSemiring R] (n : ℕ) (p : ↥(MvPolynomial.homogeneousSubmodule σ R n)) (s : { s : σ →₀ ℕ // Finsupp.degree s = n }) : ((homogeneousMonomialBasis n).repr p) s = (↑p).coeff ↑s

The coordinate of a homogeneous polynomial in the monomial basis is its corresponding coefficient.

noncomputable def TauCeti.mapHomogeneousSubmodule {σ : Type u_1} {R : Type u_2} {S : Type u_3} [CommSemiring R] [CommSemiring S] (f : R →+* S) (n : ℕ) : ↥(MvPolynomial.homogeneousSubmodule σ R n) →ₛₗ[f] ↥(MvPolynomial.homogeneousSubmodule σ S n)

Mapping the coefficients of the homogeneous polynomials of degree n along a ring homomorphism f : R →+* S, as an f-semilinear map.

Equations

• TauCeti.mapHomogeneousSubmodule f n = { toFun := fun (p : ↥(MvPolynomial.homogeneousSubmodule σ R n)) => ⟨(MvPolynomial.map f) ↑p, ⋯⟩, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem TauCeti.coe_mapHomogeneousSubmodule_apply {σ : Type u_1} {R : Type u_2} {S : Type u_3} [CommSemiring R] [CommSemiring S] (f : R →+* S) {n : ℕ} (p : ↥(MvPolynomial.homogeneousSubmodule σ R n)) : ↑((mapHomogeneousSubmodule f n) p) = (MvPolynomial.map f) ↑p

@[simp]

theorem TauCeti.mapHomogeneousSubmodule_homogeneousMonomialBasis {σ : Type u_1} {R : Type u_2} {S : Type u_3} [CommSemiring R] [CommSemiring S] (f : R →+* S) (n : ℕ) (s : { s : σ →₀ ℕ // Finsupp.degree s = n }) : (mapHomogeneousSubmodule f n) ((homogeneousMonomialBasis n) s) = (homogeneousMonomialBasis n) s

Changing coefficients sends the monomial basis to the monomial basis.

noncomputable def TauCeti.finsuppDegreeFinTwoEquiv (w : ℕ) : { s : Fin 2 →₀ ℕ // Finsupp.degree s = w } ≃ Fin (w + 1)

Exponent vectors of degree w in two variables are determined by their value at 0.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.coe_finsuppDegreeFinTwoEquiv_symm (w : ℕ) (j : Fin (w + 1)) : ↑((finsuppDegreeFinTwoEquiv w).symm j) = Finsupp.single 0 ↑j + Finsupp.single 1 (w - ↑j)

theorem TauCeti.finrank_homogeneousSubmodule (σ : Type u_1) (R : Type u_2) [CommSemiring R] [StrongRankCondition R] (n : ℕ) : Module.finrank R ↥(MvPolynomial.homogeneousSubmodule σ R n) = Nat.card ↑{d : σ →₀ ℕ | Finsupp.degree d = n}

The dimension of a homogeneous component is the number of exponent vectors of its degree.

@[simp]

theorem TauCeti.finrank_homogeneousSubmodule_eq_multichoose (σ : Type u_1) (R : Type u_2) [Fintype σ] [CommSemiring R] [StrongRankCondition R] (n : ℕ) : Module.finrank R ↥(MvPolynomial.homogeneousSubmodule σ R n) = (Fintype.card σ).multichoose n

The dimension of a homogeneous component is a multichoose number.

theorem TauCeti.finrank_homogeneousSubmodule_fin_two (R : Type u_1) [CommSemiring R] [StrongRankCondition R] (w : ℕ) : Module.finrank R ↥(MvPolynomial.homogeneousSubmodule (Fin 2) R w) = w + 1

The degree-w homogeneous polynomials in two variables have dimension w + 1.