Kernels and images of right multiplication between zigzag vertex projectives

For a finite simple graph without isolated vertices, a homomorphism between vertex projectives P_j = Z e_j → P_i = Z e_i of the zigzag relation quotient is right multiplication by an element of the corner e_j Z e_i. This file computes the kernel and the image, in terms of the radical filtration P_i ⊇ J P_i ⊇ J² P_i ⊇ 0, of the two kinds of homogeneous maps of positive degree:

• right multiplication by the volume class x_i, an endomorphism of P_i of degree two, has image the socle J² P_i and kernel the radical J P_i, at every vertex; and
• right multiplication by the arrow of a dart d, a map P_{d.snd} → P_{d.fst} of degree one, always has image in J P_{d.fst} and kills J² P_{d.snd}. Its image is all of J P_{d.fst} when the tail d.fst has degree one, and its kernel is exactly J² P_{d.snd} when the head d.snd has degree one.

Together with the quotient P_i → P_i / J P_i onto the simple head, whose kernel is J P_i, these are the exactness statements behind the explicit projective resolutions of the simple modules of low-rank zigzag algebras.

Main definitions

• TauCeti.zigzagProjectiveVolumeMul: right multiplication by x_i on P_i.
• TauCeti.zigzagProjectiveArrowMul: right multiplication by the arrow of d, P_{d.snd} → P_{d.fst}.
• TauCeti.zigzagProjectiveToHead: the quotient of P_i onto its head P_i / J P_i.

Main results

• TauCeti.range_zigzagProjectiveVolumeMul and TauCeti.ker_zigzagProjectiveVolumeMul: the image J² P_i and the kernel J P_i of the volume map.
• TauCeti.range_zigzagProjectiveArrowMul and TauCeti.ker_zigzagProjectiveArrowMul: the image J P_{d.fst} and the kernel J² P_{d.snd} of the arrow map, at vertices of degree one.
• TauCeti.ker_zigzagProjectiveToHead: the kernel J P_i of the head quotient.

References

See Huerfano--Khovanov, A category for the adjoint representation, Section 3, for the projective modules of zigzag algebras and the maps between them.

The maps

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

Right multiplication by the volume class x_i, as an endomorphism of the vertex projective P_i = Z e_i.

@[simp]

theorem TauCeti.coe_zigzagProjectiveVolumeMul_apply (k : Type w) [Field k] {V : Type u} (G : SimpleGraph V) [Finite V] (i : V) (y : ↥(zigzagProjective k G i)) : ↑((zigzagProjectiveVolumeMul k G i) y) = ↑y * zigzagVolume k G i

noncomputable def TauCeti.zigzagProjectiveArrowMul (k : Type w) [Field k] {V : Type u} (G : SimpleGraph V) [Finite V] (d : G.Dart) : ↥(zigzagProjective k G d.toProd.2) →ₗ[nonisolatedZigzagQuotient k G] ↥(zigzagProjective k G d.toProd.1)

Right multiplication by the arrow of a dart d, as a homomorphism of vertex projectives P_{d.snd} → P_{d.fst}.

@[simp]

theorem TauCeti.coe_zigzagProjectiveArrowMul_apply (k : Type w) [Field k] {V : Type u} (G : SimpleGraph V) [Finite V] (d : G.Dart) (y : ↥(zigzagProjective k G d.toProd.2)) : ↑((zigzagProjectiveArrowMul k G d) y) = ↑y * (zigzagMk k G) (PathAlgebra.ofArrow (DoubledQuiver.arrow G ⋯))

theorem TauCeti.zigzagProjectiveArrowMul_mem_grade (k : Type w) [Field k] {V : Type u} (G : SimpleGraph V) [Finite V] (d : G.Dart) {p : ℤ} {x : ↥(zigzagProjective k G d.toProd.2)} (hx : x ∈ zigzagProjectiveGrade k G d.toProd.2 p) : (zigzagProjectiveArrowMul k G d) x ∈ zigzagProjectiveGrade k G d.toProd.1 (p + 1)

Right multiplication by an arrow raises the path degree by one. With the source shifted by one, this is a degree-zero map in a linear projective presentation.

@[simp]

theorem TauCeti.zigzagProjectiveArrowMul_comp_zigzagProjectiveVolumeMul (k : Type w) [Field k] {V : Type u} (G : SimpleGraph V) [Finite V] (d : G.Dart) : zigzagProjectiveArrowMul k G d ∘ₗ zigzagProjectiveVolumeMul k G d.toProd.2 = 0

An arrow map after the volume map at its source vanishes: x_{d.snd} a_d has path length three.

@[simp]

theorem TauCeti.zigzagProjectiveVolumeMul_comp_zigzagProjectiveArrowMul (k : Type w) [Field k] {V : Type u} (G : SimpleGraph V) [Finite V] (d : G.Dart) : zigzagProjectiveVolumeMul k G d.toProd.1 ∘ₗ zigzagProjectiveArrowMul k G d = 0

The volume map at the target of an arrow map, after it, vanishes: a_d x_{d.fst} has path length three.

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

The quotient of the vertex projective P_i onto its head P_i / J P_i, the radical layer TauCeti.zigzagProjectiveRadicalLayer k G i 0.

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

The head quotient is onto.

@[simp]

theorem TauCeti.zigzagProjectiveToHead_apply {k : Type w} [Field k] {V : Type u} {G : SimpleGraph V} [Finite V] (i : V) (y : ↥(zigzagProjective k G i)) : (zigzagProjectiveToHead k G i) y = Submodule.Quotient.mk ⟨y, ⋯⟩

The head quotient sends y ∈ P_i = J⁰ P_i to its class modulo J P_i.

@[simp]

theorem TauCeti.ker_zigzagProjectiveToHead {k : Type w} [Field k] {V : Type u} {G : SimpleGraph V} [Finite V] (i : V) : (zigzagProjectiveToHead k G i).ker = zigzagProjectiveRadicalPower k G i 1

The kernel of the head quotient is the radical J P_i.

Radical bookkeeping

The volume map

@[simp]

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

The image of the volume map is the socle J² P_i.

@[simp]

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

The kernel of the volume map is the radical J P_i.

The arrow map

theorem TauCeti.range_zigzagProjectiveArrowMul_le {k : Type w} [Field k] {V : Type u} {G : SimpleGraph V} [Finite V] (d : G.Dart) : (zigzagProjectiveArrowMul k G d).range ≤ zigzagProjectiveRadicalPower k G d.toProd.1 1

The image of an arrow map lies in the radical of its target.

theorem TauCeti.zigzagProjectiveRadicalPower_two_le_ker_zigzagProjectiveArrowMul {k : Type w} [Field k] {V : Type u} {G : SimpleGraph V} [Finite V] (hns : ∀ (i : V), ∃ (j : V), G.Adj i j) (d : G.Dart) : zigzagProjectiveRadicalPower k G d.toProd.2 2 ≤ (zigzagProjectiveArrowMul k G d).ker

An arrow map kills the socle of its source.

@[simp]

theorem TauCeti.zigzagProjectiveToHead_comp_zigzagProjectiveArrowMul {k : Type w} [Field k] {V : Type u} {G : SimpleGraph V} [Finite V] (d : G.Dart) : zigzagProjectiveToHead k G d.toProd.1 ∘ₗ zigzagProjectiveArrowMul k G d = 0

The head quotient at d.fst kills the image of the arrow map of d.

@[simp]

theorem TauCeti.range_zigzagProjectiveArrowMul {k : Type w} [Field k] {V : Type u} {G : SimpleGraph V} [Finite V] (hns : ∀ (i : V), ∃ (j : V), G.Adj i j) [Fintype V] [DecidableRel G.Adj] (d : G.Dart) (hd : G.degree d.toProd.1 = 1) : (zigzagProjectiveArrowMul k G d).range = zigzagProjectiveRadicalPower k G d.toProd.1 1

At a tail of degree one, the image of an arrow map is the radical J P_{d.fst}.

@[simp]

theorem TauCeti.ker_zigzagProjectiveArrowMul {k : Type w} [Field k] {V : Type u} {G : SimpleGraph V} [Finite V] (hns : ∀ (i : V), ∃ (j : V), G.Adj i j) [Fintype V] [DecidableRel G.Adj] (d : G.Dart) (hd : G.degree d.toProd.2 = 1) : (zigzagProjectiveArrowMul k G d).ker = zigzagProjectiveRadicalPower k G d.toProd.2 2

At a head of degree one, the kernel of an arrow map is the socle J² P_{d.snd}.