A proper invertible ideal in the canonical idealization

Proved

Mathoverflow507128.idealization_construction_explicit

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

commutative-algebrainvertible-modulespicard-groups

Let $P$ be a proper invertible ideal of a commutative ring $D$ , and let $M$ be a $D$ -module with its canonical opposite action and central-scalar structure. If multiplication $M\otimes_D P\to M$ is injective, then the trivial square-zero extension $D\ltimes M$ has a proper invertible ideal.

Preamble

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

Formal statement

namespace Mathoverflow507128

universe u v

/-- Platform-safe explicit form of the square-zero idealization construction. -/
theorem idealization_construction_explicit
    (D : Type u) [CommRing D]
    (M : Type v) [AddCommGroup M] [Module D M]
    (P : Ideal D) [Module.Invertible D P]
    (hP : P ≠ ⊤)
    (hPM : Function.Injective (moduleIdealMul D M P)) :
    letI : Module Dᵐᵒᵖ M :=
      Module.compHom M ((RingHom.id D).fromOpposite mul_comm)
    letI : IsCentralScalar D M := ⟨fun _ _ => rfl⟩
    ∃ I : Ideal (TrivSqZeroExt D M),
      I ≠ ⊤ ∧ Module.Invertible (TrivSqZeroExt D M) I := by
  sorry

end Mathoverflow507128

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