Canonical idealization is a total quotient ring

Proved

Mathoverflow507128.isFractionRing_self_of_kills_nonunits_explicit

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

commutative-algebrainvertible-modulespicard-groups

Let $D$ be a commutative ring and $M$ a $D$ -module. Equip $M$ with the canonical opposite action and central-scalar structure. If every nonunit of $D$ annihilates a nonzero element of $M$ , then the trivial square-zero extension $D\ltimes M$ is a total ring of fractions of itself.

Preamble

import Mathlib.Algebra.TrivSqZeroExt.Basic
import Mathlib.RingTheory.Localization.FractionRing

Formal statement

namespace Mathoverflow507128

universe u v

/-- Platform-safe explicit form of the square-zero total-fraction-ring criterion. -/
theorem isFractionRing_self_of_kills_nonunits_explicit
    (D : Type u) [CommRing D]
    (M : Type v) [AddCommGroup M] [Module D M]
    (hkill : ∀ a : D, ¬ IsUnit a → ∃ m : M, m ≠ 0 ∧ a • m = 0) :
    letI : Module Dᵐᵒᵖ M :=
      Module.compHom M ((RingHom.id D).fromOpposite mul_comm)
    letI : IsCentralScalar D M := ⟨fun _ _ => rfl⟩
    IsFractionRing (TrivSqZeroExt D M) (TrivSqZeroExt D M) := 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