Radical layers of vertex projectives over a zigzag algebra

For a finite simple graph without isolated vertices, the vertex projective P_i = Z e_i has Loewy length three. Its first radical power is spanned by the arrows leaving i together with the volume at i; its second radical power is the volume line; and its third radical power is zero. Consequently the head and socle layers are one-dimensional, while the middle layer has dimension equal to the degree of i.

The powers here are defined intrinsically by the algebra radical acting on P_i.

Main definitions

• TauCeti.zigzagProjectiveRadicalPower: the submodule J^n P_i.
• TauCeti.zigzagProjectiveRadicalLayer: the quotient J^n P_i / J^(n+1) P_i.

Main results

• TauCeti.mem_zigzagProjectiveRadicalPower_one_iff: J P_i is the positive-degree part of P_i.
• TauCeti.mem_zigzagProjectiveRadicalPower_two_iff: J^2 P_i is the volume line.
• TauCeti.zigzagProjectiveRadicalPower_three_eq_bot: J^3 P_i = 0.
• TauCeti.isSimpleModule_zigzagProjectiveRadicalLayer_zero: the head is simple.
• TauCeti.socle_zigzagProjective_eq_radicalPower_two: the socle is J² P_i.
• TauCeti.finrank_zigzagProjectiveRadicalLayer_zero, TauCeti.finrank_zigzagProjectiveRadicalLayer_one, and TauCeti.finrank_zigzagProjectiveRadicalLayer_two: the dimensions 1, deg(i), and 1.

References

See R. Huerfano and M. Khovanov, A category for the adjoint representation, Section 3, and M. Ehrig and D. Tubbenhauer, Algebraic properties of zigzag algebras, Section 2.

noncomputable def TauCeti.zigzagProjectiveRadicalPower (k : Type w) [Field k] {V : Type u} (G : SimpleGraph V) [Finite V] (i : V) (n : ℕ) : Submodule (nonisolatedZigzagQuotient k G) ↥(zigzagProjective k G i)

The n-th radical power of the vertex projective P_i = Z e_i, namely J^n P_i.

theorem TauCeti.mem_zigzagProjectiveRadicalPower_iff (k : Type w) [Field k] {V : Type u} (G : SimpleGraph V) [Finite V] (i : V) (n : ℕ) (x : ↥(zigzagProjective k G i)) : x ∈ zigzagProjectiveRadicalPower k G i n ↔ ↑x ∈ Ring.jacobson (nonisolatedZigzagQuotient k G) ^ n

An element of P_i belongs to J^n P_i exactly when its underlying algebra element belongs to J^n.

@[simp]

theorem TauCeti.zigzagProjectiveRadicalPower_zero (k : Type w) [Field k] {V : Type u} (G : SimpleGraph V) [Finite V] (i : V) : zigzagProjectiveRadicalPower k G i 0 = ⊤

theorem TauCeti.zigzagProjectiveRadicalPower_antitone (k : Type w) [Field k] {V : Type u} (G : SimpleGraph V) [Finite V] (i : V) : Antitone (zigzagProjectiveRadicalPower k G i)

The radical powers of a vertex projective form a descending filtration.

@[reducible, inline]

noncomputable abbrev TauCeti.zigzagProjectiveRadicalLayer (k : Type w) [Field k] {V : Type u} (G : SimpleGraph V) [Finite V] (i : V) (n : ℕ) : Type (max u w)

The n-th radical layer of the vertex projective, J^n P_i / J^(n+1) P_i.

@[simp]

theorem TauCeti.mem_zigzagProjectiveRadicalPower_one_iff {k : Type w} [Field k] {V : Type u} {G : SimpleGraph V} [Finite V] (hns : ∀ (i : V), ∃ (j : V), G.Adj i j) (i : V) (x : ↥(zigzagProjective k G i)) : x ∈ zigzagProjectiveRadicalPower k G i 1 ↔ ↑x ∈ zigzagPositiveSpan k G

The first radical power of P_i consists exactly of the elements whose underlying algebra element has positive path length.

@[simp]

theorem TauCeti.mem_zigzagProjectiveRadicalPower_two_iff {k : Type w} [Field k] {V : Type u} {G : SimpleGraph V} [Finite V] (hns : ∀ (i : V), ∃ (j : V), G.Adj i j) (i : V) (x : ↥(zigzagProjective k G i)) : x ∈ zigzagProjectiveRadicalPower k G i 2 ↔ ↑x ∈ zigzagVolumeSpan k G

The second radical power of P_i consists exactly of the elements whose underlying algebra element lies in the span of the volume classes.

theorem TauCeti.zigzagProjectiveRadicalPower_three_eq_bot {k : Type w} [Field k] {V : Type u} {G : SimpleGraph V} [Finite V] (hns : ∀ (i : V), ∃ (j : V), G.Adj i j) (i : V) : zigzagProjectiveRadicalPower k G i 3 = ⊥

The third radical power of every vertex projective vanishes.

noncomputable def TauCeti.zigzagProjectiveVolume (k : Type w) [Field k] {V : Type u} (G : SimpleGraph V) [Finite V] (i : V) : ↥(zigzagProjective k G i)

The volume vector in the vertex projective P_i.

theorem TauCeti.zigzagProjectiveBasisFun_inr_inr (k : Type w) [Field k] {V : Type u} (G : SimpleGraph V) [Finite V] (i : V) (a : Unit) : zigzagProjectiveBasisFun k G i (Sum.inr (Sum.inr a)) = zigzagProjectiveVolume k G i

The degree-two projective basis vector is its volume vector.

@[simp]

theorem TauCeti.coe_zigzagProjectiveVolume (k : Type w) [Field k] {V : Type u} (G : SimpleGraph V) [Finite V] (i : V) : ↑(zigzagProjectiveVolume k G i) = zigzagVolume k G i

noncomputable def TauCeti.zigzagProjectiveHeadCoeff (k : Type w) [Field k] {V : Type u} (G : SimpleGraph V) [Finite V] (i : V) : ↥(zigzagProjective k G i) →ₗ[k] k

The head-coordinate map on P_i. It reads the coefficient of e_i, equivalently the value at i of the vertex-coefficient homomorphism of the zigzag algebra.

@[simp]

theorem TauCeti.zigzagProjectiveHeadCoeff_apply (k : Type w) [Field k] {V : Type u} (G : SimpleGraph V) [Finite V] (i : V) (x : ↥(zigzagProjective k G i)) : (zigzagProjectiveHeadCoeff k G i) x = (zigzagTrivialCoeff k G) (↑x) (DoubledQuiver.vertex G i)

theorem TauCeti.zigzagProjectiveHeadCoeff_generator (k : Type w) [Field k] {V : Type u} (G : SimpleGraph V) [Finite V] (i : V) : (zigzagProjectiveHeadCoeff k G i) (zigzagProjectiveGenerator k G i) = 1

theorem TauCeti.zigzagProjectiveHeadCoeff_surjective (k : Type w) [Field k] {V : Type u} (G : SimpleGraph V) [Finite V] (i : V) : Function.Surjective ⇑(zigzagProjectiveHeadCoeff k G i)

The head-coordinate map is onto.

noncomputable def TauCeti.zigzagProjectiveVolumeLine (k : Type w) [Field k] {V : Type u} (G : SimpleGraph V) [Finite V] (i : V) : Submodule k ↥(zigzagProjective k G i)

The one-dimensional volume line inside P_i.

@[simp]

theorem TauCeti.mem_zigzagProjectiveVolumeLine_iff (k : Type w) [Field k] {V : Type u} (G : SimpleGraph V) [Finite V] (i : V) (x : ↥(zigzagProjective k G i)) : x ∈ zigzagProjectiveVolumeLine k G i ↔ ∃ (c : k), c • zigzagProjectiveVolume k G i = x

Membership in the volume line means being a scalar multiple of the volume vector.

theorem TauCeti.restrictScalars_zigzagProjectiveRadicalPower_two_eq_volumeLine {k : Type w} [Field k] {V : Type u} {G : SimpleGraph V} [Finite V] (hns : ∀ (i : V), ∃ (j : V), G.Adj i j) (i : V) : Submodule.restrictScalars k (zigzagProjectiveRadicalPower k G i 2) = zigzagProjectiveVolumeLine k G i

The second radical power of P_i, after restriction to the coefficient field, is exactly the line spanned by its volume vector.

The first radical power and the head coordinate

theorem TauCeti.ker_zigzagProjectiveHeadCoeff_eq_restrictScalars_radicalPower_one {k : Type w} [Field k] {V : Type u} {G : SimpleGraph V} [Finite V] (hns : ∀ (i : V), ∃ (j : V), G.Adj i j) (i : V) : (zigzagProjectiveHeadCoeff k G i).ker = Submodule.restrictScalars k (zigzagProjectiveRadicalPower k G i 1)

The kernel of the head-coordinate map is the first radical power of P_i.

theorem TauCeti.finrank_restrictScalars_zigzagProjectiveRadicalPower_one {k : Type w} [Field k] {V : Type u} {G : SimpleGraph V} [Finite V] [Fintype V] [DecidableRel G.Adj] (hns : ∀ (i : V), ∃ (j : V), G.Adj i j) (i : V) : Module.finrank k ↥(zigzagProjectiveRadicalPower k G i 1) = G.degree i + 1

The first radical power of P_i has dimension deg(i) + 1: its basis consists of the outgoing arrows and the volume vector.

theorem TauCeti.finrank_restrictScalars_zigzagProjectiveRadicalPower_two {k : Type w} [Field k] {V : Type u} {G : SimpleGraph V} [Finite V] (hns : ∀ (i : V), ∃ (j : V), G.Adj i j) (i : V) : Module.finrank k ↥(zigzagProjectiveRadicalPower k G i 2) = 1

The second radical power of P_i is one-dimensional.

theorem TauCeti.isSimpleModule_zigzagProjectiveRadicalPower_two {k : Type w} [Field k] {V : Type u} {G : SimpleGraph V} [Finite V] (hns : ∀ (i : V), ∃ (j : V), G.Adj i j) (i : V) : IsSimpleModule (nonisolatedZigzagQuotient k G) ↥(zigzagProjectiveRadicalPower k G i 2)

The second radical power of P_i is a simple module over the zigzag algebra.

theorem TauCeti.socle_zigzagProjective_eq_radicalPower_two {k : Type w} [Field k] {V : Type u} {G : SimpleGraph V} [Finite V] (hns : ∀ (i : V), ∃ (j : V), G.Adj i j) (i : V) : socle (nonisolatedZigzagQuotient k G) ↥(zigzagProjective k G i) = zigzagProjectiveRadicalPower k G i 2

The socle of P_i is its second radical power, the simple line spanned by the volume at i.

theorem TauCeti.finrank_restrictScalars_zigzagProjectiveRadicalPower_of_three_le {k : Type w} [Field k] {V : Type u} {G : SimpleGraph V} [Finite V] (hns : ∀ (i : V), ∃ (j : V), G.Adj i j) (i : V) {n : ℕ} (hn : 3 ≤ n) : Module.finrank k ↥(zigzagProjectiveRadicalPower k G i n) = 0

Every radical power from the third onward has dimension zero.

Dimensions of the radical layers

theorem TauCeti.finrank_zigzagProjectiveRadicalLayer_add_finrank_succ {k : Type w} [Field k] {V : Type u} {G : SimpleGraph V} [Finite V] (hns : ∀ (i : V), ∃ (j : V), G.Adj i j) (i : V) (n : ℕ) : Module.finrank k (zigzagProjectiveRadicalLayer k G i n) + Module.finrank k ↥(zigzagProjectiveRadicalPower k G i n.succ) = Module.finrank k ↥(zigzagProjectiveRadicalPower k G i n)

Rank-nullity for consecutive radical powers: the dimension of J^n P_i / J^(n+1) P_i plus the dimension of the lower power is the dimension of the upper power.

theorem TauCeti.finrank_zigzagProjectiveRadicalLayer_zero {k : Type w} [Field k] {V : Type u} {G : SimpleGraph V} [Finite V] (hns : ∀ (i : V), ∃ (j : V), G.Adj i j) (i : V) : Module.finrank k (zigzagProjectiveRadicalLayer k G i 0) = 1

The head layer P_i / J P_i is one-dimensional.

theorem TauCeti.isSimpleModule_zigzagProjectiveRadicalLayer_zero {k : Type w} [Field k] {V : Type u} {G : SimpleGraph V} [Finite V] (hns : ∀ (i : V), ∃ (j : V), G.Adj i j) (i : V) : IsSimpleModule (nonisolatedZigzagQuotient k G) (zigzagProjectiveRadicalLayer k G i 0)

The head P_i / J P_i is a simple module over the zigzag algebra. Its one-dimensional coefficient-field structure forces every nonzero vector to generate it already under scalars.

theorem TauCeti.finrank_zigzagProjectiveRadicalLayer_one {k : Type w} [Field k] {V : Type u} {G : SimpleGraph V} [Finite V] [Fintype V] [DecidableRel G.Adj] (hns : ∀ (i : V), ∃ (j : V), G.Adj i j) (i : V) : Module.finrank k (zigzagProjectiveRadicalLayer k G i 1) = G.degree i

The middle radical layer J P_i / J² P_i has one dimension for each edge incident to i.

theorem TauCeti.finrank_zigzagProjectiveRadicalLayer_two {k : Type w} [Field k] {V : Type u} {G : SimpleGraph V} [Finite V] (hns : ∀ (i : V), ∃ (j : V), G.Adj i j) (i : V) : Module.finrank k (zigzagProjectiveRadicalLayer k G i 2) = 1

The socle layer J² P_i / J³ P_i is one-dimensional.