Coverage by finite endpoint-word intervals #
Besides its lower and upper boundary subspaces, an endpoint word transports the zero and whole source spaces. A vector lying in the transported whole space but outside the transported zero space can be followed down the finite source-extension tree: membership in the lower boundary forces the positive child, while failure of membership in the upper boundary forces the inverse child. Both moves preserve the invariant and strictly increase word length. The uniform finite-word bound therefore forces the process to stop inside an actual word interval.
noncomputable def
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.zeroSubspace
{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)
:
Transport of the zero source subspace along an endpoint word.
Instances For
noncomputable def
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.wholeSubspace
{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)
:
Transport of the whole source space along an endpoint word.
Instances For
theorem
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.zeroSubspace_le_lowerSubspace
{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)
:
zeroSubspace N C ≤ lowerSubspace N C
theorem
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.upperSubspace_le_wholeSubspace
{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)
:
upperSubspace N C ≤ wholeSubspace N C
theorem
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.lowerSubspace_eq_zeroSubspace_of_not_nonempty_incomingExtension
{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)
(hinc : ¬Nonempty C.IncomingExtension)
:
lowerSubspace N C = zeroSubspace N C
With no positive source extension, the lower endpoint is the transported zero space.
theorem
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.upperSubspace_eq_wholeSubspace_of_not_nonempty_outgoingInverseExtension
{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)
(hout : ¬Nonempty C.OutgoingInverseExtension)
:
upperSubspace N C = wholeSubspace N C
With no inverse source extension, the upper endpoint is the transported whole space.
theorem
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.zeroSubspace_prependIncoming
{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)
(inc : C.IncomingExtension)
:
zeroSubspace N (C.prependIncoming inc) = zeroSubspace N C
A positive child has the same transported zero space as its parent.
theorem
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.wholeSubspace_prependIncoming
{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)
(inc : C.IncomingExtension)
:
wholeSubspace N (C.prependIncoming inc) = lowerSubspace N C
The transported whole space of a positive child is exactly the lower endpoint of its parent.
theorem
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.zeroSubspace_prependOutgoingInverse
{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)
(out : C.OutgoingInverseExtension)
:
zeroSubspace N (C.prependOutgoingInverse out) = upperSubspace N C
The transported zero space of an inverse child is exactly the upper endpoint of its parent.
theorem
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.wholeSubspace_prependOutgoingInverse
{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)
(out : C.OutgoingInverseExtension)
:
wholeSubspace N (C.prependOutgoingInverse out) = wholeSubspace N C
An inverse child has the same transported whole space as its parent.
theorem
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.exists_descendant_mem_upperSubspace_not_mem_lowerSubspace
{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))
(C : EndpointWord S u t)
(x : ↑(N.obj (Opposite.op (obj P.relations u))))
(hxWhole : x ∈ wholeSubspace N C)
(hxZero : x ∉ zeroSubspace N C)
:
∃ (D : EndpointWord S u t) (pref : SignedPath D.source C.source),
D.path = Quiver.Path.comp pref C.path ∧ x ∈ upperSubspace N D ∧ x ∉ lowerSubspace N D
Starting from a word whose transported whole space contains x but
whose transported zero space does not, finite word length forces x into
one of its source-extension descendant intervals. The returned prefix is
the certificate that the terminal word really descends from the initial
one.
theorem
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.exists_mem_upperSubspace_not_mem_lowerSubspace
{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))
(C : EndpointWord S u t)
(x : ↑(N.obj (Opposite.op (obj P.relations u))))
(hxWhole : x ∈ wholeSubspace N C)
(hxZero : x ∉ zeroSubspace N C)
:
∃ (D : EndpointWord S u t), x ∈ upperSubspace N D ∧ x ∉ lowerSubspace N D
The descendant certificate may be forgotten when only interval coverage is needed.
theorem
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.exists_endpointWord_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))
(u : Q)
(t : Bool)
(x : ↑(N.obj (Opposite.op (obj P.relations u))))
(hx : x ≠ 0)
:
∃ (C : EndpointWord S u t), x ∈ upperSubspace N C ∧ x ∉ lowerSubspace N C
Every nonzero vector at a displayed vertex lies in the upper but not the lower subspace of some endpoint word of either fixed polarization.
noncomputable def
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.orderedWordOrderIso
{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 (EndpointWord S u t)) ≃o EndpointWord S u t
The finite endpoint-word family in its canonical in-order enumeration.
Instances For
noncomputable def
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.orderedWord
{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 (EndpointWord S u t)))
:
EndpointWord S u t
The ith endpoint word in canonical in-order enumeration.
Instances For
theorem
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.orderedWord_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 (EndpointWord S u t))}
:
orderedWord i < orderedWord j ↔ i < j
theorem
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.orderedWord_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 orderedWord
theorem
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.orderedWord_upperSubspace_le_lowerSubspace
{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 (EndpointWord S u t))}
(hij : i < j)
:
upperSubspace N (orderedWord i) ≤ lowerSubspace N (orderedWord j)
Upper endpoints of earlier canonical words lie below the lower endpoint of every later word.
noncomputable def
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.cumulativeWordSubspace
{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 (EndpointWord S u t) + 1))
:
Cumulative upper endpoints before the cut j in the finite word order.
Instances For
theorem
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.cumulativeWordSubspace_le_lowerSubspace
{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 (EndpointWord S u t)))
:
cumulativeWordSubspace N j.castSucc ≤ lowerSubspace N (orderedWord j)
Before the jth word, the cumulative upper endpoints lie in its lower
endpoint.
theorem
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.lowerSubspace_le_cumulativeWordSubspace
{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 (EndpointWord S u t)))
:
lowerSubspace N (orderedWord j) ≤ cumulativeWordSubspace N j.castSucc
Coverage and avoidance leave no gap before any word interval.
theorem
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.cumulativeWordSubspace_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 (EndpointWord S u t)))
:
cumulativeWordSubspace N j.castSucc = lowerSubspace N (orderedWord j)
The cumulative cut immediately before a word is exactly its lower endpoint.
theorem
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.cumulativeWordSubspace_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 (EndpointWord S u t)))
:
cumulativeWordSubspace N j.succ = upperSubspace N (orderedWord j)
Adding the jth upper endpoint makes the cumulative cut exactly that
upper endpoint.
theorem
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.cumulativeWordSubspace_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))
:
cumulativeWordSubspace N 0 = ⊥
The initial cumulative word cut is zero.
theorem
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.cumulativeWordSubspace_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))
:
cumulativeWordSubspace N (Fin.last (Nat.card (EndpointWord S u t))) = ⊤
Coverage makes the final cumulative word cut the whole vertex space.
noncomputable def
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.orderedWordFiltration
{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 (EndpointWord S u t))
The canonical finite filtration supplied by one endpoint polarization.
Instances For
theorem
MagnitudeConjecture.BoundQuiver.StringWord.EndpointWord.orderedWordFiltration_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))))
(orderedWordFiltration M) (orderedWordFiltration N)
Every module morphism preserves the canonical polarized word filtrations.