Scalar torsion in commutative Hopf algebras

Over a domain, scalar torsion is stable under the counit and antipode. If the tensor square of the torsion-free quotient is torsion-free, comultiplication also descends to that quotient, so the scalar-torsion ideal is a Hopf ideal. Over a Dedekind domain the tensor condition is automatic: torsion-free modules are flat, and the tensor product of flat modules is flat.

This constructs the flat closure of the generic fiber of an affine group scheme over a Dedekind domain. It also detects torsion in a subgroup generated by flat group schemes.

References

• The Stacks Project, Tag 0AUW, for flatness of torsion-free modules over Dedekind domains.

The Hopf-ideal construction follows TauCeti.HopfIdeal.reduction, replacing nilpotence by annihilation by a regular scalar. The module input is Mathlib's torsion-free quotient and Dedekind-domain flatness criterion.

noncomputable def TauCeti.HopfIdeal.scalarTorsion (R : Type u) [CommRing R] [IsDomain R] (H : Type v) [CommRing H] [HopfAlgebra R H] [Module.IsTorsionFree R (TensorProduct R (H ⧸ scalarTorsionIdeal R H) (H ⧸ scalarTorsionIdeal R H))] : HopfIdeal R H

The scalar-torsion ideal as a Hopf ideal, when the tensor square of its quotient is scalar-torsion-free. Over a Dedekind domain this condition holds automatically.

Equations

• TauCeti.HopfIdeal.scalarTorsion R H = TauCeti.HopfIdeal.ofIdeal (TauCeti.scalarTorsionIdeal R H) ⋯ ⋯ ⋯

@[simp]

theorem TauCeti.HopfIdeal.scalarTorsion_toIdeal (R : Type u) [CommRing R] [IsDomain R] (H : Type v) [CommRing H] [HopfAlgebra R H] [Module.IsTorsionFree R (TensorProduct R (H ⧸ scalarTorsionIdeal R H) (H ⧸ scalarTorsionIdeal R H))] : (scalarTorsion R H).toIdeal = scalarTorsionIdeal R H

The scalar-torsion Hopf ideal has the scalar-torsion ideal as its underlying ideal.

@[simp]

theorem TauCeti.HopfIdeal.mem_scalarTorsion (R : Type u) [CommRing R] [IsDomain R] (H : Type v) [CommRing H] [HopfAlgebra R H] [Module.IsTorsionFree R (TensorProduct R (H ⧸ scalarTorsionIdeal R H) (H ⧸ scalarTorsionIdeal R H))] {x : H} : x ∈ scalarTorsion R H ↔ ∃ (r : ↥(nonZeroDivisors R)), r • x = 0

Membership in the scalar-torsion Hopf ideal is annihilation by a regular scalar.

instance TauCeti.HopfIdeal.isTorsionFree_quotient_scalarTorsion (R : Type u) [CommRing R] [IsDomain R] (H : Type v) [CommRing H] [HopfAlgebra R H] [Module.IsTorsionFree R (TensorProduct R (H ⧸ scalarTorsionIdeal R H) (H ⧸ scalarTorsionIdeal R H))] : Module.IsTorsionFree R (H ⧸ (scalarTorsion R H).toIdeal)

The quotient by the scalar-torsion Hopf ideal is scalar-torsion-free.