Explicit idealization input from the cuspidal cubic

import Mathlib.Algebra.TrivSqZeroExt.Basic
import Mathlib.LinearAlgebra.TensorProduct.Prod
import Mathlib.RingTheory.Localization.FractionRing
import Mathlib.RingTheory.PicardGroup
import Definitions.Def_RybinP18_CuspidalCubicInput
import Definitions.Def_RybinP18_MO507128

/-!
# MathOverflow 507128: the idealization step

This file deliberately does not import or clone `formal-conjectures`.  It copies the
statement of the target theorem and proves the square-zero idealization argument using
mathlib.

The input for the idealization is constructed explicitly from the cuspidal cubic
`Y² = X³`.  Thus the final `#print axioms` contains no problem-specific axiom.
-/

namespace Mathoverflow507128

universe u v

variable (D : Type u) [CommRing D]
variable (M : Type v) [AddCommGroup M] [Module D M]

local instance p2m_Theorems_Thm_Mathoverflow507128_idealizationInput_explicit_1 : Module Dᵐᵒᵖ M :=
  Module.compHom M ((RingHom.id D).fromOpposite mul_comm)

local instance p2m_Theorems_Thm_Mathoverflow507128_idealizationInput_explicit_2 : IsCentralScalar D M := ⟨fun _ _ => rfl⟩

local notation "R" => TrivSqZeroExt D M

































/-- The explicit cuspidal-cubic input:

* `D = ℂ[X,Y]/(Y²-X³) ≅ ℂ[t²,t³]`;
* `P = (X-1,Y-1)`;
* `M = ⨁ (r : ℂ), (r ≠ 1) → ℂ_r`, where `D` acts by evaluation
  `(X,Y) = (r²,r³)`.

The normalization argument in `CuspidalCubicInput` proves that every nonunit is
annihilated in some component with `r ≠ 1`. -/
theorem idealizationInput_explicit : IdealizationInput := by
  sorry

end Mathoverflow507128

namespace Mathoverflow507128



end Mathoverflow507128