Generic finite triangular denominator arguments

This file records the purely module-theoretic part of the triangular denominator argument. The coefficients act on the right, represented by scalars in Rᵐᵒᵖ; in particular (op s) • m means m * s.

There are two useful forms. First, a finite family of torsion generators has one common nonzero denominator, obtained from the finite intersection of their right annihilator ideals. Second, explicit denominator clearance through a finite filtration composes to denominator clearance for the whole quotient. The hypotheses describing the filtration are data, rather than an assertion that an arbitrary Ore extension is free or flat.

def AlgebraicAnalysis.TriangularDenominator.rightActionLinear {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module Rᵐᵒᵖ M] (m : M) : R →ₗ[Rᵐᵒᵖ] M

The right-action map associated to a vector.

Equations

• AlgebraicAnalysis.TriangularDenominator.rightActionLinear m = { toFun := fun (s : R) => MulOpposite.op s • m, map_add' := ⋯, map_smul' := ⋯ }

def AlgebraicAnalysis.TriangularDenominator.rightAnnihilator {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module Rᵐᵒᵖ M] (m : M) : Submodule Rᵐᵒᵖ R

The right annihilator of a vector, represented as a right ideal.

Equations

• AlgebraicAnalysis.TriangularDenominator.rightAnnihilator m = (AlgebraicAnalysis.TriangularDenominator.rightActionLinear m).ker

theorem AlgebraicAnalysis.TriangularDenominator.finite_vectors_common_annihilator {R : Type u} [Ring R] [IsDomain R] {M : Type v} [AddCommGroup M] [Module Rᵐᵒᵖ M] {n : ℕ} (g : Fin n → M) (hAnn : ∀ (i : Fin n), ∃ (s : R), s ≠ 0 ∧ MulOpposite.op s • g i = 0) (hOre : OreRightIntersection.RightOreCondition R) : ∃ (s : R), s ≠ 0 ∧ ∀ (i : Fin n), MulOpposite.op s • g i = 0

A finite family of torsion vectors admits one common nonzero denominator.

def AlgebraicAnalysis.TriangularDenominator.StepClearance {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module Rᵐᵒᵖ M] (F : ℕ → Submodule Rᵐᵒᵖ M) (i : ℕ) : Prop

One explicit denominator-clearing step of a filtration.

Equations

• AlgebraicAnalysis.TriangularDenominator.StepClearance F i = ∀ m ∈ F (i + 1), ∃ (s : R), s ≠ 0 ∧ MulOpposite.op s • m ∈ F i

theorem AlgebraicAnalysis.TriangularDenominator.filtration_clearance {R : Type u} [Ring R] [IsDomain R] {M : Type v} [AddCommGroup M] [Module Rᵐᵒᵖ M] (F : ℕ → Submodule Rᵐᵒᵖ M) (n : ℕ) (hstep : ∀ i < n, StepClearance F i) {m : M} (hm : m ∈ F n) : ∃ (s : R), s ≠ 0 ∧ MulOpposite.op s • m ∈ F 0

Iterating finitely many explicit triangular steps clears a denominator.

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

A finite cleared filtration makes the terminal quotient torsion.

Equations

• AlgebraicAnalysis.TriangularDenominator.IsTorsionRight N = ∀ (z : M ⧸ N), ∃ (s : R), s ≠ 0 ∧ MulOpposite.op s • z = 0

theorem AlgebraicAnalysis.TriangularDenominator.filtration_quotient_isTorsion {R : Type u} [Ring R] [IsDomain R] {M : Type v} [AddCommGroup M] [Module Rᵐᵒᵖ M] (F : ℕ → Submodule Rᵐᵒᵖ M) (n : ℕ) (hstep : ∀ i < n, StepClearance F i) (htop : F n = ⊤) : IsTorsionRight (F 0)