A proper invertible ideal in a square-zero idealization

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_idealization_construction_1 : Module Dᵐᵒᵖ M :=
  Module.compHom M ((RingHom.id D).fromOpposite mul_comm)

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

local notation "R" => TrivSqZeroExt D M



























/-- The square-zero idealization argument.  The desired ideal is the range of
`(D ⋉ M) ⊗[D] P → D ⋉ M`. -/
theorem idealization_construction
    (P : Ideal D) [Module.Invertible D P]
    (hP : P ≠ ⊤)
    (hPM : Function.Injective (moduleIdealMul D M P)) :
    ∃ I : Ideal R, I ≠ ⊤ ∧ Module.Invertible R I := by
  sorry







end Mathoverflow507128

namespace Mathoverflow507128



end Mathoverflow507128