Documentation

TauCeti.RepresentationTheory.Quiver.SemisimpleQuotient

The semisimple quotient of a path algebra #

Killing the arrows of a quiver leaves its vertices. This file makes that precise at the level of algebras: reading off the coordinates of an element of pathAlgebra k Q on the trivial paths is an algebra homomorphism TauCeti.PathAlgebra.trivialCoeff onto the product algebra Q → k, and its kernel is exactly the arrow ideal. So the arrow ideal is the kernel of a map onto a product of copies of the base semiring. Over a commutative ring this induces the equivalence

pathAlgebra k Q ⧸ arrowIdeal k Q ≃ₐ[k] (Q → k).

Multiplicativity is the one point that needs an argument, and it is the length filtration again: concatenation adds lengths, so a product of paths is trivial only when both factors are, and the coordinate of f * g on the trivial path at v is the product of the coordinates of f and of g there.

For a finite acyclic quiver over a field the arrow ideal is the Jacobson radical (TauCeti.jacobson_pathAlgebra_eq_arrowIdeal), so the displayed equivalence becomes

pathAlgebra k Q ⧸ Ring.jacobson (pathAlgebra k Q) ≃ₐ[k] (Q → k),

which is the Wedderburn decomposition of the semisimple quotient: one block for each vertex, and every block is the base field itself. In particular the semisimple quotient is commutative and reduced -- the path algebra of a finite acyclic quiver is a basic algebra, with every matrix block of size one -- and its dimension is the number of vertices.

Main definitions #

Main results #

Implementation notes #

The trivial-coefficient homomorphism and its characteristic formulas are defined in TauCeti.RepresentationTheory.Quiver.PathAlgebra.TrivialCoeff; this file identifies its kernel and constructs the induced quotient equivalences. The map needs no acyclicity and no field: it is stated for a commutative base semiring and a quiver with finitely many vertices, which may have infinitely many paths. Acyclicity enters only to identify the arrow ideal with the Jacobson radical, which is imported.

References #

The kernel of the trivial-coefficient homomorphism #

source
theorem TauCeti.PathAlgebra.ker_trivialCoeff (k : Type w) (Q : Type u) [CommSemiring k] [Quiver Q] [Finite Q] :
RingHom.ker (trivialCoeff k Q) = arrowIdeal k Q

The kernel of the trivial-coefficient homomorphism is the arrow ideal: an element has all its trivial coordinates zero exactly when it is supported on the paths of positive length.

The quotient by the arrow ideal #

source
noncomputable def TauCeti.PathAlgebra.quotientArrowIdealAlgEquiv (k : Type w) (Q : Type u) [CommRing k] [Quiver Q] [Finite Q] :
(pathAlgebra k Q ⧸ arrowIdeal k Q) ≃ₐ[k] Q → k

Killing the arrows leaves the vertices: the quotient of the path algebra by the arrow ideal is the product of one copy of the base ring for each vertex.

Equations
Instances For
    source
    @[simp]
    theorem TauCeti.PathAlgebra.quotientArrowIdealAlgEquiv_mk (k : Type w) (Q : Type u) [CommRing k] [Quiver Q] [Finite Q] (f : pathAlgebra k Q) :
    (quotientArrowIdealAlgEquiv k Q) ((Ideal.Quotient.mk (arrowIdeal k Q)) f) = (trivialCoeff k Q) f

    The equivalence out of the quotient by the arrow ideal is the trivial-coefficient homomorphism.

    Trivial coefficients modulo relations #

    source
    noncomputable def TauCeti.PathAlgebra.quotientTrivialCoeff {k : Type w} {Q : Type u} [CommRing k] [Quiver Q] [Finite Q] {I : Ideal (pathAlgebra k Q)} [I.IsTwoSided] (hI : I ≤ arrowIdeal k Q) :
    pathAlgebra k Q ⧸ I →ₐ[k] Q → k

    The trivial-coefficient map descends through any ideal of relations contained in the arrow ideal.

    Equations
    Instances For
      source
      @[simp]
      theorem TauCeti.PathAlgebra.quotientTrivialCoeff_mk {k : Type w} {Q : Type u} [CommRing k] [Quiver Q] [Finite Q] {I : Ideal (pathAlgebra k Q)} [I.IsTwoSided] (hI : I ≤ arrowIdeal k Q) (a : pathAlgebra k Q) :
      (quotientTrivialCoeff hI) ((Ideal.Quotient.mk I) a) = (trivialCoeff k Q) a

      Trivial coefficients are unchanged by passage to the quotient by relations.

      source
      theorem TauCeti.PathAlgebra.quotientTrivialCoeff_surjective {k : Type w} {Q : Type u} [CommRing k] [Quiver Q] [Finite Q] {I : Ideal (pathAlgebra k Q)} [I.IsTwoSided] (hI : I ≤ arrowIdeal k Q) :
      Function.Surjective ⇑(quotientTrivialCoeff hI)

      Every family of vertex coordinates occurs in the quotient by relations.

      source
      theorem TauCeti.PathAlgebra.ker_quotientTrivialCoeff {k : Type w} {Q : Type u} [CommRing k] [Quiver Q] [Finite Q] {I : Ideal (pathAlgebra k Q)} [I.IsTwoSided] (hI : I ≤ arrowIdeal k Q) :
      RingHom.ker (quotientTrivialCoeff hI) = Ideal.map (Ideal.Quotient.mk I) (arrowIdeal k Q)

      The kernel of the descended trivial-coefficient map is the image of the arrow ideal.

      The semisimple quotient #

      source
      noncomputable def TauCeti.PathAlgebra.quotientJacobsonAlgEquiv (k : Type w) (Q : Type u) [Field k] [Quiver Q] [Finite Q] (h : Quiver.IsAcyclic Q) :
      (pathAlgebra k Q ⧸ Ring.jacobson (pathAlgebra k Q)) ≃ₐ[k] Q → k

      The semisimple quotient of the path algebra of a finite acyclic quiver is a product of copies of the base field, one for each vertex. This is its Wedderburn decomposition: every block is the base field, so every block is one-dimensional, matching the vertex simple modules.

      Equations
      Instances For
        source
        @[simp]
        theorem TauCeti.PathAlgebra.quotientJacobsonAlgEquiv_mk (k : Type w) (Q : Type u) [Field k] [Quiver Q] [Finite Q] (h : Quiver.IsAcyclic Q) (f : pathAlgebra k Q) :
        (quotientJacobsonAlgEquiv k Q h) ((Ideal.Quotient.mk (Ring.jacobson (pathAlgebra k Q))) f) = (trivialCoeff k Q) f

        The equivalence out of the semisimple quotient is the trivial-coefficient homomorphism.

        source
        theorem TauCeti.PathAlgebra.isSemisimpleRing_quotient_jacobson (k : Type w) (Q : Type u) [Field k] [Quiver Q] [Finite Q] (h : Quiver.IsAcyclic Q) :
        IsSemisimpleRing (pathAlgebra k Q ⧸ Ring.jacobson (pathAlgebra k Q))

        The semisimple quotient of the path algebra of a finite acyclic quiver is indeed semisimple: a finite product of fields is a semisimple ring.

        source
        theorem TauCeti.PathAlgebra.isReduced_quotient_jacobson (k : Type w) (Q : Type u) [Field k] [Quiver Q] [Finite Q] (h : Quiver.IsAcyclic Q) :
        IsReduced (pathAlgebra k Q ⧸ Ring.jacobson (pathAlgebra k Q))

        The semisimple quotient of the path algebra of a finite acyclic quiver is reduced: no Wedderburn block of it is a matrix algebra of size greater than one.

        source
        theorem TauCeti.PathAlgebra.isBasic (k : Type w) (Q : Type u) [Field k] [Quiver Q] [Finite Q] (h : Quiver.IsAcyclic Q) :
        IsBasic (pathAlgebra k Q)

        The path algebra of a finite acyclic quiver is a basic algebra. This is the previous two results read through TauCeti.IsBasic: by TauCeti.isBasic_iff_pi_divisionRing the quotient by the radical is then a product of division rings -- here, one copy of k for each vertex -- so the vertices index the simple modules and the indecomposable projectives without repetition.

        source
        theorem TauCeti.PathAlgebra.mul_comm_quotient_jacobson (k : Type w) (Q : Type u) [Field k] [Quiver Q] [Finite Q] (h : Quiver.IsAcyclic Q) (x y : pathAlgebra k Q ⧸ Ring.jacobson (pathAlgebra k Q)) :
        x * y = y * x

        The semisimple quotient of the path algebra of a finite acyclic quiver is commutative.

        source
        theorem TauCeti.PathAlgebra.finrank_quotient_jacobson (k : Type w) (Q : Type u) [Field k] [Quiver Q] [Finite Q] (h : Quiver.IsAcyclic Q) :
        Module.finrank k (pathAlgebra k Q ⧸ Ring.jacobson (pathAlgebra k Q)) = Nat.card Q

        The semisimple quotient of the path algebra of a finite acyclic quiver has dimension the number of vertices: one for each vertex simple module.