Rank and torsion over Ore localizations

This file contains the part of handover packet 2 which is available without postulating a noncommutative flatness theorem. A right R-module is encoded as a left Rᵐᵒᵖ-module. When the right Ore condition needed for this localization holds, its Ore localization is a module over the division ring of fractions of Rᵐᵒᵖ; oreRank is the ordinary vector-space rank of that localization.

The pinned Mathlib has the Ore localization and its division-ring structure, but not the noncommutative tensor/localization exactness theorem (the commutative tensor-product exactness file explicitly lists this as TODO). Consequently this file proves the rank-nullity and torsion criteria for the localized division-ring module, and records the exact first missing bridge: that localization sends an arbitrary short exact sequence of right R-modules to a short exact sequence. No proposition in this file assumes that bridge or introduces an axiom for it.

The commutative-domain criterion rank_eq_zero_iff_isTorsion imported from Mathlib remains available, but is deliberately not reused as a theorem about noncommutative R.

Unconditional vector-space rank facts

theorem AlgebraicAnalysis.RankTorsion.rank_quotient_add_rank {Q : Type u} [DivisionRing Q] {V : Type v} [AddCommGroup V] [Module Q V] (P : Submodule Q V) : Module.rank Q (V ⧸ P) + Module.rank Q ↥P = Module.rank Q V

theorem AlgebraicAnalysis.RankTorsion.rank_eq_zero_iff_subsingleton {Q : Type u} [DivisionRing Q] {V : Type v} [AddCommGroup V] [Module Q V] : Module.rank Q V = 0 ↔ Subsingleton V

theorem AlgebraicAnalysis.RankTorsion.rank_eq_zero_iff_forall_zero {Q : Type u} [DivisionRing Q] {V : Type v} [AddCommGroup V] [Module Q V] : Module.rank Q V = 0 ↔ ∀ (v : V), v = 0

theorem AlgebraicAnalysis.RankTorsion.rank_eq_zero_iff_isTorsionOverDivisionRing {Q : Type u} [DivisionRing Q] {V : Type v} [AddCommGroup V] [Module Q V] : Module.rank Q V = 0 ↔ ∀ (v : V), ∃ (a : Q), a ≠ 0 ∧ a • v = 0

theorem AlgebraicAnalysis.RankTorsion.finrank_quotient_add_finrank {Q : Type u} [DivisionRing Q] {V : Type v} [AddCommGroup V] [Module Q V] [Module.Finite Q V] (P : Submodule Q V) : Module.finrank Q (V ⧸ P) + Module.finrank Q ↥P = Module.finrank Q V

theorem AlgebraicAnalysis.RankTorsion.rank_eq_of_surjective {Q : Type u} [DivisionRing Q] {V V' : Type v} [AddCommGroup V] [Module Q V] [AddCommGroup V'] [Module Q V'] (f : V →ₗ[Q] V') (hf : Function.Surjective ⇑f) : Module.rank Q V = Module.rank Q V' + Module.rank Q ↥f.ker

theorem AlgebraicAnalysis.RankTorsion.finrank_eq_of_surjective {Q : Type u} [DivisionRing Q] {V V' : Type v} [AddCommGroup V] [Module Q V] [AddCommGroup V'] [Module Q V'] [Module.Finite Q V] (f : V →ₗ[Q] V') (hf : Function.Surjective ⇑f) : Module.finrank Q V = Module.finrank Q V' + Module.finrank Q ↥f.ker

OreSet R⁰ is the left Ore condition. A right module is localized using the opposite ring, so the corresponding right Ore condition is represented by an explicit OreSet (Rᵐᵒᵖ)⁰ assumption. This is intentional: left Ore alone does not imply right Ore for a general domain.

@[reducible, inline]

abbrev AlgebraicAnalysis.RankTorsion.FractionRingOp (R : Type u) [Ring R] [OreLocalization.OreSet (nonZeroDivisors Rᵐᵒᵖ)] : Type u

The full Ore localization of the opposite coefficient ring.

Equations

• AlgebraicAnalysis.RankTorsion.FractionRingOp R = OreLocalization (nonZeroDivisors Rᵐᵒᵖ) Rᵐᵒᵖ

@[reducible, inline]

abbrev AlgebraicAnalysis.RankTorsion.LocalizedRightModule (R : Type u) (M : Type v) [Ring R] [OreLocalization.OreSet (nonZeroDivisors Rᵐᵒᵖ)] [AddCommGroup M] [Module Rᵐᵒᵖ M] : Type (max u v)

Localization of a right R-module, represented as a left opposite-module.

Equations

• AlgebraicAnalysis.RankTorsion.LocalizedRightModule R M = OreLocalization (nonZeroDivisors Rᵐᵒᵖ) M

noncomputable def AlgebraicAnalysis.RankTorsion.oreRank {R : Type u} [Ring R] [OreLocalization.OreSet (nonZeroDivisors Rᵐᵒᵖ)] (M : Type v) [AddCommGroup M] [Module Rᵐᵒᵖ M] : Cardinal.{max v u}

The rank of a right module after passage to the full fraction ring.

Equations

• AlgebraicAnalysis.RankTorsion.oreRank M = Module.rank (AlgebraicAnalysis.RankTorsion.FractionRingOp R) (AlgebraicAnalysis.RankTorsion.LocalizedRightModule R M)

theorem AlgebraicAnalysis.RankTorsion.oreRank_eq_rank_localized {R : Type u} [Ring R] [OreLocalization.OreSet (nonZeroDivisors Rᵐᵒᵖ)] {M : Type v} [AddCommGroup M] [Module Rᵐᵒᵖ M] : oreRank M = Module.rank (FractionRingOp R) (LocalizedRightModule R M)

theorem AlgebraicAnalysis.RankTorsion.oreRank_eq_of_localizedLinearEquiv {R : Type u} [Ring R] [OreLocalization.OreSet (nonZeroDivisors Rᵐᵒᵖ)] {M : Type v} [AddCommGroup M] [Module Rᵐᵒᵖ M] {N : Type v} [AddCommGroup N] [Module Rᵐᵒᵖ N] (e : LocalizedRightModule R M ≃ₗ[FractionRingOp R] LocalizedRightModule R N) : oreRank M = oreRank N

theorem AlgebraicAnalysis.RankTorsion.localized_oreDiv_one_eq_zero_iff {R : Type u} [Ring R] [OreLocalization.OreSet (nonZeroDivisors Rᵐᵒᵖ)] {M : Type v} [AddCommGroup M] [Module Rᵐᵒᵖ M] (m : M) : m /ₒ 1 = 0 ↔ ∃ (s : ↥(nonZeroDivisors Rᵐᵒᵖ)), s • m = 0

theorem AlgebraicAnalysis.RankTorsion.oreRank_zero_iff_localized_subsingleton {R : Type u} [Ring R] [Nontrivial R] [NoZeroDivisors R] [OreLocalization.OreSet (nonZeroDivisors Rᵐᵒᵖ)] {M : Type v} [AddCommGroup M] [Module Rᵐᵒᵖ M] : oreRank M = 0 ↔ Subsingleton (LocalizedRightModule R M)

theorem AlgebraicAnalysis.RankTorsion.oreRank_zero_iff_rightTorsion {R : Type u} [Ring R] [Nontrivial R] [NoZeroDivisors R] [OreLocalization.OreSet (nonZeroDivisors Rᵐᵒᵖ)] {M : Type v} [AddCommGroup M] [Module Rᵐᵒᵖ M] : oreRank M = 0 ↔ ∀ (m : M), ∃ (s : ↥(nonZeroDivisors Rᵐᵒᵖ)), s • m = 0

theorem AlgebraicAnalysis.RankTorsion.oreRank_zero_iff_localized_torsion {R : Type u} [Ring R] [Nontrivial R] [NoZeroDivisors R] [OreLocalization.OreSet (nonZeroDivisors Rᵐᵒᵖ)] {M : Type v} [AddCommGroup M] [Module Rᵐᵒᵖ M] : oreRank M = 0 ↔ ∀ (z : LocalizedRightModule R M), ∃ (a : FractionRingOp R), a ≠ 0 ∧ a • z = 0