Documentation

TauCeti.RepresentationTheory.Quiver.Kronecker.UpperTriangular

The path algebra of the A₂ quiver #

The A₂ quiver • → • is the generalized Kronecker quiver on a one-element arrow type. Its path algebra has the two trivial paths and the single arrow as a basis, and this file identifies it with the algebra of upper-triangular 2 × 2 matrices over a commutative semiring. This algebra has finite rank three when the base satisfies the strong rank condition.

The identification sends a path from a to b to the matrix unit E_{b,a}, in the row of its target and the column of its source: with the later factor first convention of TauCeti.pathAlgebra, an arrow acts on a left module by carrying the component at its source to the component at its target, so it is the target that indexes the row. The single arrow runs from src to tgt, so the matrices are upper triangular exactly when tgt is indexed before src; that is the ordering TauCeti.Quiver.Kronecker.vertexEquiv fixes.

Main definitions #

Main results #

References #

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

Collapsing the paths onto the matrix units #

The identification with the upper-triangular matrices #

source
noncomputable def TauCeti.Quiver.Kronecker.upperTriangularAlgEquiv {A : Type v} [Unique A] (k : Type w) [CommSemiring k] :
pathAlgebra k (Kronecker A) ≃ₐ[k] ↥(Matrix.blockTriangularSubalgebra k k id)

The path algebra of the A₂ quiver is the algebra of upper-triangular 2 × 2 matrices. A path goes to the matrix unit in the row of its target and the column of its source, so the two vertex idempotents go to the two diagonal matrix units and the arrow to the entry above the diagonal.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem TauCeti.Quiver.Kronecker.upperTriangularAlgEquiv_single {A : Type v} [Unique A] (k : Type w) [CommSemiring k] (x : TotalPath (Kronecker A)) (c : k) :
    ↑((upperTriangularAlgEquiv k) (PathAlgebra.single x c)) = Matrix.single (vertexEquiv x.snd.fst) (vertexEquiv x.fst) c

    The identification sends a path to the matrix unit in the row of its target and the column of its source.

    source
    @[simp]
    theorem TauCeti.Quiver.Kronecker.upperTriangularAlgEquiv_symm_apply {A : Type v} [Unique A] (k : Type w) [CommSemiring k] (M : ↥(Matrix.blockTriangularSubalgebra k k id)) :
    (upperTriangularAlgEquiv k).symm M = PathAlgebra.single ⟨tgt, ⟨tgt, Quiver.Path.nil⟩⟩ (↑M 0 0) + PathAlgebra.single ⟨src, ⟨tgt, arrowPath default⟩⟩ (↑M 0 1) + PathAlgebra.single ⟨src, ⟨src, Quiver.Path.nil⟩⟩ (↑M 1 1)

    The inverse identification reads an upper-triangular matrix off as a combination of the three paths: the two diagonal entries carry the trivial paths, and the entry above the diagonal carries the arrow. The entry below the diagonal, which vanishes, is reached by no path.

    source
    @[simp]
    theorem TauCeti.Quiver.Kronecker.upperTriangularAlgEquiv_vertexIdempotent_tgt {A : Type v} [Unique A] (k : Type w) [CommSemiring k] :
    ↑((upperTriangularAlgEquiv k) (PathAlgebra.vertexIdempotent k tgt)) = Matrix.single 0 0 1

    The vertex idempotent at the target goes to the first diagonal matrix unit.

    source
    @[simp]
    theorem TauCeti.Quiver.Kronecker.upperTriangularAlgEquiv_vertexIdempotent_src {A : Type v} [Unique A] (k : Type w) [CommSemiring k] :
    ↑((upperTriangularAlgEquiv k) (PathAlgebra.vertexIdempotent k src)) = Matrix.single 1 1 1

    The vertex idempotent at the source goes to the second diagonal matrix unit.

    source
    theorem TauCeti.Quiver.Kronecker.upperTriangularAlgEquiv_ofArrow {A : Type v} [Unique A] (k : Type w) [CommSemiring k] (a : A) :
    ↑((upperTriangularAlgEquiv k) (PathAlgebra.ofArrow (arrow a))) = Matrix.single 0 1 1

    The arrow goes to the matrix unit above the diagonal: it is the arrow that makes the algebra triangular rather than diagonal.

    This is not @[simp]: its left-hand side is not in simp-normal form, since ofArrow_eq_ofPath and toPath_arrow rewrite an arrow to the length-one path it traces.

    The dimension #

    source
    theorem TauCeti.Quiver.Kronecker.finrank_blockTriangularSubalgebra_eq_three (k : Type w) [CommSemiring k] [StrongRankCondition k] :
    Module.finrank k ↥(Matrix.blockTriangularSubalgebra k k id) = 3

    The algebra of upper-triangular 2 × 2 matrices has finite rank three over a commutative semiring satisfying the strong rank condition.