The finite-string detecting functors #
For C in Butler--Ringel's W(u,t), this file constructs the detecting
quotient
(1^+ ∩ C^+) / ((1^+ ∩ C^-) + (1^- ∩ C^+))
as a functor from linear modules over the bound path category to
ModuleCat k. Here 1 is the oppositely polarized trivial word
1_(u,not t). The subspace naturality proved in the preceding files gives
the induced quotient maps and the functor laws.
def
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.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}
(_C : EndpointWord S u₀ t)
:
EndpointWord S u₀ !t
The oppositely polarized trivial word 1_(u,not t) used in the detector
indexed by C ∈ W(u,t).
Instances For
@[simp]
theorem
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.oppositeVertex_path
{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)
:
C.oppositeVertex.path = Quiver.Path.nil
@[simp]
theorem
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.upperSubspace_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}
(N : CategoryTheory.Functor (Category P.relations)ᵒᵖ (ModuleCat k))
(C : EndpointWord S u₀ t)
:
@[simp]
theorem
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.lowerSubspace_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}
(N : CategoryTheory.Functor (Category P.relations)ᵒᵖ (ModuleCat k))
(C : EndpointWord S u₀ t)
:
noncomputable def
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.detectorNumerator
{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)
:
The numerator 1^+ ∩ C^+ of the detecting quotient.
Instances For
noncomputable def
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.detectorDenominator
{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)
:
The denominator (1^+ ∩ C^-) + (1^- ∩ C^+) of the detecting quotient.
Instances For
theorem
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.detectorDenominator_le_detectorNumerator
{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)
:
detectorDenominator N C ≤ detectorNumerator N C
The detector denominator lies in its numerator.
noncomputable def
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.detectorDenominatorInNumerator
{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 ↥(detectorNumerator N C)
The denominator regarded as a submodule of the numerator.
Instances For
@[reducible, inline]
abbrev
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.DetectorSpace
{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)
:
Type u
The underlying vector space of the Butler--Ringel detector.
Instances For
theorem
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.detectorNumerator_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₀)))) (detectorNumerator M C) ≤ detectorNumerator N C
The detector numerator is preserved by a module morphism.
theorem
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.detectorDenominator_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₀)))) (detectorDenominator M C) ≤ detectorDenominator N C
The detector denominator is preserved by a module morphism.
noncomputable def
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.detectorNumeratorMap
{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)
:
↥(detectorNumerator M C) →ₗ[k] ↥(detectorNumerator N C)
Restriction of a module morphism to the detector numerators.
Instances For
@[simp]
theorem
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.detectorNumeratorMap_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)
(C : EndpointWord S u₀ t)
(x : ↥(detectorNumerator M C))
:
↑((detectorNumeratorMap f C) x) = (CategoryTheory.ConcreteCategory.hom (f.app (Opposite.op (obj P.relations u₀)))) ↑x
theorem
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.detectorDenominatorInNumerator_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)
(C : EndpointWord S u₀ t)
:
detectorDenominatorInNumerator M C ≤ Submodule.comap (detectorNumeratorMap f C) (detectorDenominatorInNumerator N C)
The restricted numerator map preserves the denominator submodules.
noncomputable def
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.detectorLinearMap
{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)
:
DetectorSpace M C →ₗ[k] DetectorSpace N C
The linear map induced on detector quotients.
Instances For
@[simp]
theorem
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.detectorLinearMap_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)
(C : EndpointWord S u₀ t)
(x : ↥(detectorNumerator M C))
:
(detectorLinearMap f C) (Submodule.Quotient.mk x) = Submodule.Quotient.mk ((detectorNumeratorMap f C) x)
noncomputable def
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.detectorFunctor
{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)
:
CategoryTheory.Functor (CoveringHom.LinearModuleCategory k) (ModuleCat k)
The Butler--Ringel detector associated to an endpoint word.
Instances For
instance
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.detectorFunctor_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}
(C : EndpointWord S u₀ t)
:
C.detectorFunctor.Additive
instance
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.detectorFunctor_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}
(C : EndpointWord S u₀ t)
:
CategoryTheory.Functor.Linear k C.detectorFunctor