Grid refinement of the two endpoint-word filtrations #
For opposite endpoint polarizations, Ringel refines the left word interval by the right word filtration. This file first identifies one resulting grid quotient with the already defined pair detector, by a canonical natural linear equivalence.
noncomputable def
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.pairGridLower
{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)
:
Lower endpoint of the grid interval obtained by refining L with R.
Instances For
noncomputable def
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.pairGridUpper
{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)
:
Upper endpoint of the grid interval obtained by refining L with R.
Instances For
theorem
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.pairGridLower_le_pairGridUpper
{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)
:
pairGridLower N L R ≤ pairGridUpper N L R
noncomputable def
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.pairGridLowerInUpper
{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 ↥(pairGridUpper N L R)
The lower grid endpoint as a subspace of its upper endpoint.
Instances For
@[reducible, inline]
abbrev
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.PairGridSpace
{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
One successive quotient in Ringel's two-filtration grid.
Instances For
theorem
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.mem_pairDetectorDenominator_iff_mem_pairGridLower
{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)
(x : ↑(N.obj (Opposite.op (obj P.relations u₀))))
(hx : x ∈ pairDetectorNumerator N L R)
:
x ∈ pairDetectorDenominator N L R ↔ x ∈ pairGridLower N L R
On the pair numerator, membership in the pair denominator is equivalent to membership in the lower grid endpoint. This is the elementwise modular law underlying Ringel's quotient formula.
noncomputable def
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.pairNumeratorToGridUpperMap
{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)
:
↥(pairDetectorNumerator N L R) →ₗ[k] ↥(pairGridUpper N L R)
Inclusion of the pair numerator into the upper grid endpoint.
Instances For
@[simp]
theorem
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.pairNumeratorToGridUpperMap_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}
(N : CategoryTheory.Functor (Category P.relations)ᵒᵖ (ModuleCat k))
(L : EndpointWord S u₀ !t)
(R : EndpointWord S u₀ t)
(x : ↥(pairDetectorNumerator N L R))
:
↑((pairNumeratorToGridUpperMap N L R) x) = ↑x
theorem
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.pairDetectorDenominatorInNumerator_le_comap_pairGridLowerInUpper
{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)
:
pairDetectorDenominatorInNumerator N L R ≤ Submodule.comap (pairNumeratorToGridUpperMap N L R) (pairGridLowerInUpper N L R)
The pair denominator maps into the lower grid endpoint.
noncomputable def
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.pairDetectorToGridLinearMap
{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)
:
PairDetectorSpace N L R →ₗ[k] PairGridSpace N L R
Canonical map from the pair detector to its grid realization.
Instances For
@[simp]
theorem
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.pairDetectorToGridLinearMap_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}
(N : CategoryTheory.Functor (Category P.relations)ᵒᵖ (ModuleCat k))
[N.Additive]
(L : EndpointWord S u₀ !t)
(R : EndpointWord S u₀ t)
(x : ↥(pairDetectorNumerator N L R))
:
(pairDetectorToGridLinearMap N L R) (Submodule.Quotient.mk x) = Submodule.Quotient.mk ((pairNumeratorToGridUpperMap N L R) x)
theorem
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.pairDetectorToGridLinearMap_injective
{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)
:
Function.Injective ⇑(pairDetectorToGridLinearMap N L R)
theorem
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.pairDetectorToGridLinearMap_surjective
{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)
:
Function.Surjective ⇑(pairDetectorToGridLinearMap N L R)
noncomputable def
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.pairDetectorGridEquiv
{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)
:
PairDetectorSpace N L R ≃ₗ[k] PairGridSpace N L R
Canonical equivalence from a pair detector to its grid quotient.
Instances For
noncomputable def
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.pairGridDetectorEquiv
{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)
:
PairGridSpace N L R ≃ₗ[k] PairDetectorSpace N L R
Ringel's grid quotient, oriented toward the existing pair detector.
Instances For
@[simp]
theorem
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.pairDetectorGridEquiv_apply
{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)
(q : PairDetectorSpace N L R)
:
(pairDetectorGridEquiv N L R) q = (pairDetectorToGridLinearMap N L R) q
theorem
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.pairGridLower_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₀)))) (pairGridLower M L R) ≤ pairGridLower N L R
A module morphism preserves lower grid endpoints.
theorem
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.pairGridUpper_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₀)))) (pairGridUpper M L R) ≤ pairGridUpper N L R
A module morphism preserves upper grid endpoints.
noncomputable def
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.pairGridLinearMap
{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)}
[M.Additive]
[N.Additive]
(f : M ⟶ N)
(L : EndpointWord S u₀ !t)
(R : EndpointWord S u₀ t)
:
PairGridSpace M L R →ₗ[k] PairGridSpace N L R
Map induced by a module morphism on one grid quotient.
Instances For
@[simp]
theorem
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.pairGridLinearMap_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)}
[M.Additive]
[N.Additive]
(f : M ⟶ N)
(L : EndpointWord S u₀ !t)
(R : EndpointWord S u₀ t)
(x : ↥(pairGridUpper M L R))
:
(pairGridLinearMap f L R) (Submodule.Quotient.mk x) = Submodule.Quotient.mk
((LinearAlgebra.FiniteFiltration.restrictionMap (ModuleCat.Hom.hom (f.app (Opposite.op (obj P.relations u₀))))
(pairGridUpper M L R) (pairGridUpper N L R) ⋯)
x)
theorem
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.pairDetectorToGridLinearMap_naturality
{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)}
[M.Additive]
[N.Additive]
(f : M ⟶ N)
(L : EndpointWord S u₀ !t)
(R : EndpointWord S u₀ t)
(q : PairDetectorSpace M L R)
:
(pairGridLinearMap f L R) ((pairDetectorToGridLinearMap M L R) q) = (pairDetectorToGridLinearMap N L R) ((pairDetectorLinearMap f L R) q)
The canonical pair-to-grid map commutes with module morphisms.
theorem
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.pairGridDetectorEquiv_naturality
{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)}
[M.Additive]
[N.Additive]
(f : M ⟶ N)
(L : EndpointWord S u₀ !t)
(R : EndpointWord S u₀ t)
(q : PairGridSpace M L R)
:
(pairGridDetectorEquiv N L R) ((pairGridLinearMap f L R) q) = (pairDetectorLinearMap f L R) ((pairGridDetectorEquiv M L R) q)
The grid-to-pair equivalence is natural under module morphisms.
@[reducible, inline]
abbrev
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.GridWordIndex
{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)
:
Type u
Pairs of oppositely polarized endpoint words, in lexicographic order.
Instances For
noncomputable def
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.orderedGridWordOrderIso
{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}
[Finite (DetectorIndex S)]
:
Fin (Nat.card (GridWordIndex S u₀ t)) ≃o GridWordIndex S u₀ t
The finite grid-word family in canonical lexicographic enumeration.
Instances For
noncomputable def
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.orderedGridWord
{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}
[Finite (DetectorIndex S)]
(i : Fin (Nat.card (GridWordIndex S u₀ t)))
:
EndpointWord S u₀ !t × EndpointWord S u₀ t
The ith pair of endpoint words in lexicographic grid order.
Instances For
theorem
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.orderedGridWord_lt_iff
{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}
[Finite (DetectorIndex S)]
{i j : Fin (Nat.card (GridWordIndex S u₀ t))}
:
toLex (orderedGridWord i) < toLex (orderedGridWord j) ↔ i < j
theorem
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.orderedGridWord_surjective
{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}
[Finite (DetectorIndex S)]
:
Function.Surjective orderedGridWord
theorem
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.lowerSubspace_le_pairGridLower
{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)
:
lowerSubspace N L ≤ pairGridLower N L R
theorem
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.pairGridUpper_le_pairGridLower_of_lex_lt
{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]
{LR LR' : EndpointWord S u₀ !t × EndpointWord S u₀ t}
(h : toLex LR < toLex LR')
:
pairGridUpper N LR.1 LR.2 ≤ pairGridLower N LR'.1 LR'.2
Grid intervals avoid one another in lexicographic pair order.
theorem
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.orderedGridWord_upper_le_lower
{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}
[Finite (DetectorIndex S)]
(N : CategoryTheory.Functor (Category P.relations)ᵒᵖ (ModuleCat k))
[N.Additive]
{i j : Fin (Nat.card (GridWordIndex S u₀ t))}
(hij : i < j)
:
pairGridUpper N (orderedGridWord i).1 (orderedGridWord i).2 ≤ pairGridLower N (orderedGridWord j).1 (orderedGridWord j).2
theorem
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.exists_pairGrid_interval_of_ne_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}
[Finite (DetectorIndex S)]
(N : CategoryTheory.Functor (Category P.relations)ᵒᵖ (ModuleCat k))
[N.Additive]
(u₀ : Q)
(t : Bool)
(x : ↑(N.obj (Opposite.op (obj P.relations u₀))))
(hx : x ≠ 0)
:
∃ (L : EndpointWord S u₀ !t) (R : EndpointWord S u₀ t), x ∈ pairGridUpper N L R ∧ x ∉ pairGridLower N L R
Every nonzero vector belongs to one of the finite grid intervals.
noncomputable def
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.cumulativeGridSubspace
{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}
[Finite (DetectorIndex S)]
(N : CategoryTheory.Functor (Category P.relations)ᵒᵖ (ModuleCat k))
(j : Fin (Nat.card (GridWordIndex S u₀ t) + 1))
:
Cumulative upper endpoints before a cut in lexicographic grid order.
Instances For
theorem
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.cumulativeGridSubspace_le_lower
{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}
[Finite (DetectorIndex S)]
(N : CategoryTheory.Functor (Category P.relations)ᵒᵖ (ModuleCat k))
[N.Additive]
(j : Fin (Nat.card (GridWordIndex S u₀ t)))
:
cumulativeGridSubspace N j.castSucc ≤ pairGridLower N (orderedGridWord j).1 (orderedGridWord j).2
theorem
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.pairGridLower_le_cumulativeGridSubspace
{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}
[Finite (DetectorIndex S)]
(N : CategoryTheory.Functor (Category P.relations)ᵒᵖ (ModuleCat k))
[N.Additive]
(j : Fin (Nat.card (GridWordIndex S u₀ t)))
:
pairGridLower N (orderedGridWord j).1 (orderedGridWord j).2 ≤ cumulativeGridSubspace N j.castSucc
theorem
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.cumulativeGridSubspace_castSucc
{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}
[Finite (DetectorIndex S)]
(N : CategoryTheory.Functor (Category P.relations)ᵒᵖ (ModuleCat k))
[N.Additive]
(j : Fin (Nat.card (GridWordIndex S u₀ t)))
:
cumulativeGridSubspace N j.castSucc = pairGridLower N (orderedGridWord j).1 (orderedGridWord j).2
theorem
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.cumulativeGridSubspace_succ
{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}
[Finite (DetectorIndex S)]
(N : CategoryTheory.Functor (Category P.relations)ᵒᵖ (ModuleCat k))
[N.Additive]
(j : Fin (Nat.card (GridWordIndex S u₀ t)))
:
cumulativeGridSubspace N j.succ = pairGridUpper N (orderedGridWord j).1 (orderedGridWord j).2
theorem
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.cumulativeGridSubspace_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}
[Finite (DetectorIndex S)]
(N : CategoryTheory.Functor (Category P.relations)ᵒᵖ (ModuleCat k))
:
cumulativeGridSubspace N 0 = ⊥
theorem
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.cumulativeGridSubspace_last
{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}
[Finite (DetectorIndex S)]
(N : CategoryTheory.Functor (Category P.relations)ᵒᵖ (ModuleCat k))
[N.Additive]
:
cumulativeGridSubspace N (Fin.last (Nat.card (GridWordIndex S u₀ t))) = ⊤
noncomputable def
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.orderedGridFiltration
{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}
[Finite (DetectorIndex S)]
(N : CategoryTheory.Functor (Category P.relations)ᵒᵖ (ModuleCat k))
[N.Additive]
:
LinearAlgebra.FiniteFiltration.Filtration k (↑(N.obj (Opposite.op (obj P.relations u₀))))
(Nat.card (GridWordIndex S u₀ t))
The finite lexicographic grid filtration at one displayed vertex.
Instances For
theorem
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.orderedGridFiltration_compatible
{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}
[Finite (DetectorIndex S)]
{M N : CategoryTheory.Functor (Category P.relations)ᵒᵖ (ModuleCat k)}
[M.Additive]
[N.Additive]
(f : M ⟶ N)
:
LinearAlgebra.FiniteFiltration.Filtration.Compatible (ModuleCat.Hom.hom (f.app (Opposite.op (obj P.relations u₀))))
(orderedGridFiltration M) (orderedGridFiltration N)
Every module morphism preserves the finite grid filtrations.