Documentation

TauCeti.RepresentationTheory.Quiver.PathAlgebra.TrivialCoeff

The trivial-coefficient homomorphism of a path algebra #

Reading off the coordinates of an element of a path algebra on the trivial paths gives the algebra homomorphism TauCeti.PathAlgebra.trivialCoeff : pathAlgebra k Q →ₐ[k] (Q → k). Concatenation adds path lengths, so a product path is trivial exactly when both factors are trivial at the same vertex. This makes the coordinate projection multiplicative.

The map needs only a commutative base semiring and finitely many vertices. It is onto: a family of coefficients is represented by the corresponding linear combination of vertex idempotents. It kills every path of positive length and sends each vertex idempotent to the indicator of that vertex. Its kernel is the arrow ideal. Over a commutative ring it induces the equivalence TauCeti.PathAlgebra.quotientArrowIdealAlgEquiv of the quotient by the arrow ideal with Q → k, constructed in TauCeti.RepresentationTheory.Quiver.SemisimpleQuotient.

Main definitions and results #

References #

Assem--Simson--Skowroński, Elements of the Representation Theory of Associative Algebras I, Ch. II and III.

The trivial-coefficient homomorphism #

source
noncomputable def TauCeti.PathAlgebra.trivialCoeff (k : Type w) (Q : Type u) [CommSemiring k] [Quiver Q] [Finite Q] :
pathAlgebra k Q →ₐ[k] Q → k

The trivial-coefficient homomorphism of a path algebra: an element is sent to the family of its coordinates on the trivial paths, one for each vertex. Concatenation adds lengths, so this is multiplicative. It is surjective with kernel the arrow ideal. Over a commutative ring it induces TauCeti.PathAlgebra.quotientArrowIdealAlgEquiv, the equivalence of the quotient by the arrow ideal with Q → k constructed in TauCeti.RepresentationTheory.Quiver.SemisimpleQuotient.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem TauCeti.PathAlgebra.trivialCoeff_apply {k : Type w} {Q : Type u} [CommSemiring k] [Quiver Q] [Finite Q] (f : pathAlgebra k Q) (v : Q) :
    (trivialCoeff k Q) f v = ((pathAlgebraBasis k Q).repr f) ⟨v, ⟨v, Quiver.Path.nil⟩⟩

    The trivial-coefficient homomorphism reads off a coordinate for the path basis.

    source
    @[simp]
    theorem TauCeti.PathAlgebra.trivialCoeff_ofPath_of_length_pos {k : Type w} {Q : Type u} [CommSemiring k] [Quiver Q] [Finite Q] {x : Quiver.TotalPath Q} (hx : 0 < x.snd.snd.length) :
    (trivialCoeff k Q) (ofPath x) = 0

    A basis path of positive length has all its trivial coordinates zero.

    source
    theorem TauCeti.PathAlgebra.trivialCoeff_ofArrow {k : Type w} {Q : Type u} [CommSemiring k] [Quiver Q] [Finite Q] {a b : Q} (e : a ⟶ b) :
    (trivialCoeff k Q) (ofArrow e) = 0

    An arrow has all its trivial coordinates zero: the arrows are what the trivial-coefficient homomorphism kills. Deliberately not a simp lemma, TauCeti.PathAlgebra.ofArrow_eq_ofPath already rewriting its left-hand side.

    source
    @[simp]
    theorem TauCeti.PathAlgebra.trivialCoeff_vertexIdempotent {k : Type w} {Q : Type u} [CommSemiring k] [Quiver Q] [Finite Q] [DecidableEq Q] (v : Q) :
    (trivialCoeff k Q) (vertexIdempotent k v) = Pi.single v 1

    The vertex idempotent at v is sent to the indicator of v.

    source
    theorem TauCeti.PathAlgebra.trivialCoeff_surjective (k : Type w) (Q : Type u) [CommSemiring k] [Quiver Q] [Finite Q] :
    Function.Surjective ⇑(trivialCoeff k Q)

    Every family of scalars is the family of trivial coordinates of an element: the trivial-coefficient homomorphism is onto, a preimage of c being ∑ᵥ c v • eᵥ.