The affine translations underlying the homogeneous coordinate changes preserve degree and irreducibility, over every coefficient field.

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

The translation X j ↦ X j + a j of polynomials in Fin n variables, as an algebra automorphism over R.

Equations

• CCDN.affineTranslation R a = CCDN.originShiftEquiv a

theorem CCDN.affineTranslation_irreducible_iff {R : Type u_1} [CommRing R] {n : ℕ} (a : Fin n → R) (f : MvPolynomial (Fin n) R) : Irreducible ((affineTranslation R a) f) ↔ Irreducible f

An affine translation of variables preserves and reflects irreducibility.

theorem CCDN.affineTranslation_totalDegree_le {R : Type u_1} [CommRing R] [Nontrivial R] {n : ℕ} (a : Fin n → R) (f : MvPolynomial (Fin n) R) : ((affineTranslation R a) f).totalDegree ≤ f.totalDegree

An affine translation of variables does not increase the total degree.

theorem CCDN.affineTranslation_totalDegree {R : Type u_1} [CommRing R] [Nontrivial R] {n : ℕ} (a : Fin n → R) (f : MvPolynomial (Fin n) R) : ((affineTranslation R a) f).totalDegree = f.totalDegree

An affine translation of variables preserves the total degree over a nontrivial ring.

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

Affine translation commutes with mapping coefficients along a ring homomorphism φ, the translation vector being mapped by φ as well.

theorem CCDN.affineChart_homogeneousTranslation {R : Type u_1} [CommRing R] {n : ℕ} (a : Fin n → R) (f : MvPolynomial (Fin (n + 1)) R) : (affineChart n) ((homogeneousTranslation R a) f) = (affineTranslation R a) ((affineChart n) f)

Dehomogenizing at X 0 intertwines the homogeneous translation Xⱼ₊₁ ↦ Xⱼ₊₁ + aⱼ X₀ with the affine translation Xⱼ ↦ Xⱼ + aⱼ.