Right-sided span consequences of escape

The preceding file proves the scalar/unit-production kernel. This file records the next unconditional module step, with right-sided order visible: the free module Fin n → S is regarded as a left module over Sᵐᵒᵖ, so scalar multiplication by op a is right multiplication by a in S.

No claim is made here that a particular escape family produces the pure coordinate vectors. That is the remaining Stafford correction construction.

def AlgebraicAnalysis.EscapeSpan.rightMulVector {S : Type u_1} [Ring S] {n : ℕ} (v : Fin n → S) (a : S) : Fin n → S

Coordinatewise right multiplication in the free right S-module.

Equations

• AlgebraicAnalysis.EscapeSpan.rightMulVector v a i = v i * a

@[simp]

theorem AlgebraicAnalysis.EscapeSpan.rightMulVector_apply {S : Type u_1} [Ring S] {n : ℕ} (v : Fin n → S) (a : S) (i : Fin n) : rightMulVector v a i = v i * a

@[simp]

theorem AlgebraicAnalysis.EscapeSpan.op_smul_vector {S : Type u_1} [Ring S] {n : ℕ} (v : Fin n → S) (a : S) : MulOpposite.op a • v = rightMulVector v a

def AlgebraicAnalysis.EscapeSpan.commutatorVector {S : Type u_1} [Ring S] {n : ℕ} (x : S) (v : Fin n → S) : Fin n → S

Coordinatewise commutator with the distinguished escape coordinate.

Equations

• AlgebraicAnalysis.EscapeSpan.commutatorVector x v i = (AlgebraicAnalysis.Escape.commutator x) (v i)

@[simp]

theorem AlgebraicAnalysis.EscapeSpan.commutatorVector_apply {S : Type u_1} [Ring S] {n : ℕ} (x : S) (v : Fin n → S) (i : Fin n) : commutatorVector x v i = (Escape.commutator x) (v i)

@[simp]

theorem AlgebraicAnalysis.EscapeSpan.commutatorVector_iterate_apply {S : Type u_1} [Ring S] {n : ℕ} (x : S) (v : Fin n → S) (k : ℕ) (i : Fin n) : (commutatorVector x)^[k] v i = (⇑(Escape.commutator x))^[k] (v i)

theorem AlgebraicAnalysis.EscapeSpan.commutatorVector_mem {S : Type u_1} [Ring S] {n : ℕ} (H : Submodule Sᵐᵒᵖ (Fin n → S)) (x : S) (hleft : ∀ v ∈ H, (fun (i : Fin n) => x * v i) ∈ H) {v : Fin n → S} (hv : v ∈ H) : commutatorVector x v ∈ H

The key right-sided module consequence. A unit coordinate can be inverted on the right, so a pure vector single i u gives every single i a.

theorem AlgebraicAnalysis.EscapeSpan.single_mem_of_unit_single_mem {S : Type u_1} [Ring S] {n : ℕ} (H : Submodule Sᵐᵒᵖ (Fin n → S)) (i : Fin n) {u : S} (hu : IsUnit u) (hmem : Pi.single i u ∈ H) (a : S) : Pi.single i a ∈ H

theorem AlgebraicAnalysis.EscapeSpan.top_of_unit_singletons {S : Type u_1} [Ring S] {n : ℕ} (H : Submodule Sᵐᵒᵖ (Fin n → S)) (hunit : ∀ (i : Fin n), ∃ (u : S), IsUnit u ∧ Pi.single i u ∈ H) : H = ⊤

If a right S-submodule contains a pure unit vector in every coordinate, then it is the whole free right module. The proof uses the finite standard basis decomposition and never reverses the right-sided scalar order.