Bounded integral shears act on all projective representatives, preserve primitivity, and preserve distinctness of their projective classes.

def CCDN.homogeneousPointTranslation {R : Type u_1} [CommRing R] {n : ℕ} (a : Fin n → R) (x : Fin (n + 1) → R) : Fin (n + 1) → R

The shear of a point x by a, keeping 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.homogeneousPointTranslation a x = Fin.cons (x 0) fun (j : Fin n) => x j.succ + a j * x 0

theorem CCDN.homogeneousPointTranslation_inverse {R : Type u_1} [CommRing R] {n : ℕ} (a : Fin n → R) (x : Fin (n + 1) → R) : homogeneousPointTranslation (-a) (homogeneousPointTranslation a x) = x

The shear by -a undoes the shear by a.

theorem CCDN.homogeneousPointTranslation_ne_zero {R : Type u_1} [CommRing R] {n : ℕ} (a : Fin n → R) {x : Fin (n + 1) → R} (hx : x ≠ 0) : homogeneousPointTranslation a x ≠ 0

The shear of a nonzero point is nonzero.

theorem CCDN.homogeneousPointTranslation_gcd {n : ℕ} (a : Fin n → ℤ) (x : Fin (n + 1) → ℤ) : Finset.univ.gcd (homogeneousPointTranslation a x) = Finset.univ.gcd x

An integral shear preserves the greatest common divisor of the coordinates of an integer point; in particular it preserves primitivity.

theorem CCDN.homogeneousPointTranslation_projective_injective {n t : ℕ} (a : Fin n → ℤ) (z : Fin t → IntPoint (n + 1)) (hz0 : ∀ (i : Fin t), z i ≠ 0) (hinj : Function.Injective fun (i : Fin t) => Projectivization.mk ℚ (rationalPoint (z i)) ⋯) : Function.Injective fun (i : Fin t) => Projectivization.mk ℚ (rationalPoint (homogeneousPointTranslation a (z i))) ⋯

An integral shear preserves distinctness of projective classes: if the nonzero integer points z i represent pairwise distinct points of projective space over ℚ, so do their shears.

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

If z lies in the box of radius B ≥ 1 and every coordinate of a lies in [0, d], then the shear of z by -a lies in the box of radius (d + 1) * B.

theorem CCDN.homogeneousTranslation_map {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] {n : ℕ} (φ : R →+* S) (a : Fin n → R) (f : MvPolynomial (Fin (n + 1)) R) : (MvPolynomial.map φ) ((homogeneousTranslation R a) f) = (homogeneousTranslation S (⇑φ ∘ a)) ((MvPolynomial.map φ) f)

The homogeneous translation commutes with coefficient maps: mapping the coefficients of the homogeneous translation of f by a along φ gives the homogeneous translation of the mapped polynomial by φ ∘ a.