English
The definition of toClass applied to the zero point is trivial as it maps to the zero element.
Русский
Определение toClass на нулевой точке тривиально: отображает в ноль.
LaTeX
$$$toClass(0) = 0$$$
Lean4
/-- 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
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 [← 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'_neg_mul h₂).symm
· simp only [add_some hxy]
exact (CoordinateRing.mk_XYIdeal'_mul_mk_XYIdeal' h₁ h₂ hxy).symm
