Negation of solutions of the projective Weierstrass equation

For a Weierstrass curve W' over a commutative ring, Mathlib's negation WeierstrassCurve.Projective.neg sends a point representative [P₀ : P₁ : P₂] to [P₀ : -P₁ - a₁P₀ - a₃P₂ : P₂]. Mathlib shows that it preserves nonsingularity over a field; this file shows that over any commutative ring it is the action on homogeneous coordinates of the change of variables negVariableChange W', which fixes W', and hence that it preserves the projective Weierstrass equation.

Main results

• WeierstrassCurve.toMatrix_negVariableChange_mulVec: the matrix of negVariableChange W acts on point representatives by WeierstrassCurve.Projective.neg.
• WeierstrassCurve.Projective.equation_neg: the negation of a point representative is a solution of the projective Weierstrass equation exactly when the representative is.

theorem WeierstrassCurve.toMatrix_negVariableChange_mulVec {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) (P : Fin 3 → R) : W.negVariableChange.toMatrix.mulVec P = W.toProjective.neg P

The change of variables negVariableChange W acts on homogeneous coordinates by Mathlib's negation: W.negVariableChange.toMatrix *ᵥ P = [P₀ : -P₁ - a₁P₀ - a₃P₂ : P₂].

theorem WeierstrassCurve.Projective.equation_neg {R : Type u_1} [CommRing R] {W' : Projective R} (P : Fin 3 → R) : W'.Equation (W'.neg P) ↔ W'.Equation P

The negation W'.neg P = [P₀ : -P₁ - a₁P₀ - a₃P₂ : P₂] of a point representative P is a solution of the projective Weierstrass equation exactly when P is: the projective form of WeierstrassCurve.Affine.equation_neg.