Naturality of contextual split detectors

A module morphism preserves the four contextual filtration subspaces at a fixed cut of a complete string. It therefore induces a map on the contextual detector quotient. This is the vertical map used in the change-of-split naturality square.

theorem MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.splitRightLower_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} {M N : CategoryTheory.Functor (Category P.relations)ᵒᵖ (ModuleCat k)} (f : M ⟶ N) (S : P.ArrowPolarization) (E : Word P.relations) (c : E.Split) : Submodule.map (ModuleCat.Hom.hom (f.app (Opposite.op (obj P.relations c.vertex)))) (splitRightLower M S E c) ≤ splitRightLower N S E c

theorem MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.splitRightUpper_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} {M N : CategoryTheory.Functor (Category P.relations)ᵒᵖ (ModuleCat k)} (f : M ⟶ N) (S : P.ArrowPolarization) (E : Word P.relations) (c : E.Split) : Submodule.map (ModuleCat.Hom.hom (f.app (Opposite.op (obj P.relations c.vertex)))) (splitRightUpper M S E c) ≤ splitRightUpper N S E c

theorem MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.splitLeftLower_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} {M N : CategoryTheory.Functor (Category P.relations)ᵒᵖ (ModuleCat k)} (f : M ⟶ N) (S : P.ArrowPolarization) (E : Word P.relations) (c : E.Split) : Submodule.map (ModuleCat.Hom.hom (f.app (Opposite.op (obj P.relations c.vertex)))) (splitLeftLower M S E c) ≤ splitLeftLower N S E c

theorem MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.splitLeftUpper_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} {M N : CategoryTheory.Functor (Category P.relations)ᵒᵖ (ModuleCat k)} (f : M ⟶ N) (S : P.ArrowPolarization) (E : Word P.relations) (c : E.Split) : Submodule.map (ModuleCat.Hom.hom (f.app (Opposite.op (obj P.relations c.vertex)))) (splitLeftUpper M S E c) ≤ splitLeftUpper N S E c

theorem MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.splitDetectorNumerator_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} {M N : CategoryTheory.Functor (Category P.relations)ᵒᵖ (ModuleCat k)} (f : M ⟶ N) (S : P.ArrowPolarization) (E : Word P.relations) (c : E.Split) : Submodule.map (ModuleCat.Hom.hom (f.app (Opposite.op (obj P.relations c.vertex)))) (splitDetectorNumerator M S E c) ≤ splitDetectorNumerator N S E c

theorem MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.splitDetectorDenominator_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} {M N : CategoryTheory.Functor (Category P.relations)ᵒᵖ (ModuleCat k)} (f : M ⟶ N) (S : P.ArrowPolarization) (E : Word P.relations) (c : E.Split) : Submodule.map (ModuleCat.Hom.hom (f.app (Opposite.op (obj P.relations c.vertex)))) (splitDetectorDenominator M S E c) ≤ splitDetectorDenominator N S E c

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.splitDetectorNumeratorMap {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} {M N : CategoryTheory.Functor (Category P.relations)ᵒᵖ (ModuleCat k)} (f : M ⟶ N) (S : P.ArrowPolarization) (E : Word P.relations) (c : E.Split) : ↥(splitDetectorNumerator M S E c) →ₗ[k] ↥(splitDetectorNumerator N S E c)

Restriction of a module morphism to contextual split numerators.

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.splitDetectorNumeratorMap_coe {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} {M N : CategoryTheory.Functor (Category P.relations)ᵒᵖ (ModuleCat k)} (f : M ⟶ N) (S : P.ArrowPolarization) (E : Word P.relations) (c : E.Split) (x : ↥(splitDetectorNumerator M S E c)) : ↑((splitDetectorNumeratorMap f S E c) x) = (CategoryTheory.ConcreteCategory.hom (f.app (Opposite.op (obj P.relations c.vertex)))) ↑x

theorem MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.splitDetectorDenominatorInNumerator_le_comap {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} {M N : CategoryTheory.Functor (Category P.relations)ᵒᵖ (ModuleCat k)} (f : M ⟶ N) (S : P.ArrowPolarization) (E : Word P.relations) (c : E.Split) : splitDetectorDenominatorInNumerator M S E c ≤ Submodule.comap (splitDetectorNumeratorMap f S E c) (splitDetectorDenominatorInNumerator N S E c)

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.splitDetectorLinearMap {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} {M N : CategoryTheory.Functor (Category P.relations)ᵒᵖ (ModuleCat k)} (f : M ⟶ N) (S : P.ArrowPolarization) (E : Word P.relations) (c : E.Split) : SplitDetectorSpace M S E c →ₗ[k] SplitDetectorSpace N S E c

Linear map induced on a contextual split detector.

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.splitDetectorLinearMap_mk {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} {M N : CategoryTheory.Functor (Category P.relations)ᵒᵖ (ModuleCat k)} (f : M ⟶ N) (S : P.ArrowPolarization) (E : Word P.relations) (c : E.Split) (x : ↥(splitDetectorNumerator M S E c)) : (splitDetectorLinearMap f S E c) (Submodule.Quotient.mk x) = Submodule.Quotient.mk ((splitDetectorNumeratorMap f S E c) x)

theorem MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.splitDetectorLinearMap_target {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} {M N : CategoryTheory.Functor (Category P.relations)ᵒᵖ (ModuleCat k)} [M.Additive] [N.Additive] (f : M ⟶ N) (S : P.ArrowPolarization) (E : Word P.relations) (q : SplitDetectorSpace M S E (Word.Split.target E)) : (splitDetectorSpaceTargetEquiv N S E) ((splitDetectorLinearMap f S E (Word.Split.target E)) q) = (detectorLinearMap f (detectorEndpoint S E)) ((splitDetectorSpaceTargetEquiv M S E) q)

At the target cut, the contextual detector map is the canonical endpoint detector map, under the target-cut identifications.

theorem MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.splitDetectorLinearMap_positiveStep {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} {M N : CategoryTheory.Functor (Category P.relations)ᵒᵖ (ModuleCat k)} [M.Additive] [N.Additive] (f : M ⟶ N) (S : P.ArrowPolarization) (E : Word P.relations) {c d : E.Split} (step : c.PositiveStep d) (q : SplitDetectorSpace M S E c) : (splitDetectorSpacePositiveStepEquiv N S E step) ((splitDetectorLinearMap f S E c) q) = (splitDetectorLinearMap f S E d) ((splitDetectorSpacePositiveStepEquiv M S E step) q)

Change of split across a positive letter commutes with module morphisms.

theorem MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.splitDetectorLinearMap_negativeStep_symm {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} {M N : CategoryTheory.Functor (Category P.relations)ᵒᵖ (ModuleCat k)} [M.Additive] [N.Additive] (f : M ⟶ N) (S : P.ArrowPolarization) (E : Word P.relations) {c d : E.Split} (step : c.NegativeStep d) (q : SplitDetectorSpace M S E d) : (splitDetectorSpaceNegativeStepEquiv N S E step).symm ((splitDetectorLinearMap f S E d) q) = (splitDetectorLinearMap f S E c) ((splitDetectorSpaceNegativeStepEquiv M S E step).symm q)

The natural arrow-direction map across a negative letter, namely the inverse of change of split, commutes with module morphisms.

theorem MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.splitDetectorLinearMap_negativeStep {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} {M N : CategoryTheory.Functor (Category P.relations)ᵒᵖ (ModuleCat k)} [M.Additive] [N.Additive] (f : M ⟶ N) (S : P.ArrowPolarization) (E : Word P.relations) {c d : E.Split} (step : c.NegativeStep d) (q : SplitDetectorSpace M S E c) : (splitDetectorSpaceNegativeStepEquiv N S E step) ((splitDetectorLinearMap f S E c) q) = (splitDetectorLinearMap f S E d) ((splitDetectorSpaceNegativeStepEquiv M S E step) q)

Change of split across a negative letter commutes with module morphisms.