The scalar-torsion ideal of an algebra

The elements of a commutative algebra killed by a regular scalar form an ideal. Its underlying scalar submodule is Mathlib's torsion submodule, and its quotient is torsion-free over a domain. This ideal is useful for constructing flat closures of affine group schemes over Dedekind domains.

The construction uses Submodule.torsion and the quotient-torsion argument from Mathlib.Algebra.Module.Torsion.Basic.

def TauCeti.scalarTorsionIdeal (R : Type u) [CommRing R] (A : Type v) [CommRing A] [Algebra R A] : Ideal A

The ideal of elements annihilated by a non-zero-divisor of the scalar ring.

Equations

• TauCeti.scalarTorsionIdeal R A = { toAddSubmonoid := (Submodule.torsion R A).toAddSubmonoid, smul_mem' := ⋯ }

@[simp]

theorem TauCeti.mem_scalarTorsionIdeal (R : Type u) [CommRing R] (A : Type v) [CommRing A] [Algebra R A] {x : A} : x ∈ scalarTorsionIdeal R A ↔ ∃ (r : ↥(nonZeroDivisors R)), r • x = 0

Scalar-torsion ideal membership is annihilation by a regular scalar.

@[simp]

theorem TauCeti.scalarTorsionIdeal_restrictScalars (R : Type u) [CommRing R] (A : Type v) [CommRing A] [Algebra R A] : Submodule.restrictScalars R (scalarTorsionIdeal R A) = Submodule.torsion R A

The scalar submodule underlying the scalar-torsion ideal is the torsion submodule.

instance TauCeti.isTorsionFree_quotient_scalarTorsionIdeal (R : Type u) [CommRing R] (A : Type v) [CommRing A] [Algebra R A] [IsDomain R] : Module.IsTorsionFree R (A ⧸ scalarTorsionIdeal R A)

Quotienting an algebra by its scalar-torsion ideal gives a torsion-free scalar module.