Documentation

TauCeti.RepresentationTheory.Quiver.PathAlgebra.Augmentation

Vertex augmentation kernels of relation quotients #

For a relation ideal contained in the arrow ideal, the trivial-path coefficients descend to an augmentation onto the product of the coefficient rings at the vertices. In the right vertex projective e_v A, the kernel of this augmentation is exactly the image of the incoming-arrow map (z_b) ↦ ∑ b z_b. This is the augmentation endpoint of vertex projective resolutions. No admissibility, acyclicity, or field hypothesis is needed.

The last-arrow decomposition reuses the homogeneous path decomposition in TauCeti.RepresentationTheory.Quiver.PathAlgebra.PathsInto. Multiplication is later-factor-first, so b z_b ends at the target of b.

References #

theorem TauCeti.PathAlgebra.quotientTrivialCoeff_eq_zero_iff_exists_eq_sum {k : Type w} {Q : Type u} [Quiver Q] [CommRing k] [Finite Q] {I : Ideal (pathAlgebra k Q)} [I.IsTwoSided] [Fintype Q] (hI : I ≤ arrowIdeal k Q) (v : Q) [(i : Q) → Fintype (i ⟶ v)] {x : pathAlgebra k Q ⧸ I} (hx : (Ideal.Quotient.mk I) (vertexIdempotent k v) * x = x) :
(quotientTrivialCoeff hI) x = 0 ↔ ∃ (z : (i : Q) → (i ⟶ v) → pathAlgebra k Q ⧸ I), (∀ (i : Q) (b : i ⟶ v), (Ideal.Quotient.mk I) (vertexIdempotent k i) * z i b = z i b) ∧ x = ∑ i : Q, ∑ b : i ⟶ v, (Ideal.Quotient.mk I) (ofArrow b) * z i b

In a vertex corner of a relation quotient, vanishing augmentation is equivalent to being a sum of incoming arrows. This identifies the augmentation kernel, independently of exactness at the earlier terms of a projective resolution.

Only the coordinate at v can be nonzero in the augmentation of e_v A.

theorem TauCeti.PathAlgebra.quotientTrivialCoeff_apply_eq_zero_iff_exists_eq_sum {k : Type w} {Q : Type u} [Quiver Q] [CommRing k] [Finite Q] {I : Ideal (pathAlgebra k Q)} [I.IsTwoSided] [Fintype Q] (hI : I ≤ arrowIdeal k Q) (v : Q) [(i : Q) → Fintype (i ⟶ v)] {x : pathAlgebra k Q ⧸ I} (hx : (Ideal.Quotient.mk I) (vertexIdempotent k v) * x = x) :
(quotientTrivialCoeff hI) x v = 0 ↔ ∃ (z : (i : Q) → (i ⟶ v) → pathAlgebra k Q ⧸ I), (∀ (i : Q) (b : i ⟶ v), (Ideal.Quotient.mk I) (vertexIdempotent k i) * z i b = z i b) ∧ x = ∑ i : Q, ∑ b : i ⟶ v, (Ideal.Quotient.mk I) (ofArrow b) * z i b

The augmentation kernel in e_v A can be tested using its single vertex coordinate.

theorem TauCeti.PathAlgebra.exists_quotientTrivialCoeff_apply_eq {k : Type w} {Q : Type u} [Quiver Q] [CommRing k] [Finite Q] {I : Ideal (pathAlgebra k Q)} [I.IsTwoSided] (hI : I ≤ arrowIdeal k Q) (v : Q) (c : k) :
∃ (x : pathAlgebra k Q ⧸ I), (Ideal.Quotient.mk I) (vertexIdempotent k v) * x = x ∧ (quotientTrivialCoeff hI) x v = c

Every scalar is the vertex coefficient of an element of the right vertex projective of a relation quotient whose ideal lies in the arrow ideal.