toClass_eq_zero — Mathlib

English

Let P be a point on the affine Weierstrass curve W. The class map κ sends P to zero if and only if P is the zero point of W.

Русский

Пусть P — точка на аффинной кривой Вейерштрасса W. Отображение класса κ отправляет P в ноль тогда и только тогда, когда P является нулевой точкой W.

LaTeX

$$$\kappa(P)=0 \iff P=0$$$

Lean4

theorem toClass_eq_zero (P : W.Point) : toClass P = 0 ↔ P = 0 :=
  by
  constructor
  · intro hP
    rcases P with (_ | ⟨h, _⟩)
    · rfl
    · rcases (ClassGroup.mk_eq_one_of_coe_ideal <| by rfl).mp hP with ⟨p, h0, hp⟩
      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 h).toLinearEquiv.finrank_eq, Module.finrank_self]
  · exact congr_arg toClass

Похожие утверждения