Cuspidal-cubic input for MathOverflow 507128

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

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

namespace CuspidalCubicInput

noncomputable section

def cusp : WeierstrassCurve.Affine ℂ := ⟨0, 0, 0, 0, 0⟩

example (x y : ℂ) :
    WeierstrassCurve.Affine.Equation cusp x y ↔ y ^ 2 = x ^ 3 := by
  rw [WeierstrassCurve.Affine.equation_iff]
  simp [cusp]

/-- The normalization map `ℂ[X,Y]/(Y²-X³) → ℂ[T]`, with
`X ↦ T²` and `Y ↦ T³`. -/
def normalize : cusp.CoordinateRing →+* ℂ[X] :=
  AdjoinRoot.lift (Polynomial.compRingHom ((X : ℂ[X]) ^ 2)) ((X : ℂ[X]) ^ 3) (by
    simp [cusp, WeierstrassCurve.Affine.polynomial]
    rw [Polynomial.eval₂_pow, Polynomial.eval₂_C]
    simp [Polynomial.coe_compRingHom_apply]
    ring)

@[simp]
lemma normalize_algebraMap (p : ℂ[X]) :
    normalize (algebraMap ℂ[X] cusp.CoordinateRing p) = p.comp ((X : ℂ[X]) ^ 2) := by
  simp [normalize, AdjoinRoot.algebraMap_eq, Polynomial.coe_compRingHom_apply]

@[simp]
lemma normalize_root :
    normalize (AdjoinRoot.root cusp.polynomial) = (X : ℂ[X]) ^ 3 := by
  simp [normalize]

@[simp]
lemma normalize_mk_Y :
    normalize (WeierstrassCurve.Affine.CoordinateRing.mk cusp Y) =
      (X : ℂ[X]) ^ 3 := by
  change normalize (AdjoinRoot.root cusp.polynomial) = (X : ℂ[X]) ^ 3
  exact normalize_root

lemma normalize_smul_basis (p q : ℂ[X]) :
    normalize (p • (1 : cusp.CoordinateRing) +
        q • WeierstrassCurve.Affine.CoordinateRing.mk cusp Y) =
      Polynomial.expand ℂ 2 p + Polynomial.expand ℂ 2 q * X ^ 3 := by
  simp only [Algebra.smul_def, map_add, map_mul, mul_one,
    normalize_mk_Y, Polynomial.expand_eq_comp_X_pow]
  rw [normalize_algebraMap, normalize_algebraMap]

lemma normalize_coeff_one (z : cusp.CoordinateRing) :
    (normalize z).coeff 1 = 0 := by
  obtain ⟨p, q, rfl⟩ :=
    WeierstrassCurve.Affine.CoordinateRing.exists_smul_basis_eq
      (W' := cusp) z
  rw [normalize_smul_basis, Polynomial.coeff_add,
    Polynomial.coeff_expand (by decide : 0 < 2)]
  simp [Polynomial.coeff_mul_X_pow']

lemma normalize_eq_zero_iff (z : cusp.CoordinateRing) :
    normalize z = 0 ↔ z = 0 := by
  obtain ⟨p, q, rfl⟩ :=
    WeierstrassCurve.Affine.CoordinateRing.exists_smul_basis_eq
      (W' := cusp) z
  constructor
  · rw [normalize_smul_basis]
    intro h
    have hq : q = 0 := by
      apply Polynomial.ext
      intro n
      have hc := congrArg (fun f : ℂ[X] ↦ f.coeff (2 * n + 3)) h
      simp only [Polynomial.coeff_add, Polynomial.coeff_zero,
        Polynomial.coeff_mul_X_pow] at hc
      have hpodd :
          (Polynomial.expand ℂ 2 p).coeff (2 * n + 3) = 0 := by
        rw [Polynomial.coeff_expand (by decide : 0 < 2)]
        rw [if_neg]
        intro hdiv
        obtain ⟨k, hk⟩ := hdiv
        omega
      rw [hpodd, zero_add, Polynomial.coeff_expand_mul'
        (by decide : 0 < 2)] at hc
      exact hc
    rw [hq, map_zero, zero_mul, add_zero] at h
    have hp : p = 0 :=
      (Polynomial.expand_eq_zero (R := ℂ) (by decide : 0 < 2)).mp h
    rw [hp, hq]
    simp
  · intro hzero
    rw [hzero]
    simp

lemma normalize_injective : Function.Injective normalize := by
  intro x y hxy
  apply sub_eq_zero.mp
  apply (normalize_eq_zero_iff (x - y)).mp
  rw [map_sub, hxy, sub_self]

@[simp]
lemma normalize_algebraMap_complex (c : ℂ) :
    normalize (algebraMap ℂ cusp.CoordinateRing c) = C c := by
  rw [show algebraMap ℂ cusp.CoordinateRing c =
      algebraMap ℂ[X] cusp.CoordinateRing (C c) by
        exact (IsScalarTower.algebraMap_apply ℂ ℂ[X]
          cusp.CoordinateRing c).symm]
  rw [normalize_algebraMap]
  simp

lemma exists_root_ne_one_of_coeff_one_eq_zero
    (f : ℂ[X]) (hf : f ≠ 0) (hdegree : f.degree ≠ 0)
    (hcoeff : f.coeff 1 = 0) :
    ∃ r : ℂ, r ≠ 1 ∧ f.eval r = 0 := by
  obtain ⟨r, hr⟩ := IsAlgClosed.exists_root f hdegree
  by_contra h
  push Not at h
  have hall : ∀ z : ℂ, Polynomial.IsRoot f z → z = 1 := by
    intro z hz
    by_contra hz1
    exact (h z hz1) hz
  have hroots :
      f.roots = Multiset.replicate f.roots.card (1 : ℂ) :=
    Multiset.eq_replicate_card.mpr fun z hz ↦
      hall z ((Polynomial.mem_roots hf).mp hz)
  have hfactor := (IsAlgClosed.splits f).eq_prod_roots
  rw [hroots] at hfactor
  simp only [Multiset.map_replicate, Multiset.prod_replicate] at hfactor
  rw [IsAlgClosed.card_roots_eq_natDegree] at hfactor
  have hn : 0 < f.natDegree :=
    Polynomial.natDegree_pos_iff_degree_pos.mpr
      (Polynomial.degree_pos_of_root hf hr)
  have hpow :
      (((X : ℂ[X]) - C 1) ^ f.natDegree).coeff 1 =
        (f.natDegree : ℂ) * (-1 : ℂ) ^ (f.natDegree - 1) := by
    rw [← Polynomial.taylor_zero (((X : ℂ[X]) - C 1) ^ f.natDegree),
      Polynomial.taylor_coeff_one, Polynomial.derivative_pow,
      Polynomial.derivative_X_sub_C, mul_one]
    simp
  have hlc : f.leadingCoeff ≠ 0 :=
    Polynomial.leadingCoeff_ne_zero.mpr hf
  have hcoeff_ne :
      f.coeff 1 ≠ 0 := by
    rw [hfactor, Polynomial.coeff_C_mul, hpow]
    exact mul_ne_zero hlc <| mul_ne_zero (Nat.cast_ne_zero.mpr hn.ne')
      (pow_ne_zero _ (by norm_num))
  exact hcoeff_ne hcoeff

lemma cusp_one_nonsingular :
    WeierstrassCurve.Affine.Nonsingular cusp (1 : ℂ) 1 := by
  rw [WeierstrassCurve.Affine.nonsingular_iff]
  simp [cusp, WeierstrassCurve.Affine.equation_iff]

def pointIdeal : Ideal cusp.CoordinateRing :=
  WeierstrassCurve.Affine.CoordinateRing.XYIdeal cusp 1 (C 1)



noncomputable def pointIdealUnit :
    (Submodule cusp.CoordinateRing cusp.FunctionField)ˣ :=
  FractionalIdeal.unitsMulEquivSubmodule
    (WeierstrassCurve.Affine.CoordinateRing.XYIdeal'
      cusp_one_nonsingular)

noncomputable def pointIdealToUnit :
    pointIdeal →ₗ[cusp.CoordinateRing] pointIdealUnit where
  toFun x :=
    ⟨algebraMap cusp.CoordinateRing cusp.FunctionField x.1, by
      change algebraMap cusp.CoordinateRing cusp.FunctionField x.1 ∈
        (pointIdeal :
          FractionalIdeal (nonZeroDivisors cusp.CoordinateRing)
            cusp.FunctionField)
      exact FractionalIdeal.mem_coeIdeal_of_mem _ x.2⟩
  map_add' x y := by
    apply Subtype.ext
    simp
  map_smul' r x := by
    apply Subtype.ext
    simp [Algebra.smul_def]

lemma pointIdealToUnit_bijective :
    Function.Bijective pointIdealToUnit := by
  constructor
  · intro x y hxy
    apply Subtype.ext
    apply IsFractionRing.injective cusp.CoordinateRing cusp.FunctionField
    exact congrArg Subtype.val hxy
  · intro y
    have hy : y.1 ∈
        (pointIdeal : FractionalIdeal (nonZeroDivisors cusp.CoordinateRing)
          cusp.FunctionField) := y.2
    obtain ⟨x, hx, hxy⟩ :=
      (FractionalIdeal.mem_coeIdeal
        (nonZeroDivisors cusp.CoordinateRing)).mp hy
    refine ⟨⟨x, hx⟩, ?_⟩
    apply Subtype.ext
    exact hxy

noncomputable def pointIdealLinearEquiv :
    pointIdeal ≃ₗ[cusp.CoordinateRing] pointIdealUnit :=
  LinearEquiv.ofBijective pointIdealToUnit pointIdealToUnit_bijective

noncomputable instance pointIdeal_invertible :
    Module.Invertible cusp.CoordinateRing pointIdeal :=
  Module.Invertible.congr pointIdealLinearEquiv.symm

def evalAt (r : ℂ) : cusp.CoordinateRing →+* ℂ :=
  (Polynomial.evalRingHom r).comp normalize

@[simp]
lemma evalAt_algebraMap (r c : ℂ) :
    evalAt r (algebraMap ℂ cusp.CoordinateRing c) = c := by
  rw [show algebraMap ℂ cusp.CoordinateRing c =
      algebraMap ℂ[X] cusp.CoordinateRing (C c) by
        exact (IsScalarTower.algebraMap_apply ℂ ℂ[X]
          cusp.CoordinateRing c).symm]
  rw [evalAt, RingHom.comp_apply, normalize_algebraMap]
  simp

@[simp]
lemma evalAt_XClass (r : ℂ) :
    evalAt r
        (WeierstrassCurve.Affine.CoordinateRing.XClass cusp 1) =
      r ^ 2 - 1 := by
  simp [evalAt, normalize,
    WeierstrassCurve.Affine.CoordinateRing.XClass,
    WeierstrassCurve.Affine.CoordinateRing.mk]

@[simp]
lemma evalAt_YClass (r : ℂ) :
    evalAt r
        (WeierstrassCurve.Affine.CoordinateRing.YClass cusp (C 1)) =
      r ^ 3 - 1 := by
  simp [evalAt, normalize,
    WeierstrassCurve.Affine.CoordinateRing.YClass,
    WeierstrassCurve.Affine.CoordinateRing.mk]

def AwayPoint := {r : ℂ // r ≠ 1}

noncomputable instance : DecidableEq AwayPoint :=
  Classical.decEq _

def Fiber (_ : AwayPoint) := ℂ

instance (r : AwayPoint) : Field (Fiber r) :=
  inferInstanceAs (Field ℂ)

instance (r : AwayPoint) : Algebra cusp.CoordinateRing (Fiber r) :=
  RingHom.toAlgebra (evalAt r.1)

abbrev detectorModule :=
  ⨁ r : AwayPoint, Fiber r

noncomputable def pointIdealX : pointIdeal :=
  ⟨WeierstrassCurve.Affine.CoordinateRing.XClass cusp 1, by
    change WeierstrassCurve.Affine.CoordinateRing.XClass cusp 1 ∈
      Ideal.span
        {WeierstrassCurve.Affine.CoordinateRing.XClass cusp 1,
          WeierstrassCurve.Affine.CoordinateRing.YClass cusp (C 1)}
    apply Ideal.subset_span
    simp⟩

noncomputable def pointIdealY : pointIdeal :=
  ⟨WeierstrassCurve.Affine.CoordinateRing.YClass cusp (C 1), by
    change WeierstrassCurve.Affine.CoordinateRing.YClass cusp (C 1) ∈
      Ideal.span
        {WeierstrassCurve.Affine.CoordinateRing.XClass cusp 1,
          WeierstrassCurve.Affine.CoordinateRing.YClass cusp (C 1)}
    apply Ideal.subset_span
    simp⟩



lemma exists_pointIdeal_eval_one (r : AwayPoint) :
    ∃ p : pointIdeal,
      algebraMap cusp.CoordinateRing (Fiber r) p.1 = 1 := by
  by_cases hx : r.1 ^ 2 - 1 = 0
  · have hy : r.1 ^ 3 - 1 ≠ 0 := by
      intro hy
      apply r.2
      have hr2 : r.1 ^ 2 = 1 := sub_eq_zero.mp hx
      have hr3 : r.1 ^ 3 = 1 := sub_eq_zero.mp hy
      calc
        r.1 = r.1 * 1 := (mul_one _).symm
        _ = r.1 * r.1 ^ 2 := by rw [hr2]
        _ = r.1 ^ 3 := by ring
        _ = 1 := hr3
    let c : ℂ := (r.1 ^ 3 - 1)⁻¹
    let p : pointIdeal :=
      ⟨algebraMap ℂ cusp.CoordinateRing c * pointIdealY.1,
        pointIdeal.mul_mem_left _ pointIdealY.2⟩
    refine ⟨p, ?_⟩
    change evalAt r.1
      (algebraMap ℂ cusp.CoordinateRing c * pointIdealY.1) = 1
    rw [map_mul, evalAt_algebraMap]
    change (r.1 ^ 3 - 1)⁻¹ *
      evalAt r.1
        (WeierstrassCurve.Affine.CoordinateRing.YClass cusp (C 1)) = 1
    rw [evalAt_YClass, inv_mul_cancel₀ hy]
  · let c : ℂ := (r.1 ^ 2 - 1)⁻¹
    let p : pointIdeal :=
      ⟨algebraMap ℂ cusp.CoordinateRing c * pointIdealX.1,
        pointIdeal.mul_mem_left _ pointIdealX.2⟩
    refine ⟨p, ?_⟩
    change evalAt r.1
      (algebraMap ℂ cusp.CoordinateRing c * pointIdealX.1) = 1
    rw [map_mul, evalAt_algebraMap]
    change (r.1 ^ 2 - 1)⁻¹ *
      evalAt r.1
        (WeierstrassCurve.Affine.CoordinateRing.XClass cusp 1) = 1
    rw [evalAt_XClass, inv_mul_cancel₀ hx]

noncomputable def fiberMul (r : AwayPoint) :
    TensorProduct cusp.CoordinateRing (Fiber r) pointIdeal
      →ₗ[Fiber r] Fiber r :=
  TensorProduct.AlgebraTensorModule.lift
    { toFun := fun m =>
        { toFun := fun p =>
            algebraMap cusp.CoordinateRing (Fiber r) p.1 * m
          map_add' := by
            intro x y
            simp [add_mul]
          map_smul' := by
            intro d p
            simp [Algebra.smul_def, mul_assoc] }
      map_add' := by
        intro x y
        ext p
        simp [mul_add]
      map_smul' := by
        intro c m
        ext p
        change algebraMap cusp.CoordinateRing (Fiber r) p.1 * (c * m) =
          c * (algebraMap cusp.CoordinateRing (Fiber r) p.1 * m)
        ring }

@[simp]
lemma fiberMul_tmul (r : AwayPoint) (m : Fiber r) (p : pointIdeal) :
    fiberMul r (TensorProduct.tmul cusp.CoordinateRing m p) =
      algebraMap cusp.CoordinateRing (Fiber r) p.1 * m :=
  rfl

lemma fiberMul_surjective (r : AwayPoint) :
    Function.Surjective (fiberMul r) := by
  obtain ⟨p, hp⟩ := exists_pointIdeal_eval_one r
  intro z
  refine ⟨TensorProduct.tmul cusp.CoordinateRing z p, ?_⟩
  rw [fiberMul_tmul, hp, one_mul]

lemma fiberMul_bijective (r : AwayPoint) :
    Function.Bijective (fiberMul r) :=
  Module.Invertible.bijective_of_surjective (fiberMul_surjective r)

noncomputable def fiberMulEquiv (r : AwayPoint) :
    TensorProduct cusp.CoordinateRing (Fiber r) pointIdeal
      ≃ₗ[cusp.CoordinateRing] Fiber r :=
  (LinearEquiv.ofBijective (fiberMul r) (fiberMul_bijective r)).restrictScalars
    cusp.CoordinateRing

noncomputable def detectorMulEquiv :
    TensorProduct cusp.CoordinateRing detectorModule pointIdeal
      ≃ₗ[cusp.CoordinateRing] detectorModule :=
  TensorProduct.directSumLeft cusp.CoordinateRing cusp.CoordinateRing
      Fiber pointIdeal ≪≫ₗ
    DirectSum.congrLinearEquiv fiberMulEquiv







end
end CuspidalCubicInput