The augmentation endpoint of the signless preprojective Koszul complex

The signless relation ideal lies in the square of the arrow ideal, so over a nontrivial ring the vertex idempotents and the arrows survive in the signless preprojective algebra. The signless preprojective algebra augments onto the product of the coefficient rings at its vertices. In the right vertex projective e_v Π, the kernel of the vertex coefficient is exactly the image of the incoming-arrow map (z_b) ↦ ∑ b z_b. Every scalar occurs as a vertex coefficient, so the cokernel of this map is one copy of the coefficient ring, not an unspecified quotient. These statements complete the augmentation endpoint of the signless Koszul complex. They work over every commutative ring, also for non-bipartite doubled graphs and in characteristic two. The positive path-degree characterization below identifies the same arrow image in a finite quiver with reversal. Injectivity at the left endpoint still requires the non-backtracking hypothesis from the signless Koszul complex.

For a connected simple graph with at least three vertices, the signless algebra is the quadratic dual of its zigzag algebra, whereas it need not be the signed preprojective algebra on a non-bipartite graph. No signed/signless comparison is used here.

References

• S. Huerfano and M. Khovanov, A category for the adjoint representation, Section 3, for the signless quadratic dual.
• P. Etingof and C.-H. Eu, Koszulity and the Hilbert series of preprojective algebras, Sections 2 and 3, for the vertex Koszul complex.

@[instance_reducible]

noncomputable def TauCeti.fintypeHomOfFiniteStar {R : Type u} [Quiver R] [(x : R) → Fintype (Quiver.Star x)] (i j : R) : Fintype (i ⟶ j)

Choose enumerations of the finite arrow types for the augmentation sums.

theorem TauCeti.signlessPreprojectiveIdeal_le_arrowIdeal_sq (k : Type w) [CommRing k] {R : Type u} [Quiver R] [Quiver.HasReverse R] [(x : R) → Fintype (Quiver.Star x)] [Finite R] : TwoSidedIdeal.asIdeal (signlessPreprojectiveIdeal k R) ≤ arrowIdeal k R ^ 2

The signless relation ideal lies in the square of the arrow ideal, since each relator is a sum of length-two backtracks. In particular the vertex coefficients survive the quotient.

theorem TauCeti.signlessPreprojectiveIdeal_le_arrowIdeal (k : Type w) [CommRing k] {R : Type u} [Quiver R] [Quiver.HasReverse R] [(x : R) → Fintype (Quiver.Star x)] [Finite R] : TwoSidedIdeal.asIdeal (signlessPreprojectiveIdeal k R) ≤ arrowIdeal k R

The signless relation ideal lies in the arrow ideal, so vertex coefficients descend to the signless preprojective algebra.

theorem TauCeti.signlessPreprojectiveMk_vertexIdempotent_ne_zero (k : Type w) [CommRing k] {R : Type u} [Quiver R] [Quiver.HasReverse R] [(x : R) → Fintype (Quiver.Star x)] [Finite R] [Nontrivial k] (i : R) : (signlessPreprojectiveMk k R) (PathAlgebra.vertexIdempotent k i) ≠ 0

Vertex idempotents survive in the signless preprojective algebra over a nontrivial ring: the relation ideal lies in the arrow ideal, which contains no vertex idempotent.

theorem TauCeti.signlessPreprojectiveMk_ofArrow_ne_zero (k : Type w) [CommRing k] {R : Type u} [Quiver R] [Quiver.HasReverse R] [(x : R) → Fintype (Quiver.Star x)] [Finite R] [Nontrivial k] {i j : R} (b : i ⟶ j) : (signlessPreprojectiveMk k R) (PathAlgebra.ofArrow b) ≠ 0

Arrows survive in the signless preprojective algebra over a nontrivial ring: the relation ideal lies in the square of the arrow ideal, which contains no path of length one.

noncomputable def TauCeti.signlessPreprojectiveAugmentation (k : Type w) [CommRing k] {R : Type u} [Quiver R] [Quiver.HasReverse R] [(x : R) → Fintype (Quiver.Star x)] [Finite R] : signlessPreprojectiveAlgebra k R →ₐ[k] R → k

The augmentation of the signless preprojective algebra onto its vertex coefficients.

theorem TauCeti.ker_signlessPreprojectiveAugmentation (k : Type w) [CommRing k] {R : Type u} [Quiver R] [Quiver.HasReverse R] [(x : R) → Fintype (Quiver.Star x)] [Finite R] : RingHom.ker (signlessPreprojectiveAugmentation k) = Ideal.map (signlessPreprojectiveMk k R) (arrowIdeal k R)

The augmentation kernel is the image of the arrow ideal in the signless algebra.

@[simp]

theorem TauCeti.signlessPreprojectiveAugmentation_mk (k : Type w) [CommRing k] {R : Type u} [Quiver R] [Quiver.HasReverse R] [(x : R) → Fintype (Quiver.Star x)] [Finite R] (f : pathAlgebra k R) : (signlessPreprojectiveAugmentation k) ((signlessPreprojectiveMk k R) f) = (PathAlgebra.trivialCoeff k R) f

On quotient representatives, the augmentation reads the trivial-path coefficients.

theorem TauCeti.signlessPreprojectiveAugmentation_ofArrow (k : Type w) [CommRing k] {R : Type u} [Quiver R] [Quiver.HasReverse R] [(x : R) → Fintype (Quiver.Star x)] [Finite R] {i j : R} (b : i ⟶ j) : (signlessPreprojectiveAugmentation k) ((signlessPreprojectiveMk k R) (PathAlgebra.ofArrow b)) = 0

Every arrow has zero augmentation.

theorem TauCeti.signlessPreprojectiveMk_ofPath_eq_zero_of_eq_algebraMap_mul (k : Type w) [CommRing k] {R : Type u} [Quiver R] [Quiver.HasReverse R] [(x : R) → Fintype (Quiver.Star x)] [Finite R] {v : R} (p : Quiver.Path v v) (hp : 0 < p.length) {r : k} (h : (signlessPreprojectiveMk k R) (PathAlgebra.ofPath ⟨v, ⟨v, p⟩⟩) = (algebraMap k (signlessPreprojectiveAlgebra k R)) r * (signlessPreprojectiveMk k R) (PathAlgebra.vertexIdempotent k v)) : (signlessPreprojectiveMk k R) (PathAlgebra.ofPath ⟨v, ⟨v, p⟩⟩) = 0

A closed path of positive length which is a scalar multiple of its vertex idempotent vanishes, since its augmentation does.

theorem TauCeti.signlessPreprojectiveAugmentation_surjective (k : Type w) [CommRing k] {R : Type u} [Quiver R] [Quiver.HasReverse R] [(x : R) → Fintype (Quiver.Star x)] [Finite R] : Function.Surjective ⇑(signlessPreprojectiveAugmentation k)

Every family of vertex coefficients occurs in the signless preprojective algebra.

theorem TauCeti.signlessPreprojectiveAugmentation_eq_single (k : Type w) [CommRing k] {R : Type u} [Quiver R] [Quiver.HasReverse R] [(x : R) → Fintype (Quiver.Star x)] [Finite R] [DecidableEq R] (v : R) {x : signlessPreprojectiveAlgebra k R} (hx : (signlessPreprojectiveMk k R) (PathAlgebra.vertexIdempotent k v) * x = x) : (signlessPreprojectiveAugmentation k) x = Pi.single v ((signlessPreprojectiveAugmentation k) x v)

On the right vertex projective e_v Π, only the coefficient at v can be nonzero.

theorem TauCeti.signlessPreprojectiveAugmentation_apply_eq_zero_iff_exists_eq_sum (k : Type w) [CommRing k] {R : Type u} [Quiver R] [Quiver.HasReverse R] [(x : R) → Fintype (Quiver.Star x)] [Fintype R] (v : R) {x : signlessPreprojectiveAlgebra k R} (hx : (signlessPreprojectiveMk k R) (PathAlgebra.vertexIdempotent k v) * x = x) : (signlessPreprojectiveAugmentation k) x v = 0 ↔ ∃ (z : (i : R) → (i ⟶ v) → signlessPreprojectiveAlgebra k R), (∀ (i : R) (b : i ⟶ v), (signlessPreprojectiveMk k R) (PathAlgebra.vertexIdempotent k i) * z i b = z i b) ∧ x = ∑ i : R, ∑ b : i ⟶ v, (signlessPreprojectiveMk k R) (PathAlgebra.ofArrow b) * z i b

Exactness at the augmentation endpoint of the signless vertex Koszul complex: x ∈ e_v Π has vertex coefficient zero exactly when x = ∑ b z_b with z_b ∈ e_i Π. This holds without a non-backtracking choice or a bipartiteness hypothesis.

theorem TauCeti.exists_signlessPreprojectiveAugmentation_apply_eq (k : Type w) [CommRing k] {R : Type u} [Quiver R] [Quiver.HasReverse R] [(x : R) → Fintype (Quiver.Star x)] [Finite R] (v : R) (c : k) : ∃ (x : signlessPreprojectiveAlgebra k R), (signlessPreprojectiveMk k R) (PathAlgebra.vertexIdempotent k v) * x = x ∧ (signlessPreprojectiveAugmentation k) x v = c

Every scalar is the vertex coefficient of an element of the right vertex projective.

theorem TauCeti.mem_iSup_signlessPreprojectiveGrade_add_one_iff_exists_eq_sum (k : Type w) (R : Type u) [CommRing k] [Quiver R] [Quiver.HasReverse R] [Fintype R] [(x : R) → Fintype (Quiver.Star x)] (v : R) {x : signlessPreprojectiveAlgebra k R} (hx : (signlessPreprojectiveMk k R) (PathAlgebra.vertexIdempotent k v) * x = x) : x ∈ ⨆ (n : ℕ), signlessPreprojectiveGrade k R (n + 1) ↔ ∃ (z : (i : R) → (i ⟶ v) → signlessPreprojectiveAlgebra k R), (∀ (i : R) (b : i ⟶ v), (signlessPreprojectiveMk k R) (PathAlgebra.vertexIdempotent k i) * z i b = z i b) ∧ x = ∑ i : R, ∑ b : i ⟶ v, (signlessPreprojectiveMk k R) (PathAlgebra.ofArrow b) * z i b

An element of the vertex corner has positive path degree exactly when it is a sum of incoming arrows times elements of their source corners. This is exactness at the augmentation endpoint of the signless Koszul complex.