English
The left and right inverses of the affine add equivalence agree with addition.
Русский
Левый и правый обратные к эквиваленции сложения согласованы с операцией сложения.
LaTeX
$$$toAffineAddEquiv(W)$.left_inv and $.right_inv behave with add$$
Lean4
/-- The addition-preserving equivalence between the type of nonsingular Jacobian points on a
Weierstrass curve `W` and the type of nonsingular points `W⟮F⟯` in affine coordinates. -/
@[simps]
noncomputable def toAffineAddEquiv [DecidableEq F] : W.Point ≃+ W.toAffine.Point
where
toFun := toAffineLift
invFun := fromAffine
left_inv := by
rintro @⟨⟨P⟩, hP⟩
by_cases hPz : P z = 0
· rw [Point.ext_iff, toAffineLift_eq, toAffine_of_Z_eq_zero hPz]
exact Quotient.eq.mpr <| Setoid.symm <| equiv_zero_of_Z_eq_zero hP hPz
· rw [Point.ext_iff, toAffineLift_eq, toAffine_of_Z_ne_zero hP hPz]
exact Quotient.eq.mpr <| Setoid.symm <| equiv_some_of_Z_ne_zero hPz
right_inv := by
rintro (_ | _)
· rw [← Affine.Point.zero_def, fromAffine_zero, toAffineLift_zero]
· rw [fromAffine_some, toAffineLift_some]
map_add' := toAffineLift_add
