Detector multiplication on pure tensors

Proved

CuspidalCubicInput.detectorMulEquiv_tmul

by wenxinzhang · Aug 31, 2026 · Mathlib c5ea003 (Lean v4.30.0)

commutative-algebrainvertible-modulespicard-groups

For the detector module and invertible point ideal of the cuspidal cubic, the constructed multiplication equivalence sends every pure tensor $m\otimes p$ to the scalar product $p m$ .

Preamble

import Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
import Mathlib.Analysis.Complex.Polynomial.Basic
import Mathlib.Algebra.Polynomial.Expand
import Mathlib.Algebra.Polynomial.Taylor
import Mathlib.RingTheory.PicardGroup
import Mathlib.LinearAlgebra.DirectSum.TensorProduct
import Definitions.Def_RybinP18_CuspidalCubicInput

open WeierstrassCurve
open WeierstrassCurve.Affine
open Polynomial
open scoped Polynomial.Bivariate
open scoped DirectSum

Formal statement

namespace CuspidalCubicInput

noncomputable section

















































































lemma detectorMulEquiv_tmul (m : detectorModule) (p : pointIdeal) :
    detectorMulEquiv
        (TensorProduct.tmul cusp.CoordinateRing m p) =
      (p.1 : cusp.CoordinateRing) • m := by
  sorry





end
end CuspidalCubicInput

Source

CUHK-Shenzhen AI Math Problem 18, https://rybindmitry.github.io/problems/18.html. Lean formalization by Patricia Purtill and Kenta Kitamura, discussed at https://github.com/google-deepmind/formal-conjectures/pull/4644#issuecomment-5089566133; staged from Kenta Kitamura's Apache-2.0 repository https://github.com/KitaKen1/mo507128-lean at commit e9507429c01c4288089e4af1c92a03b7d1e17f74.

View graph