Boundary subspaces for string detectors

For a Butler--Ringel endpoint word C, the lower subspace C^- starts with the image of the unique compatible incoming arrow, or zero if there is none. The upper subspace C^+ starts with the kernel of the unique compatible outgoing arrow, or the whole source space if there is none. Both are then transported along C.

The polarization selects the correct one of the at most two arrows at a trivial endpoint. For a nontrivial word the same sign condition is forced by string composability. This file proves the fundamental inclusion C^-(M) <= C^+(M) and its naturality under module morphisms.

@[reducible, inline]

abbrev MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.IncomingExtension {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] {P : SpecialBiserialPresentation k A Q} {S : P.ArrowPolarization} {u : Q} {t : Bool} (C : EndpointWord S u t) : Type u

An incoming ordinary arrow which can be placed immediately before C with the Butler--Ringel endpoint-sign convention.

@[reducible, inline]

abbrev MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.OutgoingInverseExtension {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] {P : SpecialBiserialPresentation k A Q} {S : P.ArrowPolarization} {u : Q} {t : Bool} (C : EndpointWord S u t) : Type u

An outgoing ordinary arrow whose formal inverse can be placed immediately before C with the Butler--Ringel endpoint-sign convention.

theorem MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.incomingExtension_subsingleton {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] {P : SpecialBiserialPresentation k A Q} {S : P.ArrowPolarization} {u : Q} {t : Bool} (C : EndpointWord S u t) : Subsingleton C.IncomingExtension

The endpoint sign selects at most one compatible incoming arrow.

theorem MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.outgoingInverseExtension_subsingleton {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] {P : SpecialBiserialPresentation k A Q} {S : P.ArrowPolarization} {u : Q} {t : Bool} (C : EndpointWord S u t) : Subsingleton C.OutgoingInverseExtension

The endpoint sign selects at most one compatible outgoing inverse.

theorem MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.outgoing_comp_incoming_eq_zero {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] {P : SpecialBiserialPresentation k A Q} {S : P.ArrowPolarization} {u : Q} {t : Bool} (C : EndpointWord S u t) (inc : C.IncomingExtension) (out : C.OutgoingInverseExtension) : CategoryTheory.CategoryStruct.comp (arrowMap P.relations (↑out).snd) (arrowMap P.relations (↑inc).snd) = 0

If both boundary extensions exist, their ordinary two-arrow composition is killed by the relations.

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.lowerBoundarySubspace {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] {P : SpecialBiserialPresentation k A Q} {S : P.ArrowPolarization} {u : Q} {t : Bool} (N : CategoryTheory.Functor (Category P.relations)ᵒᵖ (ModuleCat k)) (C : EndpointWord S u t) : Submodule k ↑(N.obj (Opposite.op (obj P.relations C.source)))

The source-space input for C^-: the image of the compatible incoming arrow, or zero when no such arrow exists.

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.upperBoundarySubspace {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] {P : SpecialBiserialPresentation k A Q} {S : P.ArrowPolarization} {u : Q} {t : Bool} (N : CategoryTheory.Functor (Category P.relations)ᵒᵖ (ModuleCat k)) (C : EndpointWord S u t) : Submodule k ↑(N.obj (Opposite.op (obj P.relations C.source)))

The source-space input for C^+: the kernel of the compatible outgoing arrow, or the whole source space when no such arrow exists.

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.lowerSubspace {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] {P : SpecialBiserialPresentation k A Q} {S : P.ArrowPolarization} {u : Q} {t : Bool} (N : CategoryTheory.Functor (Category P.relations)ᵒᵖ (ModuleCat k)) (C : EndpointWord S u t) : Submodule k ↑(N.obj (Opposite.op (obj P.relations u)))

Butler--Ringel's lower word subspace C^-(N).

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.upperSubspace {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] {P : SpecialBiserialPresentation k A Q} {S : P.ArrowPolarization} {u : Q} {t : Bool} (N : CategoryTheory.Functor (Category P.relations)ᵒᵖ (ModuleCat k)) (C : EndpointWord S u t) : Submodule k ↑(N.obj (Opposite.op (obj P.relations u)))

Butler--Ringel's upper word subspace C^+(N).

theorem MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.lowerBoundarySubspace_le_upperBoundarySubspace {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] {P : SpecialBiserialPresentation k A Q} {S : P.ArrowPolarization} {u : Q} {t : Bool} (N : CategoryTheory.Functor (Category P.relations)ᵒᵖ (ModuleCat k)) [N.Additive] (C : EndpointWord S u t) : lowerBoundarySubspace N C ≤ upperBoundarySubspace N C

The boundary image lies in the boundary kernel.

theorem MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.lowerSubspace_le_upperSubspace {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] {P : SpecialBiserialPresentation k A Q} {S : P.ArrowPolarization} {u : Q} {t : Bool} (N : CategoryTheory.Functor (Category P.relations)ᵒᵖ (ModuleCat k)) [N.Additive] (C : EndpointWord S u t) : lowerSubspace N C ≤ upperSubspace N C

The fundamental Butler--Ringel inclusion C^-(N) <= C^+(N).

theorem MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.lowerBoundarySubspace_map_le {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] {P : SpecialBiserialPresentation k A Q} {S : P.ArrowPolarization} {u : Q} {t : Bool} {M N : CategoryTheory.Functor (Category P.relations)ᵒᵖ (ModuleCat k)} (f : M ⟶ N) (C : EndpointWord S u t) : Submodule.map (ModuleCat.Hom.hom (f.app (Opposite.op (obj P.relations C.source)))) (lowerBoundarySubspace M C) ≤ lowerBoundarySubspace N C

A module map carries the lower boundary subspace into the corresponding lower boundary subspace.

theorem MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.upperBoundarySubspace_map_le {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] {P : SpecialBiserialPresentation k A Q} {S : P.ArrowPolarization} {u : Q} {t : Bool} {M N : CategoryTheory.Functor (Category P.relations)ᵒᵖ (ModuleCat k)} (f : M ⟶ N) (C : EndpointWord S u t) : Submodule.map (ModuleCat.Hom.hom (f.app (Opposite.op (obj P.relations C.source)))) (upperBoundarySubspace M C) ≤ upperBoundarySubspace N C

A module map carries the upper boundary subspace into the corresponding upper boundary subspace.

theorem MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.lowerSubspace_map_le {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] {P : SpecialBiserialPresentation k A Q} {S : P.ArrowPolarization} {u : Q} {t : Bool} {M N : CategoryTheory.Functor (Category P.relations)ᵒᵖ (ModuleCat k)} (f : M ⟶ N) (C : EndpointWord S u t) : Submodule.map (ModuleCat.Hom.hom (f.app (Opposite.op (obj P.relations u)))) (lowerSubspace M C) ≤ lowerSubspace N C

The lower word subspace is natural under arbitrary module morphisms.

theorem MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.upperSubspace_map_le {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] {P : SpecialBiserialPresentation k A Q} {S : P.ArrowPolarization} {u : Q} {t : Bool} {M N : CategoryTheory.Functor (Category P.relations)ᵒᵖ (ModuleCat k)} (f : M ⟶ N) (C : EndpointWord S u t) : Submodule.map (ModuleCat.Hom.hom (f.app (Opposite.op (obj P.relations u)))) (upperSubspace M C) ≤ upperSubspace N C

The upper word subspace is natural under arbitrary module morphisms.