Spans of monomials in two elements under a shear

Let u and y be elements of a commutative R-algebra A. The products u ^ i y ^ j with i + j < n span the values at (u, y) of the polynomials of total degree less than n. A linear change of coordinates u ↦ u + c • y preserves total degrees, so it does not change this span. This is how statements about the polynomials of bounded degree in the affine coordinates of a plane curve are transported between coordinate systems.

Main results

• TauCeti.add_smul_pow_mul_pow_mem_span: (u + c • y) ^ i y ^ j lies in the span of the products u ^ a y ^ b with a + b ≤ i + j.
• TauCeti.span_add_smul_pow_mul_pow: the products (u + c • y) ^ i y ^ j and u ^ i y ^ j with i + j < n span the same submodule.

theorem TauCeti.add_smul_pow_mul_pow_mem_span {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommSemiring A] [Algebra R A] (u y : A) (c : R) (i j : ℕ) : (u + c • y) ^ i * y ^ j ∈ Submodule.span R ((fun (p : ℕ × ℕ) => u ^ p.1 * y ^ p.2) '' {p : ℕ × ℕ | p.1 + p.2 < i + j + 1})

A product (u + c • y) ^ i y ^ j lies in the span of the products u ^ a y ^ b of total degree a + b ≤ i + j.

theorem TauCeti.span_add_smul_pow_mul_pow {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] (u y : A) (c : R) (n : ℕ) : Submodule.span R ((fun (p : ℕ × ℕ) => (u + c • y) ^ p.1 * y ^ p.2) '' {p : ℕ × ℕ | p.1 + p.2 < n}) = Submodule.span R ((fun (p : ℕ × ℕ) => u ^ p.1 * y ^ p.2) '' {p : ℕ × ℕ | p.1 + p.2 < n})

A shear does not change the span of the monomials of bounded degree: the products (u + c • y) ^ i y ^ j and u ^ i y ^ j with i + j < n span the same submodule.