Quiver
Results named in Tau Ceti's TauCeti.RepresentationTheory.Quiver modules and in no roadmap's section, as Tau Ceti has them at commit ace60277.
TheoremCouture's graded classification by Aut(G)-orbits on H¹(G, kˣ)#
Over a nontrivial
commutative ring with only trivial idempotents, the cohomology classes of two parameters lie
in the same graph-automorphism orbit exactly when their skew-zigzag relation quotients are
graded isomorphic. Together with cohomologyClass_surjective, this describes all graded
isomorphism classes of the relation quotients arising from skew-zigzag parameters.
TauCeti.SkewZigzagParameter.exists_firstCohomologyRelabel_eq_iff_exists_graded_algEquiv.{u, w}
{k : Type w} [CommRing k] [Nontrivial k] {V : Type u} [Finite V] {G : SimpleGraph V}
{c c' : TauCeti.SkewZigzagParameter k G}
(hidempotents : ∀ (e : k), IsIdempotentElem e → e = 0 ∨ e = 1) :
(∃ τ,
(SimpleGraph.firstCohomologyRelabel kˣ τ)
((TauCeti.SkewZigzagParameter.cohomologyClass k G) c) =
(TauCeti.SkewZigzagParameter.cohomologyClass k G) c') ↔
∃ φ,
∀ (n : ℕ) (x : TauCeti.skewZigzagQuotient k G c),
φ x ∈ TauCeti.skewZigzagGrade k G c' n ↔ x ∈ TauCeti.skewZigzagGrade k G c n
Lean
Formalized in Tau Ceti as TauCeti.SkewZigzagParameter.exists_firstCohomologyRelabel_eq_iff_exists_graded_algEquiv.
Sources
TheoremThe entrywise graded Cartan formula#
The diagonal entries are 1 + q², the entries over an
edge are q, and all the others vanish.
TauCeti.zigzagGradedCartanMatrix_apply.{u, w} (k : Type w) [Field k] {V : Type u}
(G : SimpleGraph V) [Finite V] (hns : ∀ (i : V), ∃ j, G.Adj i j) [DecidableEq V]
[DecidableRel G.Adj] (i j : V) :
TauCeti.zigzagGradedCartanMatrix k G i j =
(if i = j then 1 + Polynomial.X ^ 2 else 0) + if G.Adj i j then Polynomial.X else 0
Used by 1
TheoremGabriel's presentation theorem#
Every finite-dimensional algebra A over an algebraically
closed field k is Morita equivalent to a bound quiver algebra: there are a finite quiver Q
and an admissible ideal I of the path algebra kQ such that A is Morita equivalent to
kQ ⧸ I. The algebra kQ ⧸ I is isomorphic to the basic corner eAe of A
(TauCeti.IsSemiperfectRing.exists_isIdempotentElem_full_isBasic_corner), presented by
TauCeti.IsBasic.exists_surjective_pathAlgebra_isAdmissibleIdeal_ker.
TauCeti.exists_quiver_admissibleIdeal_morita.{u, w} (k : Type w) (A : Type u) [Field k]
[IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] :
∃ Q x,
∃ (x_1 : Finite Q) (_ : ∀ (i j : Q), Finite (i ⟶ j)),
∃ I,
∃ (x_3 : I.IsTwoSided),
TauCeti.IsAdmissibleIdeal I ∧ IsMoritaEquivalent k A (TauCeti.pathAlgebra k Q ⧸ I)
Lean
Formalized in Tau Ceti as TauCeti.exists_quiver_admissibleIdeal_morita.
Other forms
Gabriel's presentation theorem for basic algebras. Formalized in Tau Ceti as TauCeti.IsBasic.exists_surjective_pathAlgebra_isAdmissibleIdeal_ker.
TauCeti.IsBasic.exists_surjective_pathAlgebra_isAdmissibleIdeal_ker.{u, w} {k : Type w} {A : Type u}
[Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A]
(hA : TauCeti.IsBasic A) :
∃ Q x,
∃ (x_1 : Finite Q) (_ : ∀ (i j : Q), Finite (i ⟶ j)),
∃ F, Function.Surjective ⇑F ∧ TauCeti.IsAdmissibleIdeal (RingHom.ker F.toRingHom)
Sources
TheoremThe Hilbert series identity for a quiver without sinks#
If every vertex of Q is the tail
of an arrow and A_{v,w} = #(w ⟶ v) is the arrow-count matrix of the doubled quiver, then
((1 + X²) I - X A) H = I for the matrix Hilbert series H of Π.
TauCeti.mul_preprojectiveHilbertSeries_eq_one.{u, v, w} (k : Type w) {Q : Type u} [Field k]
[Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] (hQ : ∀ (u : Q), ∃ w, Nonempty (u ⟶ w))
[DecidableEq Q] :
((1 + PowerSeries.X ^ 2) • 1 -
PowerSeries.X •
Matrix.of fun v w =>
↑(Fintype.card (Quiver.Symmetrify.of.obj w ⟶ Quiver.Symmetrify.of.obj v))) *
TauCeti.preprojectiveHilbertSeries k Q =
1
Lean
Formalized in Tau Ceti as TauCeti.mul_preprojectiveHilbertSeries_eq_one.
Other forms
The Hilbert series identity for a quiver with a superadditive weight. Formalized in Tau Ceti as TauCeti.mul_preprojectiveHilbertSeries_eq_one_of_two_mul_le_sum.
TauCeti.mul_preprojectiveHilbertSeries_eq_one_of_two_mul_le_sum.{u, v, w, u_1} (k : Type w)
{Q : Type u} [Field k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] [DecidableEq Q]
{S : Type u_1} [CommRing S] [LinearOrder S] [IsStrictOrderedRing S] {δ : Q → S}
(hδ : ∀ (i : Q), 0 < δ i)
(hδle : ∀ (i : Q), 2 * δ i ≤ ∑ j, ↑(Fintype.card (i ⟶ j) + Fintype.card (j ⟶ i)) * δ j) :
((1 + PowerSeries.X ^ 2) • 1 -
PowerSeries.X •
Matrix.of fun v w =>
↑(Fintype.card (Quiver.Symmetrify.of.obj w ⟶ Quiver.Symmetrify.of.obj v))) *
TauCeti.preprojectiveHilbertSeries k Q =
1
Sources
Uses 1
TheoremThe Koszul defect formula#
For vertices i and v and every degree m,
dim e_v Π_{m+2} e_i + dim e_v Π_m e_i = ∑_w #(w ⟶ v) dim e_w Π_{m+1} e_i + dim K_m(i, v),
the sum running over the arrows of the doubled quiver into v, where K_m(i, v) is the space of
y ∈ e_v Π_m e_i killed by the reverse b* of every arrow b into v, the kernel of the left
map of the Koszul complex of S_v.
TauCeti.finrank_preprojectiveCorner_add_two_add_finrank_preprojectiveCorner.{u, v, w} (k : Type w)
(Q : Type u) [Field k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] (m : ℕ)
(i : Quiver.Symmetrify Q) (v : Q) :
Module.finrank k ↥(TauCeti.preprojectiveCorner k Q (m + 2) i (Quiver.Symmetrify.of.obj v)) +
Module.finrank k ↥(TauCeti.preprojectiveCorner k Q m i (Quiver.Symmetrify.of.obj v)) =
∑ w,
Fintype.card (w ⟶ Quiver.Symmetrify.of.obj v) *
Module.finrank k ↥(TauCeti.preprojectiveCorner k Q (m + 1) i w) +
Module.finrank k
↥(TauCeti.preprojectiveCorner k Q m i (Quiver.Symmetrify.of.obj v) ⊓
⨅ w,
⨅ b,
(LinearMap.mulLeft k
((TauCeti.preprojectiveMk k Q)
(TauCeti.PathAlgebra.ofArrow (Quiver.reverse b)))).ker)
Lean
Formalized in Tau Ceti as TauCeti.finrank_preprojectiveCorner_add_two_add_finrank_preprojectiveCorner.
Sources
TheoremThe Krull-Schmidt theorem for quiver representations#
If a pointwise finite-dimensional representation of a finite quiver is isomorphic to a finite biproduct of indecomposable representations in two ways, the two families of summands are matched by a bijection of their index sets under which corresponding summands are isomorphic.
TauCeti.QuiverRep.exists_indecomposable_iso_biproduct supplies such an isomorphism.
TauCeti.QuiverRep.exists_equiv_iso_of_iso_biproduct.{u, v, w, t} {k : Type u} {Q : Type v} [Field k]
[Quiver Q] [Finite Q] {ι κ : Type} [Finite ι] [Finite κ] {P : ι → TauCeti.QuiverRep k Q}
{R : κ → TauCeti.QuiverRep k Q} {M : TauCeti.QuiverRep k Q} (hM : TauCeti.IsFinDim k Q M)
(eP : M ≅ ⨁ P) (eR : M ≅ ⨁ R) (hP : ∀ (i : ι), CategoryTheory.Indecomposable (P i))
(hR : ∀ (j : κ), CategoryTheory.Indecomposable (R j)) : ∃ e, ∀ (i : ι), Nonempty (P i ≅ R (e i))
Lean
Formalized in Tau Ceti as TauCeti.QuiverRep.exists_equiv_iso_of_iso_biproduct.
Other forms
The Krull-Schmidt theorem with no ambient representation. Formalized in Tau Ceti as TauCeti.QuiverRep.exists_equiv_iso_of_biproduct_iso.
TauCeti.QuiverRep.exists_equiv_iso_of_biproduct_iso.{u, v, w, t} {k : Type u} {Q : Type v} [Field k]
[Quiver Q] [Finite Q] {ι κ : Type} [Finite ι] [Finite κ] {P : ι → TauCeti.QuiverRep k Q}
{R : κ → TauCeti.QuiverRep k Q} (h : TauCeti.IsFinDim k Q (⨁ P)) (e : ⨁ P ≅ ⨁ R)
(hP : ∀ (i : ι), CategoryTheory.Indecomposable (P i))
(hR : ∀ (j : κ), CategoryTheory.Indecomposable (R j)) : ∃ f, ∀ (i : ι), Nonempty (P i ≅ R (f i))
Sources
Uses 1
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.