Coordinate subspaces in literal string modules

The displayed arrow maps of a literal string module are partial injections on the position basis. Consequently images and preimages of coordinate subspaces are again coordinate subspaces. This file propagates that fact through the Butler--Ringel boundary filters and detector operations.

The resulting closure under individual coordinate parts is the linear-algebra bridge from detector vectors to the word-position occurrence calculation.

def MagnitudeConjecture.BoundQuiver.StringWord.Word.IsCoordinateSubspace {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (D : Word R) {x : Q} (U : Submodule k (D.Space x)) : Prop

A subspace of a position space is coordinate when it contains every individual coordinate part of each of its elements.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.mem_of_all_coordinateParts_mem {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (D : Word R) {x : Q} (U : Submodule k (D.Space x)) (v : D.Space x) (hparts : ∀ (i : D.PositionAt x), Finsupp.single i (v i) ∈ U) : v ∈ U

A vector belongs to a subspace once all of its individual coordinate parts do.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.isCoordinateSubspace_bot {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (D : Word R) (x : Q) : D.IsCoordinateSubspace ⊥

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.isCoordinateSubspace_top {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (D : Word R) (x : Q) : D.IsCoordinateSubspace ⊤

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.IsCoordinateSubspace.inf {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (D : Word R) {x : Q} {U V : Submodule k (D.Space x)} (hU : D.IsCoordinateSubspace U) (hV : D.IsCoordinateSubspace V) : D.IsCoordinateSubspace (U ⊓ V)

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.IsCoordinateSubspace.sup {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (D : Word R) {x : Q} {U V : Submodule k (D.Space x)} (hU : D.IsCoordinateSubspace U) (hV : D.IsCoordinateSubspace V) : D.IsCoordinateSubspace (U ⊔ V)

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.IsCoordinateSubspace.map_arrowLinearMap {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (D : Word R) {x y : Q} {U : Submodule k (D.Space x)} (hU : D.IsCoordinateSubspace U) (a : x ⟶ y) : D.IsCoordinateSubspace (Submodule.map (D.arrowLinearMap a) U)

Direct image under a displayed arrow preserves coordinate subspaces.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.IsCoordinateSubspace.comap_arrowLinearMap {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (D : Word R) {x y : Q} {U : Submodule k (D.Space y)} (hU : D.IsCoordinateSubspace U) (a : x ⟶ y) : D.IsCoordinateSubspace (Submodule.comap (D.arrowLinearMap a) U)

Preimage under a displayed arrow preserves coordinate subspaces.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.signedArrowSubspace_coordinatePart {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (D : Word R) (hmono : IsMonomial R) {x y : Q} (e : SignedArrow x y) {U : Submodule k (D.Space x)} (hU : D.IsCoordinateSubspace U) (v : D.Space y) (hv : v ∈ signedArrowSubspace (D.rightModule hmono) e U) (j : D.PositionAt y) : Finsupp.single j (v j) ∈ signedArrowSubspace (D.rightModule hmono) e U

Taking an individual coordinate part commutes with membership after transport across one signed arrow in a literal string module.

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.signedPathSubspace_coordinatePart {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (D : Word R) (hmono : IsMonomial R) {x y : Q} (p : SignedPath x y) {U : Submodule k (D.Space x)} : D.IsCoordinateSubspace U → ∀ v ∈ signedPathSubspace (D.rightModule hmono) p U, ∀ (j : D.PositionAt y), Finsupp.single j (v j) ∈ signedPathSubspace (D.rightModule hmono) p U

Taking an individual coordinate part commutes with membership after transport along a signed path in a literal string module.

theorem MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.lowerBoundarySubspace_isCoordinate_rightModule {k Q : Type u} [Field k] [Quiver Q] {A : Type u} [Ring A] [Algebra k A] [Fintype Q] [(x y : Q) → Fintype (x ⟶ y)] {P : StringPresentation k A Q} {S : P.ArrowPolarization} {u₀ : Q} {t : Bool} (D : Word P.relations) (C : EndpointWord S u₀ t) : D.IsCoordinateSubspace (lowerBoundarySubspace (D.rightModule ⋯) C)

Every lower boundary filter is coordinate in a literal string module.

theorem MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.upperBoundarySubspace_isCoordinate_rightModule {k Q : Type u} [Field k] [Quiver Q] {A : Type u} [Ring A] [Algebra k A] [Fintype Q] [(x y : Q) → Fintype (x ⟶ y)] {P : StringPresentation k A Q} {S : P.ArrowPolarization} {u₀ : Q} {t : Bool} (D : Word P.relations) (C : EndpointWord S u₀ t) : D.IsCoordinateSubspace (upperBoundarySubspace (D.rightModule ⋯) C)

Every upper boundary filter is coordinate in a literal string module.

theorem MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.lowerSubspace_isCoordinate_rightModule {k Q : Type u} [Field k] [Quiver Q] {A : Type u} [Ring A] [Algebra k A] [Fintype Q] [(x y : Q) → Fintype (x ⟶ y)] {P : StringPresentation k A Q} {S : P.ArrowPolarization} {u₀ : Q} {t : Bool} (D : Word P.relations) (C : EndpointWord S u₀ t) : D.IsCoordinateSubspace (lowerSubspace (D.rightModule ⋯) C)

Every lower word subspace is coordinate in a literal string module.

theorem MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.upperSubspace_isCoordinate_rightModule {k Q : Type u} [Field k] [Quiver Q] {A : Type u} [Ring A] [Algebra k A] [Fintype Q] [(x y : Q) → Fintype (x ⟶ y)] {P : StringPresentation k A Q} {S : P.ArrowPolarization} {u₀ : Q} {t : Bool} (D : Word P.relations) (C : EndpointWord S u₀ t) : D.IsCoordinateSubspace (upperSubspace (D.rightModule ⋯) C)

Every upper word subspace is coordinate in a literal string module.

theorem MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.detectorNumerator_isCoordinate_rightModule {k Q : Type u} [Field k] [Quiver Q] {A : Type u} [Ring A] [Algebra k A] [Fintype Q] [(x y : Q) → Fintype (x ⟶ y)] {P : StringPresentation k A Q} {S : P.ArrowPolarization} {u₀ : Q} {t : Bool} (D : Word P.relations) (C : EndpointWord S u₀ t) : D.IsCoordinateSubspace (detectorNumerator (D.rightModule ⋯) C)

The detector numerator is coordinate on every literal string module.

theorem MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.detectorDenominator_isCoordinate_rightModule {k Q : Type u} [Field k] [Quiver Q] {A : Type u} [Ring A] [Algebra k A] [Fintype Q] [(x y : Q) → Fintype (x ⟶ y)] {P : StringPresentation k A Q} {S : P.ArrowPolarization} {u₀ : Q} {t : Bool} (D : Word P.relations) (C : EndpointWord S u₀ t) : D.IsCoordinateSubspace (detectorDenominator (D.rightModule ⋯) C)

The detector denominator is coordinate on every literal string module.