The graded homomorphism spaces of the zigzag vertex projectives

For a finite simple graph without isolated vertices, TauCeti.zigzagProjective is the indecomposable left projective P_i = Z e_i of the zigzag relation quotient and TauCeti.zigzagCorner is the corner e_i Z e_j. This file supplies the dictionary those two files leave open, namely

Hom_Z(P_i, P_j) ≅ e_i Z e_j,

together with its refinement by the path-length grading. The grading is extended by zero from ℕ to ℤ, and the internal shift is M{d}_p = M_{p-d}, so [M{1}] = q[M]. Thus the degree-zero homomorphisms P_i → P_j{d} are the degree-(-d) part of the corner. Equivalently, the homomorphisms which raise degree by n : ℕ are Hom(P_i{n}, P_j).

Combining the two identifications with the entrywise computation of the graded corners in TauCeti.RepresentationTheory.Quiver.Zigzag.CartanMatrix turns the graded Cartan matrix into a matrix of graded dimensions of homomorphism spaces,

C_G(q)_{i,j} = ∑_d dim_k Hom(P_i{d}, P_j) q^d = (1 + q²) δ_{i,j} + q A_{i,j}.

Moving the internal shift from source to target reverses its sign: intrinsically degree-d maps are Hom(P_i{d}, P_j), equivalently Hom(P_i, P_j{-d}), not Hom(P_i, P_j{d}).

Main definitions

• TauCeti.zigzagProjectiveHomEquivCorner: the dictionary Hom_Z(P_i, P_j) ≃ₗ[k] e_i Z e_j.
• TauCeti.zigzagProjectiveShiftGrade: the grading of the shifted projective P_i{d}.
• TauCeti.zigzagProjectiveTargetShiftHom: the degree-zero homomorphisms Hom(P_i, P_j{d}), for every d : ℤ.
• TauCeti.zigzagProjectiveHomOfDegree: the homomorphisms P_i → P_j raising path degree by d, that is Hom(P_i{d}, P_j).

Main results

• TauCeti.zigzagProjectiveHomOfDegreeEquivGradedCorner: the graded dictionary Hom(P_i{d}, P_j) ≃ₗ[k] (e_i Z e_j)_d.
• TauCeti.zigzagProjectiveTargetShiftHomEquivIntegerGradedCorner: the signed target-shift dictionary Hom(P_i, P_j{d}) ≃ₗ[k] (e_i Z e_j)_{-d} for every d : ℤ.
• TauCeti.zigzagProjectiveHomOfDegree_eq_bot_of_three_le: no homomorphism raises degree by three or more, so the graded homomorphism spaces are concentrated in degrees 0, 1 and 2.
• TauCeti.id_mem_zigzagProjectiveHomOfDegree_zero and TauCeti.zigzagProjectiveHomEquivCorner_symm_apply_mem: the identity has degree zero, and right multiplication by a homogeneous element of the corner has that element's degree.
• TauCeti.finrank_zigzagProjectiveHomOfDegree_zero_self, TauCeti.finrank_zigzagProjectiveHomOfDegree_one_of_adj and TauCeti.finrank_zigzagProjectiveHomOfDegree_two_self_of_adj: the three one-dimensional homogeneous homomorphism spaces — the identity of P_i, the map along an edge, and the map through the volume class — with the vanishing of all the others.
• TauCeti.zigzagGradedCartanMatrix_eq_sum_finrank_zigzagProjectiveHomOfDegree: the graded Cartan entry is the graded dimension of the homomorphism spaces, ∑_d dim Hom(P_i{d}, P_j) qᵈ.

Implementation notes

Both source- and target-shifted Hom spaces are defined by intrinsic homogeneity conditions, quantified over every homogeneous element of P_i, rather than as preimages of graded corners. The comparison with evaluation at the generator is then proved. The shifted projectives retain the same underlying module and change only their family of homogeneous submodules, so these Hom spaces are k-submodules of the ungraded homomorphism space.

References

Moving a shift from the target to the source reverses its sign: the nonnegative degree-raising part formalized here is Hom(P_i{d},P_j) = Hom(P_i,P_j{-d}). See Huerfano--Khovanov, A category for the adjoint representation, Section 3, and Ehrig--Tubbenhauer, Algebraic properties of zigzag algebras, Section 2.

The ungraded dictionary

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

The homomorphisms Z e_i → Z e_j are the corner e_i Z e_j, by evaluation at the generator e_i. This is the dictionary through which the corners computed by TauCeti.RepresentationTheory.Quiver.Zigzag.CartanMatrix are homomorphism spaces of the vertex projectives.

@[simp]

theorem TauCeti.coe_zigzagProjectiveHomEquivCorner_apply (k : Type w) [Field k] {V : Type u} (G : SimpleGraph V) [Finite V] {i j : V} (φ : ↥(zigzagProjective k G i) →ₗ[nonisolatedZigzagQuotient k G] ↥(zigzagProjective k G j)) : ↑((zigzagProjectiveHomEquivCorner k G i j) φ) = ↑(φ (zigzagProjectiveGenerator k G i))

@[simp]

theorem TauCeti.coe_zigzagProjectiveHomEquivCorner_symm_apply (k : Type w) [Field k] {V : Type u} (G : SimpleGraph V) [Finite V] {i j : V} (x : ↥(zigzagCorner k G i j)) (y : ↥(zigzagProjective k G i)) : ↑(((zigzagProjectiveHomEquivCorner k G i j).symm x) y) = ↑y * ↑x

theorem TauCeti.coe_zigzagProjectiveHom_apply (k : Type w) [Field k] {V : Type u} (G : SimpleGraph V) [Finite V] {i j : V} (φ : ↥(zigzagProjective k G i) →ₗ[nonisolatedZigzagQuotient k G] ↥(zigzagProjective k G j)) (x : ↥(zigzagProjective k G i)) : ↑(φ x) = ↑x * ↑(φ (zigzagProjectiveGenerator k G i))

A homomorphism Z e_i → Z e_j is right multiplication by its value at the generator.

The graded dictionary

noncomputable def TauCeti.zigzagIntegerGradedCorner (k : Type w) [Field k] {V : Type u} (G : SimpleGraph V) [Finite V] (i j : V) (d : ℤ) : Submodule k (nonisolatedZigzagQuotient k G)

The signed degree-d part of the corner e_i Z e_j.

@[simp]

theorem TauCeti.mem_zigzagIntegerGradedCorner_iff (k : Type w) [Field k] {V : Type u} (G : SimpleGraph V) [Finite V] {i j : V} {d : ℤ} {x : nonisolatedZigzagQuotient k G} : x ∈ zigzagIntegerGradedCorner k G i j d ↔ x ∈ zigzagCorner k G i j ∧ x ∈ zigzagIntegerGrade k G d

@[simp]

theorem TauCeti.zigzagIntegerGradedCorner_ofNat (k : Type w) [Field k] {V : Type u} (G : SimpleGraph V) [Finite V] (i j : V) (d : ℕ) : zigzagIntegerGradedCorner k G i j ↑d = zigzagGradedCorner k G i j d

theorem TauCeti.zigzagIntegerGradedCorner_eq_bot_of_neg (k : Type w) [Field k] {V : Type u} (G : SimpleGraph V) [Finite V] (i j : V) {d : ℤ} (hd : d < 0) : zigzagIntegerGradedCorner k G i j d = ⊥

Signed corners vanish in negative degrees.

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

The graded homomorphism space Hom(P_i, P_j{d}): the Z-linear maps which are degree zero from the grading of P_i to the shifted grading of P_j{d}. The shift parameter is an arbitrary integer, as required by the internal grading-shift action.

theorem TauCeti.mem_zigzagProjectiveTargetShiftHom_iff_isHomogeneous (k : Type w) [Field k] {V : Type u} (G : SimpleGraph V) [Finite V] {i j : V} {d : ℤ} {φ : ↥(zigzagProjective k G i) →ₗ[nonisolatedZigzagQuotient k G] ↥(zigzagProjective k G j)} : φ ∈ zigzagProjectiveTargetShiftHom k G i j d ↔ LinearMap.IsHomogeneous φ (zigzagProjectiveGrade k G i) (zigzagProjectiveGrade k G j) (-d)

A map P_i → P_j{d} is degree zero precisely when its underlying map has signed degree -d.

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

The homomorphisms P_i{d} → P_j: those Z-linear maps Z e_i → Z e_j which send a homogeneous element of degree n to a homogeneous element of degree n + d.

@[simp]

theorem TauCeti.mem_zigzagProjectiveHomOfDegree_iff (k : Type w) [Field k] {V : Type u} (G : SimpleGraph V) [Finite V] {i j : V} {d : ℕ} {φ : ↥(zigzagProjective k G i) →ₗ[nonisolatedZigzagQuotient k G] ↥(zigzagProjective k G j)} : φ ∈ zigzagProjectiveHomOfDegree k G i j d ↔ ↑(φ (zigzagProjectiveGenerator k G i)) ∈ zigzagGradedCorner k G i j d

A homomorphism raises degree by d exactly when its value at the generator is a degree-d element of the corner. The generator e_i has degree zero, which gives one direction, and multiplication adds degrees, which gives the other.

theorem TauCeti.isHomogeneous_zigzagProjective_iff (k : Type w) [Field k] {V : Type u} (G : SimpleGraph V) [Finite V] {i j : V} {d : ℤ} {φ : ↥(zigzagProjective k G i) →ₗ[nonisolatedZigzagQuotient k G] ↥(zigzagProjective k G j)} : LinearMap.IsHomogeneous φ (zigzagProjectiveGrade k G i) (zigzagProjectiveGrade k G j) d ↔ ↑(φ (zigzagProjectiveGenerator k G i)) ∈ zigzagIntegerGradedCorner k G i j d

A homomorphism of vertex projectives has signed degree d exactly when its value at the projective generator belongs to the signed degree-d corner.

@[simp]

theorem TauCeti.mem_zigzagProjectiveTargetShiftHom_iff (k : Type w) [Field k] {V : Type u} (G : SimpleGraph V) [Finite V] {i j : V} {d : ℤ} {φ : ↥(zigzagProjective k G i) →ₗ[nonisolatedZigzagQuotient k G] ↥(zigzagProjective k G j)} : φ ∈ zigzagProjectiveTargetShiftHom k G i j d ↔ ↑(φ (zigzagProjectiveGenerator k G i)) ∈ zigzagIntegerGradedCorner k G i j (-d)

Target-shift membership by evaluation. A map belongs to Hom(P_i, P_j{d}) exactly when its value at the generator belongs to the degree-(-d) corner.

theorem TauCeti.zigzagProjectiveHomOfDegree_eq_comap (k : Type w) [Field k] {V : Type u} (G : SimpleGraph V) [Finite V] (i j : V) (d : ℕ) : zigzagProjectiveHomOfDegree k G i j d = Submodule.comap (↑(zigzagProjectiveHomEquivCorner k G i j)) (Submodule.comap (zigzagCorner k G i j).subtype (zigzagGradedCorner k G i j d))

The degree-d homomorphisms are the preimage of the degree-d corner under the ungraded dictionary.

noncomputable def TauCeti.zigzagProjectiveHomOfDegreeEquivGradedCorner (k : Type w) [Field k] {V : Type u} (G : SimpleGraph V) [Finite V] (i j : V) (d : ℕ) : ↥(zigzagProjectiveHomOfDegree k G i j d) ≃ₗ[k] ↥(zigzagGradedCorner k G i j d)

The graded dictionary: the homomorphisms P_i{d} → P_j are the degree-d part of the corner e_i Z e_j.

@[simp]

theorem TauCeti.coe_zigzagProjectiveHomOfDegreeEquivGradedCorner_apply (k : Type w) [Field k] {V : Type u} (G : SimpleGraph V) [Finite V] {i j : V} {d : ℕ} (φ : ↥(zigzagProjectiveHomOfDegree k G i j d)) : ↑((zigzagProjectiveHomOfDegreeEquivGradedCorner k G i j d) φ) = ↑(↑φ (zigzagProjectiveGenerator k G i))

The graded dictionary sends a homogeneous map to its value at the projective generator.

@[simp]

theorem TauCeti.coe_zigzagProjectiveHomOfDegreeEquivGradedCorner_symm_apply (k : Type w) [Field k] {V : Type u} (G : SimpleGraph V) [Finite V] {i j : V} {d : ℕ} (x : ↥(zigzagGradedCorner k G i j d)) (y : ↥(zigzagProjective k G i)) : ↑(↑((zigzagProjectiveHomOfDegreeEquivGradedCorner k G i j d).symm x) y) = ↑y * ↑x

The inverse graded dictionary is right multiplication by the corresponding homogeneous corner element.

theorem TauCeti.zigzagProjectiveTargetShiftHom_eq_comap (k : Type w) [Field k] {V : Type u} (G : SimpleGraph V) [Finite V] (i j : V) (d : ℤ) : zigzagProjectiveTargetShiftHom k G i j d = Submodule.comap (↑(zigzagProjectiveHomEquivCorner k G i j)) (Submodule.comap (zigzagCorner k G i j).subtype (zigzagIntegerGradedCorner k G i j (-d)))

The target-shifted homomorphisms are the preimage of the signed degree-(-d) corner under the ungraded dictionary.

noncomputable def TauCeti.zigzagProjectiveTargetShiftHomEquivIntegerGradedCorner (k : Type w) [Field k] {V : Type u} (G : SimpleGraph V) [Finite V] (i j : V) (d : ℤ) : ↥(zigzagProjectiveTargetShiftHom k G i j d) ≃ₗ[k] ↥(zigzagIntegerGradedCorner k G i j (-d))

The signed target-shift dictionary: for every d : ℤ, the degree-zero maps Hom(P_i, P_j{d}) are the degree-(-d) part of the corner e_i Z e_j.

@[simp]

theorem TauCeti.coe_zigzagProjectiveTargetShiftHomEquivIntegerGradedCorner_apply (k : Type w) [Field k] {V : Type u} (G : SimpleGraph V) [Finite V] {i j : V} {d : ℤ} (φ : ↥(zigzagProjectiveTargetShiftHom k G i j d)) : ↑((zigzagProjectiveTargetShiftHomEquivIntegerGradedCorner k G i j d) φ) = ↑(↑φ (zigzagProjectiveGenerator k G i))

The signed target-shift dictionary sends a homogeneous map to its value at the projective generator.

@[simp]

theorem TauCeti.coe_zigzagProjectiveTargetShiftHomEquivIntegerGradedCorner_symm_apply (k : Type w) [Field k] {V : Type u} (G : SimpleGraph V) [Finite V] {i j : V} {d : ℤ} (x : ↥(zigzagIntegerGradedCorner k G i j (-d))) (y : ↥(zigzagProjective k G i)) : ↑(↑((zigzagProjectiveTargetShiftHomEquivIntegerGradedCorner k G i j d).symm x) y) = ↑y * ↑x

The inverse signed target-shift dictionary is right multiplication by the corresponding homogeneous corner element.

theorem TauCeti.zigzagProjectiveTargetShiftHom_neg_ofNat (k : Type w) [Field k] {V : Type u} (G : SimpleGraph V) [Finite V] (i j : V) (d : ℕ) : zigzagProjectiveTargetShiftHom k G i j (-↑d) = zigzagProjectiveHomOfDegree k G i j d

Moving a nonnegative source shift to the target reverses its sign.

theorem TauCeti.zigzagProjectiveTargetShiftHom_eq_bot_of_pos (k : Type w) [Field k] {V : Type u} (G : SimpleGraph V) [Finite V] (i j : V) {d : ℤ} (hd : 0 < d) : zigzagProjectiveTargetShiftHom k G i j d = ⊥

Positive target shifts carry no homogeneous maps between the nonnegatively graded vertex projectives.

theorem TauCeti.finrank_zigzagProjectiveTargetShiftHom (k : Type w) [Field k] {V : Type u} (G : SimpleGraph V) [Finite V] (i j : V) (d : ℤ) : Module.finrank k ↥(zigzagProjectiveTargetShiftHom k G i j d) = Module.finrank k ↥(zigzagIntegerGradedCorner k G i j (-d))

The dimension of a target-shifted Hom space is the dimension of the corresponding signed corner.

theorem TauCeti.finrank_zigzagProjectiveHomOfDegree (k : Type w) [Field k] {V : Type u} (G : SimpleGraph V) [Finite V] (i j : V) (d : ℕ) : Module.finrank k ↥(zigzagProjectiveHomOfDegree k G i j d) = Module.finrank k ↥(zigzagGradedCorner k G i j d)

The dimension of a homogeneous homomorphism space is the dimension of the corresponding graded corner.

theorem TauCeti.zigzagProjectiveHomEquivCorner_symm_apply_mem (k : Type w) [Field k] {V : Type u} (G : SimpleGraph V) [Finite V] {i j : V} {d : ℕ} (x : ↥(zigzagCorner k G i j)) (hx : ↑x ∈ zigzagGrade k G d) : (zigzagProjectiveHomEquivCorner k G i j).symm x ∈ zigzagProjectiveHomOfDegree k G i j d

Right multiplication by a degree-d element of the corner raises degree by d.

theorem TauCeti.id_mem_zigzagProjectiveHomOfDegree_zero (k : Type w) [Field k] {V : Type u} (G : SimpleGraph V) [Finite V] (i : V) : LinearMap.id ∈ zigzagProjectiveHomOfDegree k G i i 0

The identity of a vertex projective raises degree by zero.

The homogeneous homomorphism spaces

theorem TauCeti.zigzagProjectiveHomOfDegree_eq_bot_of_three_le (k : Type w) [Field k] {V : Type u} (G : SimpleGraph V) [Finite V] (i j : V) {d : ℕ} (hd : 3 ≤ d) : zigzagProjectiveHomOfDegree k G i j d = ⊥

No homomorphism of vertex projectives raises degree by three or more, since the zigzag quotient has nothing in those degrees.

theorem TauCeti.zigzagProjectiveTargetShiftHom_eq_bot_of_lt_neg_two (k : Type w) [Field k] {V : Type u} (G : SimpleGraph V) [Finite V] (i j : V) {d : ℤ} (hd : d < -2) : zigzagProjectiveTargetShiftHom k G i j d = ⊥

Target-shifted homomorphisms vanish below shift -2, since the zigzag algebra is concentrated in path degrees zero, one, and two.

theorem TauCeti.finrank_zigzagProjectiveHomOfDegree_zero_self (k : Type w) [Field k] {V : Type u} (G : SimpleGraph V) [Finite V] (i : V) : Module.finrank k ↥(zigzagProjectiveHomOfDegree k G i i 0) = 1

The degree-zero endomorphism space of a vertex projective is one-dimensional. It contains the identity, by TauCeti.id_mem_zigzagProjectiveHomOfDegree_zero.

theorem TauCeti.finrank_zigzagProjectiveHomOfDegree_zero_of_ne (k : Type w) [Field k] {V : Type u} (G : SimpleGraph V) [Finite V] {i j : V} (h : i ≠ j) : Module.finrank k ↥(zigzagProjectiveHomOfDegree k G i j 0) = 0

There is no nonzero degree-zero homomorphism between the vertex projectives at two distinct vertices.

theorem TauCeti.finrank_zigzagProjectiveHomOfDegree_one_of_adj (k : Type w) [Field k] {V : Type u} (G : SimpleGraph V) [Finite V] {i j : V} (h : G.Adj j i) : Module.finrank k ↥(zigzagProjectiveHomOfDegree k G i j 1) = 1

An edge gives a one-dimensional space of degree-one homomorphisms. The corner it comes from is spanned by the arrow crossing the edge (TauCeti.zigzagGradedCorner_one_eq_span_of_adj), which TauCeti.coe_zigzagProjectiveHomEquivCorner_symm_apply reads as right multiplication by that arrow.

theorem TauCeti.finrank_zigzagProjectiveHomOfDegree_one_of_not_adj (k : Type w) [Field k] {V : Type u} (G : SimpleGraph V) [Finite V] {i j : V} (h : ¬G.Adj j i) : Module.finrank k ↥(zigzagProjectiveHomOfDegree k G i j 1) = 0

Nonadjacent vertices carry no degree-one homomorphism of vertex projectives.

theorem TauCeti.finrank_zigzagProjectiveHomOfDegree_two_self_of_adj (k : Type w) [Field k] {V : Type u} (G : SimpleGraph V) [Finite V] {i j : V} (h : G.Adj i j) : Module.finrank k ↥(zigzagProjectiveHomOfDegree k G i i 2) = 1

The volume class gives a one-dimensional space of degree-two endomorphisms of a vertex projective at a vertex with a neighbour: the corner it comes from is spanned by that class, by TauCeti.zigzagGradedCorner_two_self_eq_span.

theorem TauCeti.finrank_zigzagProjectiveHomOfDegree_two_of_ne (k : Type w) [Field k] {V : Type u} (G : SimpleGraph V) [Finite V] {i j : V} (h : i ≠ j) : Module.finrank k ↥(zigzagProjectiveHomOfDegree k G i j 2) = 0

Distinct vertices carry no degree-two homomorphism of vertex projectives.

The graded Cartan matrix as a matrix of homomorphism dimensions

theorem TauCeti.zigzagGradedCartanMatrix_eq_sum_finrank_zigzagProjectiveHomOfDegree (k : Type w) [Field k] {V : Type u} (G : SimpleGraph V) [Finite V] (i j : V) : zigzagGradedCartanMatrix k G i j = ∑ n ∈ Finset.range 3, ↑(Module.finrank k ↥(zigzagProjectiveHomOfDegree k G i j n)) * Polynomial.X ^ n

The graded Cartan entry is the graded dimension of the homomorphism spaces of the vertex projectives, ∑_d dim_k Hom(P_i{d}, P_j) qᵈ. Together with TauCeti.zigzagGradedCartanMatrix_eq this is the graded Cartan formula read on the projectives themselves, and by TauCeti.zigzagProjectiveHomOfDegree_eq_bot_of_three_le the truncation of the sum below degree three discards only zeros.