chore(AlgebraicGeometry/EllipticCurve/Projective/*): split projective files (#22549)

Author: Multramate

Mathlib.lean

@@ -1063,7 +1063,9 @@ import Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ
 import Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian
 import Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ
 import Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
-import Mathlib.AlgebraicGeometry.EllipticCurve.Projective
+import Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
+import Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
+import Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
 import Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange
 import Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
 import Mathlib.AlgebraicGeometry.Fiber

Mathlib/AlgebraicGeometry/EllipticCurve/Group.lean

@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: David Kurniadi Angdinata
 -/
 import Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian
-import Mathlib.AlgebraicGeometry.EllipticCurve.Projective
 import Mathlib.LinearAlgebra.FreeModule.Norm
 import Mathlib.RingTheory.ClassGroup
 import Mathlib.RingTheory.Polynomial.UniqueFactorization
@@ -13,9 +12,8 @@ import Mathlib.RingTheory.Polynomial.UniqueFactorization
 # Group law on Weierstrass curves
 
 This file proves that the nonsingular rational points on a Weierstrass curve form an abelian group
-under the geometric group law defined in `Mathlib/AlgebraicGeometry/EllipticCurve/Affine.lean`, in
-`Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean`, and in
-`Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean`.
+under the geometric group law defined in `Mathlib/AlgebraicGeometry/EllipticCurve/Affine.lean` and
+in `Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean`.
 
 ## Mathematical background
 
@@ -38,9 +36,6 @@ auxiliary lemmas in the proof of `WeierstrassCurve.Affine.Point.instAddCommGroup
 When `W` is given in Jacobian coordinates, `WeierstrassCurve.Jacobian.Point.toAffineAddEquiv` pulls
 back the group law on `WeierstrassCurve.Affine.Point` to `WeierstrassCurve.Jacobian.Point`.
 
-When `W` is given in projective coordinates, `WeierstrassCurve.Projective.Point.toAffineAddEquiv`
-pulls back the group law on `WeierstrassCurve.Affine.Point` to `WeierstrassCurve.Projective.Point`.
-
 ## Main definitions
 
  * `WeierstrassCurve.Affine.CoordinateRing`: the coordinate ring `F[W]` of a Weierstrass curve `W`.
@@ -56,8 +51,6 @@ pulls back the group law on `WeierstrassCurve.Affine.Point` to `WeierstrassCurve
     coordinates forms an abelian group under addition.
  * `WeierstrassCurve.Jacobian.Point.instAddCommGroup`: the type of nonsingular points on a
     Weierstrass curve in Jacobian coordinates forms an abelian group under addition.
- * `WeierstrassCurve.Projective.Point.instAddCommGroup`: the type of nonsingular points on a
-    Weierstrass curve in projective coordinates forms an abelian group under addition.
 
 ## References
 
@@ -565,26 +558,6 @@ end Point
 
 end WeierstrassCurve.Affine
 
-namespace WeierstrassCurve.Projective.Point
-
-/-! ## Weierstrass curves in projective coordinates -/
-
-variable {F : Type u} [Field F] {W : Projective F}
-
-noncomputable instance : AddCommGroup W.Point where
-  nsmul := nsmulRec
-  zsmul := zsmulRec
-  zero_add _ := (toAffineAddEquiv W).injective <| by
-    simp only [map_add, toAffineAddEquiv_apply, toAffineLift_zero, zero_add]
-  add_zero _ := (toAffineAddEquiv W).injective <| by
-    simp only [map_add, toAffineAddEquiv_apply, toAffineLift_zero, add_zero]
-  neg_add_cancel P := (toAffineAddEquiv W).injective <| by
-    simp only [map_add, toAffineAddEquiv_apply, toAffineLift_neg, neg_add_cancel, toAffineLift_zero]
-  add_comm _ _ := (toAffineAddEquiv W).injective <| by simp only [map_add, add_comm]
-  add_assoc _ _ _ := (toAffineAddEquiv W).injective <| by simp only [map_add, add_assoc]
-
-end WeierstrassCurve.Projective.Point
-
 namespace WeierstrassCurve.Jacobian.Point
 
 /-! ## Weierstrass curves in Jacobian coordinates -/