Integral plane shears are polynomial-ring automorphisms in every characteristic. They will place the highest-degree part in the outer variable.

noncomputable def CCDN.planeShearHom (R : Type u_1) [CommRing R] (a : R) : MvPolynomial (Fin 2) R →ₐ[R] MvPolynomial (Fin 2) R

Fix variable zero and replace variable one by x₁+a*x₀.

Equations

• CCDN.planeShearHom R a = MvPolynomial.aeval ![MvPolynomial.X 0, MvPolynomial.X 1 + MvPolynomial.C a * MvPolynomial.X 0]

theorem CCDN.planeShearHom_comp {R : Type u_1} [CommRing R] (a b : R) : (planeShearHom R a).comp (planeShearHom R b) = planeShearHom R (a + b)

Composing the plane shears with parameters a and b gives the shear with parameter a + b.

@[simp]

theorem CCDN.planeShearHom_zero (R : Type u_1) [CommRing R] : planeShearHom R 0 = AlgHom.id R (MvPolynomial (Fin 2) R)

The plane shear with parameter zero is the identity.

noncomputable def CCDN.planeShear (R : Type u_1) [CommRing R] (a : R) : MvPolynomial (Fin 2) R ≃ₐ[R] MvPolynomial (Fin 2) R

The plane shear x₁ ↦ x₁ + a * x₀ as an algebra automorphism. The inverse shear uses the negative parameter, so this works over Z and all its residue fields without determinant denominators.

Equations

• CCDN.planeShear R a = AlgEquiv.ofAlgHom (CCDN.planeShearHom R a) (CCDN.planeShearHom R (-a)) ⋯ ⋯

theorem CCDN.planeShear_totalDegree {R : Type u_1} [CommRing R] [Nontrivial R] (a : R) (f : MvPolynomial (Fin 2) R) : ((planeShear R a) f).totalDegree = f.totalDegree

A plane shear preserves the total degree; the inverse shear gives the reverse inequality.

theorem CCDN.planeShear_map {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] (φ : R →+* S) (a : R) (f : MvPolynomial (Fin 2) R) : (MvPolynomial.map φ) ((planeShear R a) f) = (planeShear S (φ a)) ((MvPolynomial.map φ) f)

planeShear commutes with every coefficient map.