Subspace transport along signed paths

The Butler--Ringel detecting functors propagate subspaces of a quiver representation along strings. Traversing an ordinary arrow takes the image of a subspace; traversing its formal inverse takes the preimage. This file packages that operation for the right-module convention of the bound path category and proves its elementary path calculus.

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.moduleArrowMap {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (N : CategoryTheory.Functor (Category R)ᵒᵖ (ModuleCat k)) {x y : Q} (a : x ⟶ y) : N.obj (Opposite.op (obj R x)) ⟶ N.obj (Opposite.op (obj R y))

The displayed linear map of an ordinary quiver arrow on a raw right module over the bound path category.

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.modulePathMap {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (N : CategoryTheory.Functor (Category R)ᵒᵖ (ModuleCat k)) {x y : Q} (p : Quiver.Path x y) : N.obj (Opposite.op (obj R x)) ⟶ N.obj (Opposite.op (obj R y))

The displayed linear map of an ordinary quiver path on a raw right module over the bound path category.

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.modulePathMap_nil {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (N : CategoryTheory.Functor (Category R)ᵒᵖ (ModuleCat k)) (x : Q) : modulePathMap N Quiver.Path.nil = CategoryTheory.CategoryStruct.id (N.obj (Opposite.op (obj R x)))

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.modulePathMap_toPath {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (N : CategoryTheory.Functor (Category R)ᵒᵖ (ModuleCat k)) {x y : Q} (a : x ⟶ y) : modulePathMap N a.toPath = moduleArrowMap N a

theorem MagnitudeConjecture.BoundQuiver.StringWord.modulePathMap_comp {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (N : CategoryTheory.Functor (Category R)ᵒᵖ (ModuleCat k)) {x y z : Q} (p : Quiver.Path x y) (q : Quiver.Path y z) : modulePathMap N (p.comp q) = CategoryTheory.CategoryStruct.comp (modulePathMap N p) (modulePathMap N q)

Path action respects path concatenation in the displayed direction.

theorem MagnitudeConjecture.BoundQuiver.StringWord.modulePathMap_cons {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (N : CategoryTheory.Functor (Category R)ᵒᵖ (ModuleCat k)) {x y z : Q} (p : Quiver.Path x y) (a : y ⟶ z) : modulePathMap N (p.cons a) = CategoryTheory.CategoryStruct.comp (modulePathMap N p) (moduleArrowMap N a)

Appending one arrow to a path appends its displayed module action.

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.signedArrowSubspace {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (N : CategoryTheory.Functor (Category R)ᵒᵖ (ModuleCat k)) {x y : Q} (e : SignedArrow x y) (U : Submodule k ↑(N.obj (Opposite.op (obj R x)))) : Submodule k ↑(N.obj (Opposite.op (obj R y)))

Transport a subspace across one signed arrow. A positive arrow acts by direct image; a negative arrow acts by preimage under the corresponding ordinary-arrow map.

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.signedArrowSubspace_positive {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (N : CategoryTheory.Functor (Category R)ᵒᵖ (ModuleCat k)) {x y : Q} (a : x ⟶ y) (U : Submodule k ↑(N.obj (Opposite.op (obj R x)))) : signedArrowSubspace N (positiveArrow a) U = Submodule.map (ModuleCat.Hom.hom (moduleArrowMap N a)) U

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.signedArrowSubspace_negative {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (N : CategoryTheory.Functor (Category R)ᵒᵖ (ModuleCat k)) {x y : Q} (a : x ⟶ y) (U : Submodule k ↑(N.obj (Opposite.op (obj R y)))) : signedArrowSubspace N (negativeArrow a) U = Submodule.comap (ModuleCat.Hom.hom (moduleArrowMap N a)) U

@[irreducible]

def MagnitudeConjecture.BoundQuiver.StringWord.signedPathSubspace {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (N : CategoryTheory.Functor (Category R)ᵒᵖ (ModuleCat k)) {x y : Q} : SignedPath x y → Submodule k ↑(N.obj (Opposite.op (obj R x))) → Submodule k ↑(N.obj (Opposite.op (obj R y)))

Transport a subspace along a signed path, applying its signed arrows from left to right.

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.signedPathSubspace_nil {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (N : CategoryTheory.Functor (Category R)ᵒᵖ (ModuleCat k)) {x : Q} (U : Submodule k ↑(N.obj (Opposite.op (obj R x)))) : signedPathSubspace N Quiver.Path.nil U = U

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.signedPathSubspace_cons {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (N : CategoryTheory.Functor (Category R)ᵒᵖ (ModuleCat k)) {x y z : Q} (p : SignedPath x y) (e : SignedArrow y z) (U : Submodule k ↑(N.obj (Opposite.op (obj R x)))) : signedPathSubspace N (Quiver.Path.cons p e) U = signedArrowSubspace N e (signedPathSubspace N p U)

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.signedPathSubspace_toPath {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (N : CategoryTheory.Functor (Category R)ᵒᵖ (ModuleCat k)) {x y : Q} (e : SignedArrow x y) (U : Submodule k ↑(N.obj (Opposite.op (obj R x)))) : signedPathSubspace N (Quiver.Hom.toPath e) U = signedArrowSubspace N e U

Transport along a one-arrow path is transport across that signed arrow.

theorem MagnitudeConjecture.BoundQuiver.StringWord.signedArrowSubspace_mono {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (N : CategoryTheory.Functor (Category R)ᵒᵖ (ModuleCat k)) {x y : Q} (e : SignedArrow x y) {U V : Submodule k ↑(N.obj (Opposite.op (obj R x)))} (hUV : U ≤ V) : signedArrowSubspace N e U ≤ signedArrowSubspace N e V

Signed-arrow transport is monotone in the input subspace.

theorem MagnitudeConjecture.BoundQuiver.StringWord.signedArrowSubspace_map_le {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {M N : CategoryTheory.Functor (Category R)ᵒᵖ (ModuleCat k)} (f : M ⟶ N) {x y : Q} (e : SignedArrow x y) (U : Submodule k ↑(M.obj (Opposite.op (obj R x)))) : Submodule.map (ModuleCat.Hom.hom (f.app (Opposite.op (obj R y)))) (signedArrowSubspace M e U) ≤ signedArrowSubspace N e (Submodule.map (ModuleCat.Hom.hom (f.app (Opposite.op (obj R x)))) U)

A module morphism carries signed-arrow transport into the corresponding transport of the image subspace. The statement is an inclusion because preimages along a negative arrow need not commute with a noninvertible module morphism.

theorem MagnitudeConjecture.BoundQuiver.StringWord.signedPathSubspace_mono {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (N : CategoryTheory.Functor (Category R)ᵒᵖ (ModuleCat k)) {x y : Q} (p : SignedPath x y) {U V : Submodule k ↑(N.obj (Opposite.op (obj R x)))} : U ≤ V → signedPathSubspace N p U ≤ signedPathSubspace N p V

Signed-path transport is monotone in the input subspace.

theorem MagnitudeConjecture.BoundQuiver.StringWord.signedPathSubspace_map_le {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} {M N : CategoryTheory.Functor (Category R)ᵒᵖ (ModuleCat k)} (f : M ⟶ N) {x y : Q} (p : SignedPath x y) (U : Submodule k ↑(M.obj (Opposite.op (obj R x)))) : Submodule.map (ModuleCat.Hom.hom (f.app (Opposite.op (obj R y)))) (signedPathSubspace M p U) ≤ signedPathSubspace N p (Submodule.map (ModuleCat.Hom.hom (f.app (Opposite.op (obj R x)))) U)

A module morphism carries signed-path transport into the transport of the image subspace.

theorem MagnitudeConjecture.BoundQuiver.StringWord.signedPathSubspace_comp {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (N : CategoryTheory.Functor (Category R)ᵒᵖ (ModuleCat k)) {x y z : Q} (p : SignedPath x y) (q : SignedPath y z) (U : Submodule k ↑(N.obj (Opposite.op (obj R x)))) : signedPathSubspace N (Quiver.Path.comp p q) U = signedPathSubspace N q (signedPathSubspace N p U)

Transport along a composite signed path is iterated transport.