Generic denominator clearing and torsion quotients

This is the unconditional part of packet 9. It separates the algebraic quotient argument from the still-unformalized triangular PBW reduction. An explicit clearing witness for each vector implies torsion of the quotient; the principal right-ideal case is proved directly from the opposite Ore condition. No stage freeness or noncommutative flatness is postulated.

def AlgebraicAnalysis.DenominatorTorsion.IsTorsionRight {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module Rᵐᵒᵖ M] : Prop

Right-module torsion, with the right scalar displayed as op s.

Equations

• AlgebraicAnalysis.DenominatorTorsion.IsTorsionRight = ∀ (m : M), ∃ (s : R), s ≠ 0 ∧ MulOpposite.op s • m = 0

def AlgebraicAnalysis.DenominatorTorsion.HasDenominatorClearance {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module Rᵐᵒᵖ M] (N : Submodule Rᵐᵒᵖ M) : Prop

A denominator-clearing witness for a right submodule quotient.

Equations

• AlgebraicAnalysis.DenominatorTorsion.HasDenominatorClearance N = ∀ (m : M), ∃ (s : R), s ≠ 0 ∧ MulOpposite.op s • m ∈ N

theorem AlgebraicAnalysis.DenominatorTorsion.quotient_isTorsion_of_clearance {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module Rᵐᵒᵖ M] (N : Submodule Rᵐᵒᵖ M) (hclear : HasDenominatorClearance N) : IsTorsionRight

def AlgebraicAnalysis.DenominatorTorsion.leftMulLinear {R : Type u} [Ring R] (q : R) : R →ₗ[Rᵐᵒᵖ] R

Left multiplication by q is a right-R-linear map.

Equations

• AlgebraicAnalysis.DenominatorTorsion.leftMulLinear q = { toFun := fun (x : R) => q * x, map_add' := ⋯, map_smul' := ⋯ }

def AlgebraicAnalysis.DenominatorTorsion.principalRightIdeal {R : Type u} [Ring R] (q : R) : Submodule Rᵐᵒᵖ R

The right ideal qR, represented as the range of left multiplication.

Equations

• AlgebraicAnalysis.DenominatorTorsion.principalRightIdeal q = (AlgebraicAnalysis.DenominatorTorsion.leftMulLinear q).range

theorem AlgebraicAnalysis.DenominatorTorsion.principalRightIdeal_mem {R : Type u} [Ring R] (q x : R) : q * x ∈ principalRightIdeal q

theorem AlgebraicAnalysis.DenominatorTorsion.principal_quotient_isTorsion {R : Type u} [Ring R] [Nontrivial R] [NoZeroDivisors R] [OreLocalization.OreSet (nonZeroDivisors Rᵐᵒᵖ)] (q : R) (hq : q ≠ 0) : IsTorsionRight