Explicit invertible affine coordinates along a direction with nonzero first component. The same map carries its base point to the origin and identifies the first partial derivative with the directional derivative.

noncomputable def CCDN.directionCoordinatesHom {K : Type u_1} {σ : Type u_2} [Field K] (b : Option σ → K) : MvPolynomial (Option σ) K →ₐ[K] MvPolynomial (Option σ) K

The linear coordinates x_i = b_i*x_0 + z_i, with no z_0.

Equations

• CCDN.directionCoordinatesHom b = MvPolynomial.aeval fun (i : Option σ) => MvPolynomial.C (b i) * MvPolynomial.X none + i.elim 0 fun (j : σ) => MvPolynomial.X (some j)

noncomputable def CCDN.directionCoordinatesInv {K : Type u_1} {σ : Type u_2} [Field K] (b : Option σ → K) : MvPolynomial (Option σ) K →ₐ[K] MvPolynomial (Option σ) K

The inverse of the linear coordinates directionCoordinatesHom b when b none ≠ 0: the substitution sending $x_0$ to $b_0^{-1} x_0$ and every other $x_i$ to $x_i - b_i b_0^{-1} x_0$.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CCDN.directionCoordinates {K : Type u_1} {σ : Type u_2} [Field K] (b : Option σ → K) (hb : b none ≠ 0) : MvPolynomial (Option σ) K ≃ₐ[K] MvPolynomial (Option σ) K

The linear coordinates $x_i = b_i x_0 + z_i$ (with no $z_0$) as an algebra automorphism, for a direction b with nonzero first component.

Equations

• CCDN.directionCoordinates b hb = AlgEquiv.ofAlgHom (CCDN.directionCoordinatesHom b) (CCDN.directionCoordinatesInv b) ⋯ ⋯

noncomputable def CCDN.hypersurfaceAffineCoordinates {K : Type u_1} {σ : Type u_2} [Field K] (a b : Option σ → K) (hb : b none ≠ 0) : MvPolynomial (Option σ) K ≃ₐ[K] MvPolynomial (Option σ) K

Substitute a_i+b_i*x_0+z_i, so the new origin is the old point a.

Equations

• CCDN.hypersurfaceAffineCoordinates a b hb = (CCDN.originShiftEquiv a).trans (CCDN.directionCoordinates b hb)

theorem CCDN.hypersurfaceAffineCoordinates_X {K : Type u_1} {σ : Type u_2} [Field K] (a b : Option σ → K) (hb : b none ≠ 0) (i : Option σ) : (hypersurfaceAffineCoordinates a b hb) (MvPolynomial.X i) = MvPolynomial.C (a i) + MvPolynomial.C (b i) * MvPolynomial.X none + i.elim 0 fun (j : σ) => MvPolynomial.X (some j)

The affine coordinates substitute $a_i + b_i x_0 + z_i$ for the variable $x_i$, with no $z_0$ term for the distinguished variable.

theorem CCDN.hypersurfaceAffineCoordinates_totalDegree_le {K : Type u_1} {σ : Type u_2} [Field K] (a b : Option σ → K) (hb : b none ≠ 0) (f : MvPolynomial (Option σ) K) : ((hypersurfaceAffineCoordinates a b hb) f).totalDegree ≤ f.totalDegree

The affine change of coordinates hypersurfaceAffineCoordinates a b hb does not increase the total degree.

theorem CCDN.hypersurfaceAffineCoordinates_eval_zero {K : Type u_1} {σ : Type u_2} [Field K] (a b : Option σ → K) (hb : b none ≠ 0) (f : MvPolynomial (Option σ) K) : (MvPolynomial.eval 0) ((hypersurfaceAffineCoordinates a b hb) f) = (MvPolynomial.eval a) f

The affine coordinates carry the base point a to the origin: the transformed polynomial takes at 0 the value of f at a.

theorem CCDN.hypersurfaceAffineCoordinates_partial_zero {K : Type u_1} {σ : Type u_2} [Field K] [Fintype σ] (a b : Option σ → K) (hb : b none ≠ 0) (f : MvPolynomial (Option σ) K) : (MvPolynomial.eval 0) ((MvPolynomial.pderiv none) ((hypersurfaceAffineCoordinates a b hb) f)) = ∑ i : Option σ, (MvPolynomial.eval a) ((MvPolynomial.pderiv i) f) * b i

In the affine coordinates, the first partial derivative at the origin is the derivative of f at a in the direction b.