Square-zero idealization machinery for MathOverflow 507128

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

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

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

local notation "R" => TrivSqZeroExt D M

/-- The bilinear multiplication map whose tensor lift sends `r ⊗ p` to
`r * algebraMap D R p`. -/
def baseIdealMul (P : Ideal D) : R →ₗ[R] P →ₗ[D] R where
  toFun r :=
    { toFun := fun p => r * algebraMap D R p.1
      map_add' := by
        intro x y
        simp only [Submodule.coe_add, map_add, mul_add]
      map_smul' := by
        intro d p
        simp [Algebra.smul_def, mul_left_comm] }
  map_add' := by
    intro x y
    ext p <;> simp [add_mul]
  map_smul' := by
    intro r x
    apply LinearMap.ext
    intro p
    change (r * x) * algebraMap D R (p : D) =
      r * (x * algebraMap D R (p : D))
    rw [mul_assoc]

/-- Extension of the ideal `P` to the trivial square-zero extension. -/
def baseIdealMap (P : Ideal D) :
    TensorProduct D (TrivSqZeroExt D M) P →ₗ[TrivSqZeroExt D M]
      TrivSqZeroExt D M :=
  TensorProduct.AlgebraTensorModule.lift (baseIdealMul D M P)

/-- Multiplication `M ⊗[D] P → M`.  For the proposed direct sum `M`, this is an
isomorphism component by component. -/
def moduleIdealMul (P : Ideal D) : TensorProduct D M P →ₗ[D] M :=
  TensorProduct.lift
    { toFun := fun m =>
        { toFun := fun p => (p : D) • m
          map_add' := by
            intro x y
            simp [add_smul]
          map_smul' := by
            intro d p
            simp [mul_smul] }
      map_add' := by
        intro x y
        apply LinearMap.ext
        intro p
        simp [smul_add]
      map_smul' := by
        intro d m
        apply LinearMap.ext
        intro p
        change (p : D) • (d • m) = d • ((p : D) • m)
        exact smul_comm _ _ _ }

@[simp]
theorem moduleIdealMul_tmul (P : Ideal D) (m : M) (p : P) :
    moduleIdealMul D M P (TensorProduct.tmul D m p) = (p : D) • m := rfl

/-- The additive identification of a trivial square-zero extension with a product. -/
def toProdLinearEquiv : R ≃ₗ[D] D × M where
  toFun x := (x.fst, x.snd)
  invFun x := (x.1, x.2)
  left_inv _ := rfl
  right_inv _ := rfl
  map_add' _ _ := rfl
  map_smul' _ _ := rfl

/-- Splitting `(D ⋉ M) ⊗ P` into `(D ⊗ P) × (M ⊗ P)`. -/
def splitTensor (P : Ideal D) :
    TensorProduct D R P ≃ₗ[D]
      (TensorProduct D D P) × (TensorProduct D M P) :=
  TensorProduct.congr (toProdLinearEquiv D M) (LinearEquiv.refl D P) ≪≫ₗ
    TensorProduct.prodLeft D D D M P

@[simp]
theorem splitTensor_tmul (P : Ideal D) (r : R) (p : P) :
    splitTensor D M P (TensorProduct.tmul D r p) =
      (TensorProduct.tmul D r.fst p, TensorProduct.tmul D r.snd p) := rfl

@[simp]
theorem baseIdealMap_tmul (P : Ideal D) (r : R) (p : P) :
    baseIdealMap D M P (TensorProduct.tmul D r p) =
      r * algebraMap D R p.1 := rfl

theorem baseIdealMap_fst (P : Ideal D) (x : TensorProduct D R P) :
    (baseIdealMap D M P x).fst =
      TensorProduct.lid D P (splitTensor D M P x).1 := by
  refine TensorProduct.induction_on x ?_ ?_ ?_
  · simp
  · intro r p
    rw [baseIdealMap_tmul, splitTensor_tmul]
    simp only [TrivSqZeroExt.fst_mul, TensorProduct.lid_tmul,
      TrivSqZeroExt.algebraMap_eq_inl, TrivSqZeroExt.fst_inl,
      Submodule.coe_smul_of_tower, Algebra.smul_def,
      Algebra.algebraMap_self_apply]
  · intro x y hx hy
    simpa using congrArg₂ (· + ·) hx hy

theorem baseIdealMap_snd (P : Ideal D) (x : TensorProduct D R P) :
    (baseIdealMap D M P x).snd =
      moduleIdealMul D M P (splitTensor D M P x).2 := by
  refine TensorProduct.induction_on x ?_ ?_ ?_
  · simp
  · intro r p
    change r.fst • (0 : M) + (p : D) • r.snd = (p : D) • r.snd
    simp
  · intro x y hx hy
    simpa using congrArg₂ (· + ·) hx hy

/-- Injectivity of `M ⊗ P → M` implies injectivity of
`(D ⋉ M) ⊗ P → D ⋉ M`. -/
theorem baseIdealMap_injective (P : Ideal D)
    (hPM : Function.Injective (moduleIdealMul D M P)) :
    Function.Injective (baseIdealMap D M P) := by
  intro x y hxy
  apply (splitTensor D M P).injective
  apply Prod.ext
  · apply (TensorProduct.lid D P).injective
    apply Subtype.ext
    rw [← baseIdealMap_fst D M P, ← baseIdealMap_fst D M P]
    exact congrArg TrivSqZeroExt.fst hxy
  · apply hPM
    rw [← baseIdealMap_snd D M P, ← baseIdealMap_snd D M P, hxy]









/-- The exact input needed by the idealization argument. -/
def IdealizationInput : Prop :=
  ∃ (D : Type) (_ : CommRing D)
    (M : Type) (_ : AddCommGroup M) (_ : Module D M)
    (P : Ideal D) (_ : Module.Invertible D P),
      P ≠ ⊤ ∧
      Function.Injective (moduleIdealMul D M P) ∧
      ∀ a : D, ¬ IsUnit a → ∃ m : M, m ≠ 0 ∧ a • m = 0



end Mathoverflow507128

namespace Mathoverflow507128



end Mathoverflow507128