Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

chore(AlgebraicGeometry/EllipticCurve/*): remove redundant names #22479

Open
wants to merge 3 commits into
base: master
Choose a base branch
from
+75 −85
Open

chore(AlgebraicGeometry/EllipticCurve/*): remove redundant names #22479

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
0df530c
Remove redundant names
Multramate Mar 2, 2025
b6a49af
Revert mk
Multramate Mar 2, 2025
a4f6c76
Merge branch 'master' into EllipticCurve.Redundant
Multramate Mar 3, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
95 changes: 42 additions & 53 deletions Mathlib/AlgebraicGeometry/EllipticCurve/Affine.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -277,19 +277,30 @@ lemma nonsingular_iff_variableChange (x y : R) :
simp only [variableChange]
congr! 3 <;> ring1

lemma nonsingular_zero_of_Δ_ne_zero (h : W'.Equation 0 0) (hΔ : W'.Δ ≠ 0) :
W'.Nonsingular 0 0 := by
simp only [equation_zero, nonsingular_zero] at *
private lemma equation_zero_iff_nonsingular_zero_of_Δ_ne_zero (hΔ : W'.Δ ≠ 0) :
W'.Equation 0 0 ↔ W'.Nonsingular 0 0 := by
simp only [equation_zero, nonsingular_zero, iff_self_and]
contrapose! hΔ
simp only [b₂, b₄, b₆, b₈, Δ, h, hΔ]
simp only [b₂, b₄, b₆, b₈, Δ, hΔ]
ring1

/-- A Weierstrass curve is nonsingular at every point if its discriminant is non-zero. -/
lemma nonsingular_of_Δ_ne_zero {x y : R} (h : W'.Equation x y) (hΔ : W'.Δ ≠ 0) :
W'.Nonsingular x y :=
(nonsingular_iff_variableChange x y).mpr <|
nonsingular_zero_of_Δ_ne_zero ((equation_iff_variableChange x y).mp h) <| by
rwa [variableChange_Δ, inv_one, Units.val_one, one_pow, one_mul]
lemma equation_iff_nonsingular_of_Δ_ne_zero {x y : R} (hΔ : W'.Δ ≠ 0) :
W'.Equation x y ↔ W'.Nonsingular x y := by
rw [equation_iff_variableChange, nonsingular_iff_variableChange,
equation_zero_iff_nonsingular_zero_of_Δ_ne_zero <| by
rwa [variableChange_Δ, inv_one, Units.val_one, one_pow, one_mul]]

/-- An elliptic curve is nonsingular at every point. -/
lemma equation_iff_nonsingular [Nontrivial R] [W'.IsElliptic] {x y : R} :
W'.toAffine.Equation x y ↔ W'.toAffine.Nonsingular x y :=
W'.toAffine.equation_iff_nonsingular_of_Δ_ne_zero <| W'.coe_Δ' ▸ W'.Δ'.ne_zero

@[deprecated (since := "2025-03-01")] alias nonsingular_zero_of_Δ_ne_zero :=
equation_iff_nonsingular_of_Δ_ne_zero
@[deprecated (since := "2025-03-01")] alias nonsingular_of_Δ_ne_zero :=
equation_iff_nonsingular_of_Δ_ne_zero
@[deprecated (since := "2025-03-01")] alias nonsingular := equation_iff_nonsingular

end Nonsingular

Expand Down Expand Up @@ -389,35 +400,27 @@ This depends on `W`, and has argument order: `x₁`, `x₂`, `y₁`, `ℓ`. -/
def addY (x₁ x₂ y₁ ℓ : R) : R :=
W'.negY (W'.addX x₁ x₂ ℓ) (W'.negAddY x₁ x₂ y₁ ℓ)

lemma equation_neg_iff (x y : R) : W'.Equation x (W'.negY x y) ↔ W'.Equation x y := by
lemma equation_neg (x y : R) : W'.Equation x (W'.negY x y) ↔ W'.Equation x y := by
rw [equation_iff, equation_iff, negY]
congr! 1
ring1

lemma nonsingular_neg_iff (x y : R) : W'.Nonsingular x (W'.negY x y) ↔ W'.Nonsingular x y := by
rw [nonsingular_iff, equation_neg_iff, ← negY, negY_negY, ← @ne_comm _ y, nonsingular_iff]
@[deprecated (since := "2025-02-01")] alias equation_neg_of := equation_neg
@[deprecated (since := "2025-02-01")] alias equation_neg_iff := equation_neg

lemma nonsingular_neg (x y : R) : W'.Nonsingular x (W'.negY x y) ↔ W'.Nonsingular x y := by
rw [nonsingular_iff, equation_neg, ← negY, negY_negY, ← @ne_comm _ y, nonsingular_iff]
exact and_congr_right' <| (iff_congr not_and_or.symm not_and_or.symm).mpr <|
not_congr <| and_congr_left fun h => by rw [← h]

@[deprecated (since := "2025-02-01")] alias nonsingular_neg_of := nonsingular_neg
@[deprecated (since := "2025-02-01")] alias nonsingular_neg_iff := nonsingular_neg

lemma equation_add_iff (x₁ x₂ y₁ ℓ : R) : W'.Equation (W'.addX x₁ x₂ ℓ) (W'.negAddY x₁ x₂ y₁ ℓ) ↔
(W'.addPolynomial x₁ y₁ ℓ).eval (W'.addX x₁ x₂ ℓ) = 0 := by
rw [Equation, negAddY, addPolynomial, linePolynomial, polynomial]
eval_simp

lemma equation_neg_of {x y : R} (h : W'.Equation x <| W'.negY x y) : W'.Equation x y :=
(W'.equation_neg_iff ..).mp h

/-- The negation of an affine point in `W` lies in `W`. -/
lemma equation_neg {x y : R} (h : W'.Equation x y) : W'.Equation x <| W'.negY x y :=
(W'.equation_neg_iff ..).mpr h

lemma nonsingular_neg_of {x y : R} (h : W'.Nonsingular x <| W'.negY x y) : W'.Nonsingular x y :=
(W'.nonsingular_neg_iff ..).mp h

/-- The negation of a nonsingular affine point in `W` is nonsingular. -/
lemma nonsingular_neg {x y : R} (h : W'.Nonsingular x y) : W'.Nonsingular x <| W'.negY x y :=
(W'.nonsingular_neg_iff ..).mpr h

lemma nonsingular_negAdd_of_eval_derivative_ne_zero {x₁ x₂ y₁ ℓ : R}
(hx' : W'.Equation (W'.addX x₁ x₂ ℓ) (W'.negAddY x₁ x₂ y₁ ℓ))
(hx : (W'.addPolynomial x₁ y₁ ℓ).derivative.eval (W'.addX x₁ x₂ ℓ) ≠ 0) :
Expand Down Expand Up @@ -528,7 +531,7 @@ lemma equation_negAdd {x₁ x₂ y₁ y₂ : F} (h₁ : W.Equation x₁ y₁) (h
lemma equation_add {x₁ x₂ y₁ y₂ : F} (h₁ : W.Equation x₁ y₁) (h₂ : W.Equation x₂ y₂)
(hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)) :
W.Equation (W.addX x₁ x₂ <| W.slope x₁ x₂ y₁ y₂) (W.addY x₁ x₂ y₁ <| W.slope x₁ x₂ y₁ y₂) :=
equation_neg <| equation_negAdd h₁ h₂ hxy
(equation_neg ..).mpr <| equation_negAdd h₁ h₂ hxy

lemma C_addPolynomial_slope {x₁ x₂ y₁ y₂ : F} (h₁ : W.Equation x₁ y₁) (h₂ : W.Equation x₂ y₂)
(hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)) : C (W.addPolynomial x₁ y₁ <| W.slope x₁ x₂ y₁ y₂) =
Expand Down Expand Up @@ -567,7 +570,7 @@ lemma nonsingular_negAdd {x₁ x₂ y₁ y₂ : F} (h₁ : W.Nonsingular x₁ y
lemma nonsingular_add {x₁ x₂ y₁ y₂ : F} (h₁ : W.Nonsingular x₁ y₁) (h₂ : W.Nonsingular x₂ y₂)
(hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)) :
W.Nonsingular (W.addX x₁ x₂ <| W.slope x₁ x₂ y₁ y₂) (W.addY x₁ x₂ y₁ <| W.slope x₁ x₂ y₁ y₂) :=
nonsingular_neg <| nonsingular_negAdd h₁ h₂ hxy
(nonsingular_neg ..).mpr <| nonsingular_negAdd h₁ h₂ hxy

/-- The formula `x(P₁ + P₂) = x(P₁ - P₂) - ψ(P₁)ψ(P₂) / (x(P₂) - x(P₁))²`,
where `ψ(x,y) = 2y + a₁x + a₃`. -/
Expand Down Expand Up @@ -636,7 +639,7 @@ lemma some_ne_zero {x y : R} (h : W'.Nonsingular x y) : Point.some h ≠ 0 := by
Given a nonsingular point `P` in affine coordinates, use `-P` instead of `neg P`. -/
def neg : W'.Point → W'.Point
| 0 => 0
| some h => some <| nonsingular_neg h
| some h => some <| (nonsingular_neg ..).mpr h

instance : Neg W'.Point :=
⟨neg⟩
Expand All @@ -649,7 +652,7 @@ lemma neg_zero : (-0 : W'.Point) = 0 :=
rfl

@[simp]
lemma neg_some {x y : R} (h : W'.Nonsingular x y) : -some h = some (nonsingular_neg h) :=
lemma neg_some {x y : R} (h : W'.Nonsingular x y) : -some h = some ((nonsingular_neg ..).mpr h) :=
rfl

instance : InvolutiveNeg W'.Point where
Expand All @@ -668,10 +671,10 @@ noncomputable def add : W.Point → W.Point → W.Point
| @some _ _ _ x₁ y₁ h₁, @some _ _ _ x₂ y₂ h₂ =>
if hxy : x₁ = x₂ ∧ y₁ = W.negY x₂ y₂ then 0 else some <| nonsingular_add h₁ h₂ hxy

noncomputable instance instAddPoint : Add W.Point :=
noncomputable instance : Add W.Point :=
⟨add⟩

noncomputable instance instAddZeroClassPoint : AddZeroClass W.Point :=
noncomputable instance : AddZeroClass W.Point :=
⟨by rintro (_ | _) <;> rfl, by rintro (_ | _) <;> rfl⟩

lemma add_def (P Q : W.Point) : P + Q = P.add Q :=
Expand Down Expand Up @@ -882,26 +885,24 @@ variable [Algebra R S] [Algebra R F] [Algebra S F] [IsScalarTower R S F] [Algebr
[IsScalarTower R S K] [Algebra R L] [Algebra S L] [IsScalarTower R S L] (f : F →ₐ[S] K)
(g : K →ₐ[S] L)

/-- The function from `W⟮F⟯` to `W⟮K⟯` induced by an algebra homomorphism `f : F →ₐ[S] K`,
where `W` is defined over a subring of a ring `S`, and `F` and `K` are field extensions of `S`. -/
def mapFun : W'⟮F⟯ → W'⟮K⟯
| 0 => 0
| some h => some <| (baseChange_nonsingular _ _ f.injective).mpr h

/-- The group homomorphism from `W⟮F⟯` to `W⟮K⟯` induced by an algebra homomorphism `f : F →ₐ[S] K`,
where `W` is defined over a subring of a ring `S`, and `F` and `K` are field extensions of `S`. -/
def map : W'⟮F⟯ →+ W'⟮K⟯ where
toFun := mapFun f
toFun P := match P with
| 0 => 0
| some h => some <| (baseChange_nonsingular _ _ f.injective).mpr h
map_zero' := rfl
map_add' := by
rintro (_ | @⟨x₁, y₁, _⟩) (_ | @⟨x₂, y₂, _⟩)
any_goals rfl
by_cases hxy : x₁ = x₂ ∧ y₁ = (W'.baseChange F).toAffine.negY x₂ y₂
· simp only [add_of_Y_eq hxy.left hxy.right, mapFun]
· simp only [add_of_Y_eq hxy.left hxy.right]
rw [add_of_Y_eq (congr_arg _ hxy.left) <| by rw [hxy.right, baseChange_negY]]
· simp only [add_some hxy, mapFun, ← baseChange_addX, ← baseChange_addY, ← baseChange_slope]
· simp only [add_some hxy, ← baseChange_addX, ← baseChange_addY, ← baseChange_slope]
rw [add_some fun h => hxy ⟨f.injective h.1, f.injective (W'.baseChange_negY f .. ▸ h).2⟩]

@[deprecated (since := "2025-03-01")] alias mapFun := map

lemma map_zero : map f (0 : W'⟮F⟯) = 0 :=
rfl

Expand Down Expand Up @@ -936,16 +937,4 @@ end Point

end Affine

/-! ## Elliptic curves -/

section EllipticCurve

variable {R : Type u} [CommRing R] (E : WeierstrassCurve R) [E.IsElliptic]

lemma nonsingular [Nontrivial R] {x y : R} (h : E.toAffine.Equation x y) :
E.toAffine.Nonsingular x y :=
E.toAffine.nonsingular_of_Δ_ne_zero h <| E.coe_Δ' ▸ E.Δ'.ne_zero

end EllipticCurve

end WeierstrassCurve
38 changes: 18 additions & 20 deletions Mathlib/AlgebraicGeometry/EllipticCurve/Group.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -398,19 +398,21 @@ lemma XYIdeal'_eq {x y : F} (h : W.Nonsingular x y) :
(XYIdeal' h : FractionalIdeal W.CoordinateRing⁰ W.FunctionField) = XYIdeal W x (C y) :=
rfl

lemma mk_XYIdeal'_mul_mk_XYIdeal'_of_Yeq {x y : F} (h : W.Nonsingular x y) :
ClassGroup.mk (XYIdeal' <| nonsingular_neg h) * ClassGroup.mk (XYIdeal' h) = 1 := by
lemma mk_XYIdeal'_neg_mul {x y : F} (h : W.Nonsingular x y) :
ClassGroup.mk (XYIdeal' <| (nonsingular_neg ..).mpr h) * ClassGroup.mk (XYIdeal' h) = 1 := by
rw [← _root_.map_mul]
exact
(ClassGroup.mk_eq_one_of_coe_ideal <| by exact (FractionalIdeal.coeIdeal_mul ..).symm.trans <|
FractionalIdeal.coeIdeal_inj.mpr <| XYIdeal_neg_mul h).mpr ⟨_, XClass_ne_zero W _, rfl⟩
exact (ClassGroup.mk_eq_one_of_coe_ideal <| (FractionalIdeal.coeIdeal_mul ..).symm.trans <|
FractionalIdeal.coeIdeal_inj.mpr <| XYIdeal_neg_mul h).mpr ⟨_, XClass_ne_zero W _, rfl⟩

@[deprecated (since := "2025-03-01")] alias mk_XYIdeal'_mul_mk_XYIdeal'_of_Yeq :=
mk_XYIdeal'_neg_mul

lemma mk_XYIdeal'_mul_mk_XYIdeal' {x₁ x₂ y₁ y₂ : F} (h₁ : W.Nonsingular x₁ y₁)
(h₂ : W.Nonsingular x₂ y₂) (hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)) :
ClassGroup.mk (XYIdeal' h₁) * ClassGroup.mk (XYIdeal' h₂) =
ClassGroup.mk (XYIdeal' <| nonsingular_add h₁ h₂ hxy) := by
rw [← _root_.map_mul]
exact (ClassGroup.mk_eq_mk_of_coe_ideal (by exact (FractionalIdeal.coeIdeal_mul ..).symm) <|
exact (ClassGroup.mk_eq_mk_of_coe_ideal (FractionalIdeal.coeIdeal_mul ..).symm <|
XYIdeal'_eq _).mpr
⟨_, _, XClass_ne_zero W _, YClass_ne_zero W _, XYIdeal_mul_XYIdeal h₁.left h₂.left hxy⟩

Expand Down Expand Up @@ -496,28 +498,25 @@ namespace Point

variable {F : Type u} [Field F] {W : Affine F}

/-- The set function mapping a nonsingular affine point `(x, y)` of a Weierstrass curve `W` to the
class of the non-zero fractional ideal `⟨X - x, Y - y⟩` in the ideal class group of `F[W]`. -/
@[simp]
noncomputable def toClassFun : W.Point → Additive (ClassGroup W.CoordinateRing)
| 0 => 0
| some h => Additive.ofMul <| ClassGroup.mk <| CoordinateRing.XYIdeal' h

/-- The group homomorphism mapping a nonsingular affine point `(x, y)` of a Weierstrass curve `W` to
the class of the non-zero fractional ideal `⟨X - x, Y - y⟩` in the ideal class group of `F[W]`. -/
@[simps]
noncomputable def toClass : W.Point →+ Additive (ClassGroup W.CoordinateRing) where
toFun := toClassFun
toFun P := match P with
| 0 => 0
| some h => Additive.ofMul <| ClassGroup.mk <| CoordinateRing.XYIdeal' h
map_zero' := rfl
map_add' := by
rintro (_ | @⟨x₁, y₁, h₁⟩) (_ | @⟨x₂, y₂, h₂⟩)
any_goals simp only [toClassFun, ← zero_def, zero_add, add_zero]
any_goals simp only [← zero_def, zero_add, add_zero]
by_cases hxy : x₁ = x₂ ∧ y₁ = W.negY x₂ y₂
· simp only [hxy.left, hxy.right, add_of_Y_eq rfl rfl]
exact (CoordinateRing.mk_XYIdeal'_mul_mk_XYIdeal'_of_Yeq h₂).symm
exact (CoordinateRing.mk_XYIdeal'_neg_mul h₂).symm
· simp only [add_some hxy]
exact (CoordinateRing.mk_XYIdeal'_mul_mk_XYIdeal' h₁ h₂ hxy).symm

@[deprecated (since := "2025-02-01")] alias toClassFun := toClass

lemma toClass_zero : toClass (0 : W.Point) = 0 :=
rfl

Expand All @@ -544,15 +543,14 @@ lemma toClass_eq_zero (P : W.Point) : toClass P = 0 ↔ P = 0 := by
apply (p.natDegree_norm_ne_one _).elim
rw [← finrank_quotient_span_eq_natDegree_norm (CoordinateRing.basis W) h0,
← (quotientEquivAlgOfEq F hp).toLinearEquiv.finrank_eq,
(CoordinateRing.quotientXYIdealEquiv W h).toLinearEquiv.finrank_eq,
Module.finrank_self]
(CoordinateRing.quotientXYIdealEquiv W h).toLinearEquiv.finrank_eq, Module.finrank_self]
· exact congr_arg toClass

lemma toClass_injective : Function.Injective <| @toClass _ _ W := by
rintro (_ | h) _ hP
all_goals rw [← neg_inj, ← add_eq_zero, ← toClass_eq_zero, map_add, ← hP]
· exact zero_add 0
· exact CoordinateRing.mk_XYIdeal'_mul_mk_XYIdeal'_of_Yeq h
· exact CoordinateRing.mk_XYIdeal'_neg_mul h

noncomputable instance : AddCommGroup W.Point where
nsmul := nsmulRec
Expand Down Expand Up @@ -615,6 +613,6 @@ variable {R : Type*} [Nontrivial R] [CommRing R] (E : WeierstrassCurve R) [E.IsE

/-- An affine point on an elliptic curve `E` over a commutative ring `R`. -/
def mk {x y : R} (h : E.toAffine.Equation x y) : E.toAffine.Point :=
WeierstrassCurve.Affine.Point.some <| nonsingular E h
.some <| (equation_iff_nonsingular ..).mp h

end WeierstrassCurve.Affine.Point
16 changes: 9 additions & 7 deletions Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -184,7 +184,7 @@ section Jacobian
/-! ### Jacobian coordinates -/

/-- The scalar multiplication for a Jacobian point representative on a Weierstrass curve. -/
scoped instance instSMulPoint : SMul R <| Fin 3 → R :=
scoped instance : SMul R <| Fin 3 → R :=
⟨fun u P => ![u ^ 2 * P x, u ^ 3 * P y, u * P z]⟩

lemma smul_fin3 (P : Fin 3 → R) (u : R) : u • P = ![u ^ 2 * P x, u ^ 3 * P y, u * P z] :=
Expand All @@ -200,12 +200,13 @@ lemma comp_smul (f : R →+* S) (P : Fin 3 → R) (u : R) : f ∘ (u • P) = f
@[deprecated (since := "2025-01-30")] alias map_smul := comp_smul

/-- The multiplicative action for a Jacobian point representative on a Weierstrass curve. -/
scoped instance instMulActionPoint : MulAction R <| Fin 3 → R where
scoped instance : MulAction R <| Fin 3 → R where
one_smul _ := by simp_rw [smul_fin3, one_pow, one_mul, fin3_def]
mul_smul _ _ _ := by simp_rw [smul_fin3, mul_pow, mul_assoc, fin3_def_ext]

/-- The equivalence setoid for a Jacobian point representative on a Weierstrass curve. -/
@[reducible] scoped instance instSetoidPoint : Setoid <| Fin 3 → R :=
@[reducible]
scoped instance : Setoid <| Fin 3 → R :=
MulAction.orbitRel Rˣ <| Fin 3 → R

variable (R) in
Expand Down Expand Up @@ -1238,7 +1239,8 @@ lemma neg_of_Z_ne_zero {P : Fin 3 → F} (hPz : P z ≠ 0) :

private lemma nonsingular_neg_of_Z_ne_zero {P : Fin 3 → F} (hP : W.Nonsingular P) (hPz : P z ≠ 0) :
W.Nonsingular ![P x / P z ^ 2, W.toAffine.negY (P x / P z ^ 2) (P y / P z ^ 3), 1] :=
(nonsingular_some ..).mpr <| Affine.nonsingular_neg <| (nonsingular_of_Z_ne_zero hPz).mp hP
(nonsingular_some ..).mpr <| (Affine.nonsingular_neg ..).mpr <|
(nonsingular_of_Z_ne_zero hPz).mp hP

lemma nonsingular_neg {P : Fin 3 → F} (hP : W.Nonsingular P) : W.Nonsingular <| W.neg P := by
by_cases hPz : P z = 0
Expand Down Expand Up @@ -1490,7 +1492,7 @@ namespace Point
lemma mk_point {P : PointClass R} (h : W'.NonsingularLift P) : (mk h).point = P :=
rfl

instance instZeroPoint [Nontrivial R] : Zero W'.Point :=
instance [Nontrivial R] : Zero W'.Point :=
⟨⟨nonsingularLift_zero⟩⟩

lemma zero_def [Nontrivial R] : (0 : W'.Point) = ⟨nonsingularLift_zero⟩ :=
Expand Down Expand Up @@ -1523,7 +1525,7 @@ Given a nonsingular Jacobian point `P` on `W`, use `-P` instead of `neg P`. -/
def neg (P : W.Point) : W.Point :=
⟨nonsingularLift_negMap P.nonsingular⟩

instance instNegPoint : Neg W.Point :=
instance : Neg W.Point :=
⟨neg⟩

lemma neg_def (P : W.Point) : -P = P.neg :=
Expand All @@ -1538,7 +1540,7 @@ Given two nonsingular Jacobian points `P` and `Q` on `W`, use `P + Q` instead of
noncomputable def add (P Q : W.Point) : W.Point :=
⟨nonsingularLift_addMap P.nonsingular Q.nonsingular⟩

noncomputable instance instAddPoint : Add W.Point :=
noncomputable instance : Add W.Point :=
⟨add⟩

lemma add_def (P Q : W.Point) : P + Q = P.add Q :=
Expand Down
11 changes: 6 additions & 5 deletions Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -196,7 +196,7 @@ lemma comp_smul (f : R →+* S) (P : Fin 3 → R) (u : R) : f ∘ (u • P) = f
ext n; fin_cases n <;> simp only [smul_fin3, comp_fin3] <;> map_simp

/-- The equivalence setoid for a projective point representative on a Weierstrass curve. -/
scoped instance instSetoidPoint : Setoid <| Fin 3 → R :=
scoped instance : Setoid <| Fin 3 → R :=
MulAction.orbitRel Rˣ <| Fin 3 → R

variable (R) in
Expand Down Expand Up @@ -1320,7 +1320,8 @@ lemma neg_of_Z_ne_zero {P : Fin 3 → F} (hPz : P z ≠ 0) :

private lemma nonsingular_neg_of_Z_ne_zero {P : Fin 3 → F} (hP : W.Nonsingular P) (hPz : P z ≠ 0) :
W.Nonsingular ![P x / P z, W.toAffine.negY (P x / P z) (P y / P z), 1] :=
(nonsingular_some ..).mpr <| Affine.nonsingular_neg <| (nonsingular_of_Z_ne_zero hPz).mp hP
(nonsingular_some ..).mpr <| (Affine.nonsingular_neg ..).mpr <|
(nonsingular_of_Z_ne_zero hPz).mp hP

lemma nonsingular_neg {P : Fin 3 → F} (hP : W.Nonsingular P) : W.Nonsingular <| W.neg P := by
by_cases hPz : P z = 0
Expand Down Expand Up @@ -1567,7 +1568,7 @@ namespace Point
lemma mk_point {P : PointClass R} (h : W'.NonsingularLift P) : (mk h).point = P :=
rfl

instance instZeroPoint [Nontrivial R] : Zero W'.Point :=
instance [Nontrivial R] : Zero W'.Point :=
⟨⟨nonsingularLift_zero⟩⟩

lemma zero_def [Nontrivial R] : (0 : W'.Point) = ⟨nonsingularLift_zero⟩ :=
Expand Down Expand Up @@ -1600,7 +1601,7 @@ Given a nonsingular projective point `P` on `W`, use `-P` instead of `neg P`. -/
def neg (P : W.Point) : W.Point :=
⟨nonsingularLift_negMap P.nonsingular⟩

instance instNegPoint : Neg W.Point :=
instance : Neg W.Point :=
⟨neg⟩

lemma neg_def (P : W.Point) : -P = P.neg :=
Expand All @@ -1615,7 +1616,7 @@ Given two nonsingular projective points `P` and `Q` on `W`, use `P + Q` instead
noncomputable def add (P Q : W.Point) : W.Point :=
⟨nonsingularLift_addMap P.nonsingular Q.nonsingular⟩

noncomputable instance instAddPoint : Add W.Point :=
noncomputable instance : Add W.Point :=
⟨add⟩

lemma add_def (P Q : W.Point) : P + Q = P.add Q :=
Expand Down