Pair-position string detectors

Ringel's filtration uses a detector at every split position of a string. At a vertex u, such a split is represented by endpoint words with opposite polarizations. This file packages the corresponding subquotient

(L⁺ ∩ R⁺) / ((L⁺ ∩ R⁻) + (L⁻ ∩ R⁺))

and its functorial action. The detector already used in the campaign is the special case in which L is the oppositely polarized trivial word.

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.pairDetectorNumerator {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)) (L : EndpointWord S u₀ !t) (R : EndpointWord S u₀ t) : Submodule k ↑(N.obj (Opposite.op (obj P.relations u₀)))

Numerator of the detector at a split position.

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.pairDetectorDenominator {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)) (L : EndpointWord S u₀ !t) (R : EndpointWord S u₀ t) : Submodule k ↑(N.obj (Opposite.op (obj P.relations u₀)))

Denominator of the detector at a split position.

theorem MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.pairDetectorDenominator_le_pairDetectorNumerator {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] (L : EndpointWord S u₀ !t) (R : EndpointWord S u₀ t) : pairDetectorDenominator N L R ≤ pairDetectorNumerator N L R

The pair denominator lies in the pair numerator.

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.pairDetectorDenominatorInNumerator {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)) (L : EndpointWord S u₀ !t) (R : EndpointWord S u₀ t) : Submodule k ↥(pairDetectorNumerator N L R)

The pair denominator as a submodule of the pair numerator.

@[reducible, inline]

abbrev MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.PairDetectorSpace {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)) (L : EndpointWord S u₀ !t) (R : EndpointWord S u₀ t) : Type u

Underlying vector space of the detector at a split position.

theorem MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.pairDetectorNumerator_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) (L : EndpointWord S u₀ !t) (R : EndpointWord S u₀ t) : Submodule.map (ModuleCat.Hom.hom (f.app (Opposite.op (obj P.relations u₀)))) (pairDetectorNumerator M L R) ≤ pairDetectorNumerator N L R

A module morphism preserves pair numerators.

theorem MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.pairDetectorDenominator_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) (L : EndpointWord S u₀ !t) (R : EndpointWord S u₀ t) : Submodule.map (ModuleCat.Hom.hom (f.app (Opposite.op (obj P.relations u₀)))) (pairDetectorDenominator M L R) ≤ pairDetectorDenominator N L R

A module morphism preserves pair denominators.

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.pairDetectorNumeratorMap {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) (L : EndpointWord S u₀ !t) (R : EndpointWord S u₀ t) : ↥(pairDetectorNumerator M L R) →ₗ[k] ↥(pairDetectorNumerator N L R)

Restriction of a module morphism to pair numerators.

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.pairDetectorNumeratorMap_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} {S : P.ArrowPolarization} {u₀ : Q} {t : Bool} {M N : CategoryTheory.Functor (Category P.relations)ᵒᵖ (ModuleCat k)} (f : M ⟶ N) (L : EndpointWord S u₀ !t) (R : EndpointWord S u₀ t) (x : ↥(pairDetectorNumerator M L R)) : ↑((pairDetectorNumeratorMap f L R) x) = (CategoryTheory.ConcreteCategory.hom (f.app (Opposite.op (obj P.relations u₀)))) ↑x

theorem MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.pairDetectorDenominatorInNumerator_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} {S : P.ArrowPolarization} {u₀ : Q} {t : Bool} {M N : CategoryTheory.Functor (Category P.relations)ᵒᵖ (ModuleCat k)} (f : M ⟶ N) (L : EndpointWord S u₀ !t) (R : EndpointWord S u₀ t) : pairDetectorDenominatorInNumerator M L R ≤ Submodule.comap (pairDetectorNumeratorMap f L R) (pairDetectorDenominatorInNumerator N L R)

The restricted pair-numerator map preserves the pair denominator.

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.pairDetectorLinearMap {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) (L : EndpointWord S u₀ !t) (R : EndpointWord S u₀ t) : PairDetectorSpace M L R →ₗ[k] PairDetectorSpace N L R

Linear map induced on a pair detector.

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.pairDetectorLinearMap_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} {S : P.ArrowPolarization} {u₀ : Q} {t : Bool} {M N : CategoryTheory.Functor (Category P.relations)ᵒᵖ (ModuleCat k)} (f : M ⟶ N) (L : EndpointWord S u₀ !t) (R : EndpointWord S u₀ t) (x : ↥(pairDetectorNumerator M L R)) : (pairDetectorLinearMap f L R) (Submodule.Quotient.mk x) = Submodule.Quotient.mk ((pairDetectorNumeratorMap f L R) x)

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.pairDetectorFunctor {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} (L : EndpointWord S u₀ !t) (R : EndpointWord S u₀ t) : CategoryTheory.Functor (CoveringHom.LinearModuleCategory k) (ModuleCat k)

The detector functor attached to a split pair.

instance MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.pairDetectorFunctor_additive {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} (L : EndpointWord S u₀ !t) (R : EndpointWord S u₀ t) : (L.pairDetectorFunctor R).Additive

instance MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.pairDetectorFunctor_linear {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} (L : EndpointWord S u₀ !t) (R : EndpointWord S u₀ t) : CategoryTheory.Functor.Linear k (L.pairDetectorFunctor R)

noncomputable def MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.pairDetectorSpaceOppositeVertexEquiv {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) : PairDetectorSpace N C.oppositeVertex C ≃ₗ[k] DetectorSpace N C

The existing endpoint detector is literally the pair detector with a trivial left half.

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.pairDetectorLinearMap_oppositeVertex {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) : pairDetectorLinearMap f C.oppositeVertex C = detectorLinearMap f C