Abstract two-simplicity transfer

This file records the ring-theoretic transfer from a principal-right-quotient torsion statement to two-simplicity. It does not assert the localization or rank theorem needed to produce that torsion statement.

def AlgebraicAnalysis.TwoSimplicity.TwoSimple (R : Type u_3) [Ring R] : Prop

The two-sided coefficient identity used for two-simplicity.

Equations

• AlgebraicAnalysis.TwoSimplicity.TwoSimple R = ∀ (d₁ d₂ : R), d₁ ≠ 0 → d₂ ≠ 0 → ∃ (f : R) (g : R) (u : R) (v : R), f * d₁ * u + g * d₂ * v = 1

structure AlgebraicAnalysis.TwoSimplicity.FiniteTorsionFreeExtension {Λ : Type u_1} {Γ : Type u_2} [Ring Λ] [Ring Γ] (ι : Λ →+* Γ) : Prop

Finite, torsion-free bimodule extension data with written orders visible.

• injective : Function.Injective ⇑ι
• rightFinite : ∃ (n : ℕ) (basis : Fin n → Γ), ∀ (x : Γ), ∃ (a : Fin n → Λ), x = ∑ i : Fin n, basis i * ι (a i)
• leftFinite : ∃ (n : ℕ) (basis : Fin n → Γ), ∀ (x : Γ), ∃ (a : Fin n → Λ), x = ∑ i : Fin n, ι (a i) * basis i
• rightTorsionFree (a : Λ) : a ≠ 0 → ∀ (x : Γ), x * ι a = 0 → x = 0
• leftTorsionFree (a : Λ) : a ≠ 0 → ∀ (x : Γ), ι a * x = 0 → x = 0

def AlgebraicAnalysis.TwoSimplicity.PrincipalRightQuotientTorsion {Λ : Type u_1} {Γ : Type u_2} [Ring Λ] [Ring Γ] (ι : Λ →+* Γ) : Prop

The exact class-of-1 torsion statement needed by the transfer.

Equations

• AlgebraicAnalysis.TwoSimplicity.PrincipalRightQuotientTorsion ι = ∀ (d : Γ), d ≠ 0 → ∃ (a : Λ), a ≠ 0 ∧ ∃ (w : Γ), ι a = d * w

theorem AlgebraicAnalysis.TwoSimplicity.twoSimple_of_principalRightQuotientTorsion {Λ : Type u_1} {Γ : Type u_2} [Ring Λ] [Ring Γ] (ι : Λ →+* Γ) (hΛ : TwoSimple Λ) (hquot : PrincipalRightQuotientTorsion ι) : TwoSimple Γ

Two-simplicity transfers along a ring map once the principal right-quotient torsion condition is supplied. Producing that condition is a separate localization/rank theorem.