Integral translations of the affine chart, lifted to homogeneous linear coordinate changes, preserve primitive equations and homogeneous degree.

noncomputable def CCDN.homogeneousTranslationHom (R : Type u_1) [CommRing R] {n : ℕ} (a : Fin n → R) : MvPolynomial (Fin (n + 1)) R →ₐ[R] MvPolynomial (Fin (n + 1)) R

The homogeneous linear substitution fixing X 0 and sending X (j + 1) to X (j + 1) + a j * X 0; on the affine chart X 0 = 1 it is the translation by a.

Equations

• CCDN.homogeneousTranslationHom R a = MvPolynomial.aeval (Fin.cons (MvPolynomial.X 0) fun (j : Fin n) => MvPolynomial.X j.succ + MvPolynomial.C (a j) * MvPolynomial.X 0)

theorem CCDN.homogeneousTranslationHom_comp {R : Type u_1} [CommRing R] {n : ℕ} (a b : Fin n → R) : (homogeneousTranslationHom R a).comp (homogeneousTranslationHom R b) = homogeneousTranslationHom R (a + b)

Composing the homogeneous translations by a and by b gives the homogeneous translation by a + b.

@[simp]

theorem CCDN.homogeneousTranslationHom_zero (R : Type u_1) [CommRing R] (n : ℕ) : homogeneousTranslationHom R 0 = AlgHom.id R (MvPolynomial (Fin (n + 1)) R)

The homogeneous translation by zero is the identity.

noncomputable def CCDN.homogeneousTranslation (R : Type u_1) [CommRing R] {n : ℕ} (a : Fin n → R) : MvPolynomial (Fin (n + 1)) R ≃ₐ[R] MvPolynomial (Fin (n + 1)) R

The homogeneous translation by a (fixing X 0 and sending X (j + 1) to X (j + 1) + a j * X 0) as an algebra automorphism, with inverse the homogeneous translation by -a.

Equations

• CCDN.homogeneousTranslation R a = AlgEquiv.ofAlgHom (CCDN.homogeneousTranslationHom R a) (CCDN.homogeneousTranslationHom R (-a)) ⋯ ⋯

theorem CCDN.homogeneousTranslation_homogeneous {R : Type u_1} [CommRing R] {n d : ℕ} (a : Fin n → R) {f : MvPolynomial (Fin (n + 1)) R} (hf : f.IsHomogeneous d) : ((homogeneousTranslation R a) f).IsHomogeneous d

The homogeneous translation of a homogeneous polynomial of degree d is homogeneous of degree d.

theorem CCDN.PrimitiveIntegerPolynomial.translate_homogeneous {n : ℕ} (a : Fin n → ℤ) {f : MvPolynomial (Fin (n + 1)) ℤ} (hf : PrimitiveIntegerPolynomial f) : PrimitiveIntegerPolynomial ((homogeneousTranslation ℤ a) f)

The homogeneous translation by an integer vector of a primitive integer polynomial is primitive.

theorem CCDN.homogeneousTranslation_eval {R : Type u_1} [CommRing R] {n : ℕ} (a : Fin n → R) (f : MvPolynomial (Fin (n + 1)) R) (x : Fin (n + 1) → R) : (MvPolynomial.eval x) ((homogeneousTranslation R a) f) = (MvPolynomial.eval (Fin.cons (x 0) fun (j : Fin n) => x j.succ + a j * x 0)) f

The homogeneous translation of f by a evaluates at x to the value of f at the point with coordinates x 0 and x (j + 1) + a j * x 0.

theorem CCDN.homogeneousTranslation_eval_chart {R : Type u_1} [CommRing R] {n : ℕ} (a z : Fin n → R) (f : MvPolynomial (Fin (n + 1)) R) : (MvPolynomial.eval (Fin.cons 1 z)) ((homogeneousTranslation R a) f) = (MvPolynomial.eval (Fin.cons 1 (z + a))) f

On the affine chart X 0 = 1, the homogeneous translation of f by a evaluates at the point (1, z) to the value of f at (1, z + a).

theorem CCDN.homogeneousTranslation_integer_point_box {n : ℕ} {B : ℝ} {d : ℕ} (hB : 1 ≤ B) (a z : Fin n → ℤ) (ha : ∀ (j : Fin n), 0 ≤ a j ∧ a j ≤ ↑d) (hz : InBox z B) (j : Fin n) : |↑(z j - a j)| ≤ (↑d + 1) * B

If z lies in the box of radius B ≥ 1 and every coordinate of a lies in [0, d], then every coordinate of z - a has absolute value at most (d + 1) * B.