Contextual detectors at every position of a string

The boundary conditions of a string detector belong to the two outer ends of the complete string. At an internal split, they are transported along the prefix and the reversed suffix. Keeping those outer boundary conditions fixed makes passage across one displayed letter a pure image/preimage calculation, even when the monomial relations have length greater than two.

structure MagnitudeConjecture.BoundQuiver.StringWord.Word.Split {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} (E : Word P.relations) : Type u

A displayed cut of a word into a prefix and suffix.

• vertex : Q
• prefixPath : SignedPath E.source self.vertex
• suffixPath : SignedPath self.vertex E.target
• factor : E.path = Quiver.Path.comp self.prefixPath self.suffixPath

def MagnitudeConjecture.BoundQuiver.StringWord.Word.Split.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} (E : Word P.relations) : E.Split

The cut at the target endpoint.

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.Word.Split.ofPosition {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} (E : Word P.relations) (i : E.Position) : E.Split

The cut represented by a word position.

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.Split.target_vertex {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} (E : Word P.relations) : (target E).vertex = E.target

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.Split.target_prefix {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} (E : Word P.relations) : (target E).prefixPath = E.path

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.Word.Split.target_suffix {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} (E : Word P.relations) : (target E).suffixPath = Quiver.Path.nil

structure MagnitudeConjecture.BoundQuiver.StringWord.Word.Split.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} {E : Word P.relations} (c d : E.Split) : Type u

Two consecutive cuts separated by a positively traversed quiver arrow.

• arrow : c.vertex ⟶ d.vertex
• prefix_eq : d.prefixPath = Quiver.Path.comp c.prefixPath (Quiver.Hom.toPath (positiveArrow self.arrow))
• suffix_eq : c.suffixPath = (Quiver.Hom.toPath (positiveArrow self.arrow)).comp d.suffixPath

structure MagnitudeConjecture.BoundQuiver.StringWord.Word.Split.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} {E : Word P.relations} (c d : E.Split) : Type u

Two consecutive cuts separated by a formally inverse quiver arrow.

• arrow : d.vertex ⟶ c.vertex
• prefix_eq : d.prefixPath = Quiver.Path.comp c.prefixPath (Quiver.Hom.toPath (negativeArrow self.arrow))
• suffix_eq : c.suffixPath = (Quiver.Hom.toPath (negativeArrow self.arrow)).comp d.suffixPath

@[reducible, inline]

abbrev MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.detectorEndpoint {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) (E : Word P.relations) : EndpointWord S E.target (signedPathTargetSignOr S false E.path)

The endpoint detector word belonging to a literal word.

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.splitRightLower {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} (N : CategoryTheory.Functor (Category P.relations)ᵒᵖ (ModuleCat k)) (S : P.ArrowPolarization) (E : Word P.relations) (c : E.Split) : Submodule k ↑(N.obj (Opposite.op (obj P.relations c.vertex)))

Lower filtration subspace arriving from the source end of E.

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.splitRightUpper {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} (N : CategoryTheory.Functor (Category P.relations)ᵒᵖ (ModuleCat k)) (S : P.ArrowPolarization) (E : Word P.relations) (c : E.Split) : Submodule k ↑(N.obj (Opposite.op (obj P.relations c.vertex)))

Upper filtration subspace arriving from the source end of E.

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.splitLeftLower {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} (N : CategoryTheory.Functor (Category P.relations)ᵒᵖ (ModuleCat k)) (S : P.ArrowPolarization) (E : Word P.relations) (c : E.Split) : Submodule k ↑(N.obj (Opposite.op (obj P.relations c.vertex)))

Lower filtration subspace arriving backwards from the target end of E.

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.splitLeftUpper {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} (N : CategoryTheory.Functor (Category P.relations)ᵒᵖ (ModuleCat k)) (S : P.ArrowPolarization) (E : Word P.relations) (c : E.Split) : Submodule k ↑(N.obj (Opposite.op (obj P.relations c.vertex)))

Upper filtration subspace arriving backwards from the target end of E.

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.splitDetectorNumerator {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} (N : CategoryTheory.Functor (Category P.relations)ᵒᵖ (ModuleCat k)) (S : P.ArrowPolarization) (E : Word P.relations) (c : E.Split) : Submodule k ↑(N.obj (Opposite.op (obj P.relations c.vertex)))

Numerator of the contextual detector at c.

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.splitDetectorDenominator {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} (N : CategoryTheory.Functor (Category P.relations)ᵒᵖ (ModuleCat k)) (S : P.ArrowPolarization) (E : Word P.relations) (c : E.Split) : Submodule k ↑(N.obj (Opposite.op (obj P.relations c.vertex)))

Denominator of the contextual detector at c.

theorem MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.splitRightLower_le_splitRightUpper {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} (N : CategoryTheory.Functor (Category P.relations)ᵒᵖ (ModuleCat k)) [N.Additive] (S : P.ArrowPolarization) (E : Word P.relations) (c : E.Split) : splitRightLower N S E c ≤ splitRightUpper N S E c

theorem MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.splitLeftLower_le_splitLeftUpper {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} (N : CategoryTheory.Functor (Category P.relations)ᵒᵖ (ModuleCat k)) [N.Additive] (S : P.ArrowPolarization) (E : Word P.relations) (c : E.Split) : splitLeftLower N S E c ≤ splitLeftUpper N S E c

theorem MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.splitRightLower_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} (N : CategoryTheory.Functor (Category P.relations)ᵒᵖ (ModuleCat k)) (S : P.ArrowPolarization) (E : Word P.relations) {c d : E.Split} (step : c.PositiveStep d) : splitRightLower N S E d = Submodule.map (ModuleCat.Hom.hom (moduleArrowMap N step.arrow)) (splitRightLower N S E c)

theorem MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.splitRightUpper_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} (N : CategoryTheory.Functor (Category P.relations)ᵒᵖ (ModuleCat k)) (S : P.ArrowPolarization) (E : Word P.relations) {c d : E.Split} (step : c.PositiveStep d) : splitRightUpper N S E d = Submodule.map (ModuleCat.Hom.hom (moduleArrowMap N step.arrow)) (splitRightUpper N S E c)

theorem MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.splitLeftLower_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} (N : CategoryTheory.Functor (Category P.relations)ᵒᵖ (ModuleCat k)) (S : P.ArrowPolarization) (E : Word P.relations) {c d : E.Split} (step : c.PositiveStep d) : splitLeftLower N S E c = Submodule.comap (ModuleCat.Hom.hom (moduleArrowMap N step.arrow)) (splitLeftLower N S E d)

theorem MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.splitLeftUpper_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} (N : CategoryTheory.Functor (Category P.relations)ᵒᵖ (ModuleCat k)) (S : P.ArrowPolarization) (E : Word P.relations) {c d : E.Split} (step : c.PositiveStep d) : splitLeftUpper N S E c = Submodule.comap (ModuleCat.Hom.hom (moduleArrowMap N step.arrow)) (splitLeftUpper N S E d)

theorem MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.splitRightLower_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} (N : CategoryTheory.Functor (Category P.relations)ᵒᵖ (ModuleCat k)) (S : P.ArrowPolarization) (E : Word P.relations) {c d : E.Split} (step : c.NegativeStep d) : splitRightLower N S E d = Submodule.comap (ModuleCat.Hom.hom (moduleArrowMap N step.arrow)) (splitRightLower N S E c)

theorem MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.splitRightUpper_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} (N : CategoryTheory.Functor (Category P.relations)ᵒᵖ (ModuleCat k)) (S : P.ArrowPolarization) (E : Word P.relations) {c d : E.Split} (step : c.NegativeStep d) : splitRightUpper N S E d = Submodule.comap (ModuleCat.Hom.hom (moduleArrowMap N step.arrow)) (splitRightUpper N S E c)

theorem MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.splitLeftLower_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} (N : CategoryTheory.Functor (Category P.relations)ᵒᵖ (ModuleCat k)) (S : P.ArrowPolarization) (E : Word P.relations) {c d : E.Split} (step : c.NegativeStep d) : splitLeftLower N S E c = Submodule.map (ModuleCat.Hom.hom (moduleArrowMap N step.arrow)) (splitLeftLower N S E d)

theorem MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.splitLeftUpper_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} (N : CategoryTheory.Functor (Category P.relations)ᵒᵖ (ModuleCat k)) (S : P.ArrowPolarization) (E : Word P.relations) {c d : E.Split} (step : c.NegativeStep d) : splitLeftUpper N S E c = Submodule.map (ModuleCat.Hom.hom (moduleArrowMap N step.arrow)) (splitLeftUpper N S E d)

theorem MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.splitDetectorDenominator_le_splitDetectorNumerator {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} (N : CategoryTheory.Functor (Category P.relations)ᵒᵖ (ModuleCat k)) [N.Additive] (S : P.ArrowPolarization) (E : Word P.relations) (c : E.Split) : splitDetectorDenominator N S E c ≤ splitDetectorNumerator N S E c

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.splitDetectorDenominatorInNumerator {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} (N : CategoryTheory.Functor (Category P.relations)ᵒᵖ (ModuleCat k)) (S : P.ArrowPolarization) (E : Word P.relations) (c : E.Split) : Submodule k ↥(splitDetectorNumerator N S E c)

Contextual denominator inside its numerator.

@[reducible, inline]

abbrev MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.SplitDetectorSpace {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} (N : CategoryTheory.Functor (Category P.relations)ᵒᵖ (ModuleCat k)) (S : P.ArrowPolarization) (E : Word P.relations) (c : E.Split) : Type u

Contextual detector space at a displayed split.

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.splitDetectorSpacePositiveStepEquiv {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} (N : CategoryTheory.Functor (Category P.relations)ᵒᵖ (ModuleCat k)) [N.Additive] (S : P.ArrowPolarization) (E : Word P.relations) {c d : E.Split} (step : c.PositiveStep d) : SplitDetectorSpace N S E c ≃ₗ[k] SplitDetectorSpace N S E d

Contextual detector spaces at consecutive positive positions are canonically linearly equivalent.

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.splitDetectorSpaceNegativeStepEquiv {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} (N : CategoryTheory.Functor (Category P.relations)ᵒᵖ (ModuleCat k)) [N.Additive] (S : P.ArrowPolarization) (E : Word P.relations) {c d : E.Split} (step : c.NegativeStep d) : SplitDetectorSpace N S E c ≃ₗ[k] SplitDetectorSpace N S E d

Contextual detector spaces at consecutive negative positions are canonically linearly equivalent.

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.splitDetectorSpacePositiveStepEquiv_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} (N : CategoryTheory.Functor (Category P.relations)ᵒᵖ (ModuleCat k)) [N.Additive] (S : P.ArrowPolarization) (E : Word P.relations) {c d : E.Split} (step : c.PositiveStep d) (x : ↥(splitDetectorNumerator N S E c)) : (splitDetectorSpacePositiveStepEquiv N S E step) (Submodule.Quotient.mk x) = Submodule.Quotient.mk ⟨(CategoryTheory.ConcreteCategory.hom (moduleArrowMap N step.arrow)) ↑x, ⋯⟩

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.splitDetectorSpaceNegativeStepEquiv_symm_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} (N : CategoryTheory.Functor (Category P.relations)ᵒᵖ (ModuleCat k)) [N.Additive] (S : P.ArrowPolarization) (E : Word P.relations) {c d : E.Split} (step : c.NegativeStep d) (x : ↥(splitDetectorNumerator N S E d)) : (splitDetectorSpaceNegativeStepEquiv N S E step).symm (Submodule.Quotient.mk x) = Submodule.Quotient.mk ⟨(CategoryTheory.ConcreteCategory.hom (moduleArrowMap N step.arrow)) ↑x, ⋯⟩

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.splitRightLower_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} (N : CategoryTheory.Functor (Category P.relations)ᵒᵖ (ModuleCat k)) [N.Additive] (S : P.ArrowPolarization) (E : Word P.relations) : splitRightLower N S E (Word.Split.target E) = lowerSubspace N (detectorEndpoint S E)

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.splitRightUpper_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} (N : CategoryTheory.Functor (Category P.relations)ᵒᵖ (ModuleCat k)) [N.Additive] (S : P.ArrowPolarization) (E : Word P.relations) : splitRightUpper N S E (Word.Split.target E) = upperSubspace N (detectorEndpoint S E)

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.splitLeftLower_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} (N : CategoryTheory.Functor (Category P.relations)ᵒᵖ (ModuleCat k)) (S : P.ArrowPolarization) (E : Word P.relations) : splitLeftLower N S E (Word.Split.target E) = lowerSubspace N (detectorEndpoint S E).oppositeVertex

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.splitLeftUpper_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} (N : CategoryTheory.Functor (Category P.relations)ᵒᵖ (ModuleCat k)) (S : P.ArrowPolarization) (E : Word P.relations) : splitLeftUpper N S E (Word.Split.target E) = upperSubspace N (detectorEndpoint S E).oppositeVertex

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.splitDetectorNumerator_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} (N : CategoryTheory.Functor (Category P.relations)ᵒᵖ (ModuleCat k)) [N.Additive] (S : P.ArrowPolarization) (E : Word P.relations) : splitDetectorNumerator N S E (Word.Split.target E) = detectorNumerator N (detectorEndpoint S E)

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.splitDetectorDenominator_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} (N : CategoryTheory.Functor (Category P.relations)ᵒᵖ (ModuleCat k)) [N.Additive] (S : P.ArrowPolarization) (E : Word P.relations) : splitDetectorDenominator N S E (Word.Split.target E) = detectorDenominator N (detectorEndpoint S E)

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.splitDetectorSpaceTargetEquiv {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} (N : CategoryTheory.Functor (Category P.relations)ᵒᵖ (ModuleCat k)) [N.Additive] (S : P.ArrowPolarization) (E : Word P.relations) : SplitDetectorSpace N S E (Word.Split.target E) ≃ₗ[k] DetectorSpace N (detectorEndpoint S E)

At the target cut, the contextual detector is the campaign's canonical endpoint detector.

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.splitDetectorSpaceTargetEquiv_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} (N : CategoryTheory.Functor (Category P.relations)ᵒᵖ (ModuleCat k)) [N.Additive] (S : P.ArrowPolarization) (E : Word P.relations) (x : ↥(splitDetectorNumerator N S E (Word.Split.target E))) : (splitDetectorSpaceTargetEquiv N S E) (Submodule.Quotient.mk x) = Submodule.Quotient.mk ⟨↑x, ⋯⟩