Incidence tables with zero relations #
For Case 2 of Lemma 8.11 (local-ray-geometry.tex) the paper uses a tree category with
one zero relation (F = 1 in Lemma 8.8). Here: the incidence table of a finite poset with a
set Z of comparable pairs declared zero, closed under extension (incZ), and configurations
of it in a ray table (ConfZ), which make its linearization representation-finite when kP
is (Lemmas 8.9 and C.1 as in TableConf).
@[reducible, inline]
Comparable pairs outside Z.
Instances For
structure
MultiplicativeBasisDeformations.RaySys.ZeroSet
(Q : Type)
[PartialOrder Q]
(Z : Q → Q → Prop)
:
A zero set: closed under extension, and containing no identity pair.
- ext (a b c d : Q) : Z b c → a ≤ b → c ≤ d → Z a d
- irrefl (a : Q) : ¬Z a a
Instances For
theorem
MultiplicativeBasisDeformations.RaySys.mulZ_assoc
{Q : Type}
[PartialOrder Q]
[Fintype Q]
[DecidableEq Q]
[DecidableLE Q]
{Z : Q → Q → Prop}
[DecidableRel Z]
(hZ : ZeroSet Q Z)
(p p' p'' : IPZ Q Z)
:
theorem
MultiplicativeBasisDeformations.RaySys.incZ_mul_of
{Q : Type}
[PartialOrder Q]
[Fintype Q]
[DecidableEq Q]
[DecidableLE Q]
{Z : Q → Q → Prop}
[DecidableRel Z]
(hZ : ZeroSet Q Z)
(p p' : IPZ Q Z)
(h : (↑p).2 = (↑p').1)
(hz : ¬Z (↑p).1 (↑p').2)
:
structure
MultiplicativeBasisDeformations.RaySys.Tab.ConfZ
{V R L : Type}
[AddCommGroup L]
(P : Tab V R L)
(Q : Type)
[PartialOrder Q]
(Z : Q → Q → Prop)
:
A configuration of a bound poset in the graded covering category.
- v : Q → V
- g : Q → L
- ρ (a b : Q) : a ≤ b → ¬Z a b → R
Instances For
theorem
MultiplicativeBasisDeformations.RaySys.Tab.ConfZ.ρ_eq_of
{V R L : Type}
[AddCommGroup L]
[DecidableEq L]
[Fintype V]
[DecidableEq V]
[Fintype R]
[DecidableEq R]
{P : Tab V R L}
{Q : Type}
[PartialOrder Q]
[Fintype Q]
[DecidableEq Q]
[DecidableLE Q]
{Z : Q → Q → Prop}
[DecidableRel Z]
(C : P.ConfZ Q Z)
{a b : Q}
(hab : a ≤ b)
(hab' : ¬Z a b)
(h : R)
(h1 : P.src h = C.v a)
(h2 : P.tgt h = C.v b)
(h3 : P.wt h = C.g b - C.g a)
:
h = C.ρ a b hab hab'
theorem
MultiplicativeBasisDeformations.RaySys.Tab.ConfZ.ρ_self
{V R L : Type}
[AddCommGroup L]
[DecidableEq L]
[Fintype V]
[DecidableEq V]
[Fintype R]
[DecidableEq R]
{P : Tab V R L}
{Q : Type}
[PartialOrder Q]
[Fintype Q]
[DecidableEq Q]
[DecidableLE Q]
{Z : Q → Q → Prop}
[DecidableRel Z]
(hZ : ZeroSet Q Z)
(C : P.ConfZ Q Z)
(a : Q)
:
theorem
MultiplicativeBasisDeformations.RaySys.Tab.ConfZ.retL_all
{V R L : Type}
[AddCommGroup L]
[DecidableEq L]
[Fintype V]
[DecidableEq V]
[Fintype R]
[DecidableEq R]
{P : Tab V R L}
{Q : Type}
[PartialOrder Q]
[Fintype Q]
[DecidableEq Q]
[DecidableLE Q]
{Z : Q → Q → Prop}
[DecidableRel Z]
(hZ : ZeroSet Q Z)
(C : P.ConfZ Q Z)
[LocallyFiniteOrder Q]
(a b c : Q)
(hab : a ≤ b)
(hab' : ¬Z a b)
(hac : a ≤ c)
(hac' : ¬Z a c)
(h : R)
(h1 : P.src h = C.v b)
(h2 : P.tgt h = C.v c)
(h3 : P.wt h = C.g c - C.g b)
(hm : P.mul (C.ρ a b hab hab') h = some (C.ρ a c hac hac'))
:
b ≤ c
theorem
MultiplicativeBasisDeformations.RaySys.Tab.ConfZ.retR_all
{V R L : Type}
[AddCommGroup L]
[DecidableEq L]
[Fintype V]
[DecidableEq V]
[Fintype R]
[DecidableEq R]
{P : Tab V R L}
{Q : Type}
[PartialOrder Q]
[Fintype Q]
[DecidableEq Q]
[DecidableLE Q]
{Z : Q → Q → Prop}
[DecidableRel Z]
(hZ : ZeroSet Q Z)
(C : P.ConfZ Q Z)
[LocallyFiniteOrder Q]
(a b c : Q)
(hab : a ≤ b)
(hab' : ¬Z a b)
(hcb : c ≤ b)
(hcb' : ¬Z c b)
(h : R)
(h1 : P.src h = C.v c)
(h2 : P.tgt h = C.v a)
(h3 : P.wt h = C.g a - C.g c)
(hm : P.mul h (C.ρ a b hab hab') = some (C.ρ c b hcb hcb'))
:
c ≤ a
theorem
MultiplicativeBasisDeformations.RaySys.Tab.ConfZ.emb_injective
{V R L : Type}
[AddCommGroup L]
[DecidableEq L]
[Fintype V]
[DecidableEq V]
[Fintype R]
[DecidableEq R]
{P : Tab V R L}
{Q : Type}
[PartialOrder Q]
[Fintype Q]
[DecidableEq Q]
[DecidableLE Q]
{Z : Q → Q → Prop}
[DecidableRel Z]
(C : P.ConfZ Q Z)
[LocallyFiniteOrder Q]
:
Function.Injective C.emb
def
MultiplicativeBasisDeformations.RaySys.Tab.ConfZ.mor
{V R L : Type}
[AddCommGroup L]
[DecidableEq L]
[Fintype V]
[DecidableEq V]
[Fintype R]
[DecidableEq R]
{P : Tab V R L}
{Q : Type}
[PartialOrder Q]
[Fintype Q]
[DecidableEq Q]
[DecidableLE Q]
{Z : Q → Q → Prop}
[DecidableRel Z]
(hZ : ZeroSet Q Z)
(C : P.ConfZ Q Z)
:
The selected rays embed the bound incidence table into the graded cover.
Instances For
theorem
MultiplicativeBasisDeformations.RaySys.Tab.ConfZ.hL
{V R L : Type}
[AddCommGroup L]
[DecidableEq L]
[Fintype V]
[DecidableEq V]
[Fintype R]
[DecidableEq R]
{P : Tab V R L}
{Q : Type}
[PartialOrder Q]
[Fintype Q]
[DecidableEq Q]
[DecidableLE Q]
{Z : Q → Q → Prop}
[DecidableRel Z]
(hZ : ZeroSet Q Z)
(C : P.ConfZ Q Z)
[LocallyFiniteOrder Q]
[LocallyFiniteOrder Q]
(s : IPZ Q Z)
(t : P.CR C.v P.wt C.g)
(t' : IPZ Q Z)
(hm : (P.cover C.v P.wt ⋯ C.g).mul (C.emb s) t = some (C.emb t'))
:
theorem
MultiplicativeBasisDeformations.RaySys.Tab.ConfZ.hR
{V R L : Type}
[AddCommGroup L]
[DecidableEq L]
[Fintype V]
[DecidableEq V]
[Fintype R]
[DecidableEq R]
{P : Tab V R L}
{Q : Type}
[PartialOrder Q]
[Fintype Q]
[DecidableEq Q]
[DecidableLE Q]
{Z : Q → Q → Prop}
[DecidableRel Z]
(hZ : ZeroSet Q Z)
(C : P.ConfZ Q Z)
[LocallyFiniteOrder Q]
[LocallyFiniteOrder Q]
(s : IPZ Q Z)
(t : P.CR C.v P.wt C.g)
(t' : IPZ Q Z)
(hm : (P.cover C.v P.wt ⋯ C.g).mul t (C.emb s) = some (C.emb t'))
:
theorem
MultiplicativeBasisDeformations.RaySys.Tab.ConfZ.isRepresentationFinite
{V R L : Type}
[AddCommGroup L]
[DecidableEq L]
[Fintype V]
[DecidableEq V]
[Fintype R]
[DecidableEq R]
{P : Tab V R L}
{Q : Type}
[PartialOrder Q]
[Fintype Q]
[DecidableEq Q]
[DecidableLE Q]
{Z : Q → Q → Prop}
[DecidableRel Z]
(hZ : ZeroSet Q Z)
(C : P.ConfZ Q Z)
[LocallyFiniteOrder Q]
[LocallyFiniteOrder Q]
(k : Type u)
[Field k]
(h : IsRepresentationFinite k ↥(P.Lin k))
:
IsRepresentationFinite k ↥((incZ hZ).Lin k)
A bound configuration makes the bound incidence algebra representation-finite.