Documentation

TauCeti.RepresentationTheory.Quiver.Preprojective.PathAlgebra

The path algebra inside the preprojective algebra #

Let Q be a finite quiver. Its path algebra kQ maps to the additive preprojective algebra Π_k(Q), by including Q in the doubled quiver Quiver.Symmetrify Q and passing to the quotient. In the other direction, killing every formal reverse a* is an algebra homomorphism from the doubled path algebra onto kQ which kills both backtracks a a* and a* a of every arrow, hence the preprojective relator; so it descends to

Π_k(Q) → kQ,

and this is a retraction of the first map. Thus kQ is simultaneously a subalgebra and a quotient algebra of Π_k(Q).

The quotient statement bounds Π_k(Q) from below: if Π_k(Q) is a finite module over a nonzero commutative ring then so is kQ, and Q has no oriented cycle. Since Π_k(Q) does not depend on the orientation of Q (TauCeti.reorientPreprojectiveAlgebraEquiv), the same holds for every reorientation TauCeti.Reorient Q σ of Q. A cycle of the underlying multigraph of Q — a loop, a pair of parallel arrows, or a cycle through distinct vertices — becomes an oriented cycle after turning some of its arrows around. Consequently the preprojective algebra of a quiver whose underlying graph is not a forest is not a finite module; this includes every quiver of affine type Ã_n.

Main definitions #

Main results #

References #

The inclusion of kQ in Π_k(Q) and the quotient map killing the reverse arrows are standard; see W. Crawley-Boevey, Lectures on representations of quivers, and C. M. Ringel, The preprojective algebra of a quiver, in Algebras and Modules II, CMS Conf. Proc. 24 (1998).

source
noncomputable def TauCeti.pathAlgebraToPreprojective (k : Type w) (Q : Type u) [CommRing k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] :
pathAlgebra k Q →ₐ[k] preprojectiveAlgebra k Q

The algebra homomorphism kQ →ₐ[k] Π_k(Q) sending a path of Q to the class of the same path in the doubled quiver.

Instances For
    source
    @[simp]
    theorem TauCeti.pathAlgebraToPreprojective_ofPath (k : Type w) (Q : Type u) [CommRing k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] (x : Quiver.TotalPath Q) :
    (pathAlgebraToPreprojective k Q) (PathAlgebra.ofPath x) = (preprojectiveMk k Q) (PathAlgebra.ofPath (Quiver.Symmetrify.of.mapTotalPath x))

    The map kQ →ₐ[k] Π_k(Q) sends a path of Q to the class of the same path in the doubled quiver.

    source
    theorem TauCeti.pathAlgebraToPreprojective_ofArrow (k : Type w) (Q : Type u) [CommRing k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] {a b : Q} (f : a ⟶ b) :
    (pathAlgebraToPreprojective k Q) (PathAlgebra.ofArrow f) = (preprojectiveMk k Q) (PathAlgebra.ofArrow (Quiver.Symmetrify.of.map f))

    The map kQ →ₐ[k] Π_k(Q) sends an arrow of Q to the class of the same arrow. Deliberately not a simp lemma, TauCeti.PathAlgebra.ofArrow_eq_ofPath already rewriting its left-hand side.

    source
    noncomputable def TauCeti.preprojectiveToPathAlgebra (k : Type w) (Q : Type u) [CommRing k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] :
    preprojectiveAlgebra k Q →ₐ[k] pathAlgebra k Q

    The algebra homomorphism Π_k(Q) →ₐ[k] kQ which fixes the vertex idempotents and the arrows of Q and kills every formal reverse. It is the descent of TauCeti.PathAlgebra.symmetrifyRetraction to the preprojective algebra.

    Instances For
      source
      @[simp]
      theorem TauCeti.preprojectiveToPathAlgebra_preprojectiveMk (k : Type w) (Q : Type u) [CommRing k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] (x : pathAlgebra k (Quiver.Symmetrify Q)) :
      (preprojectiveToPathAlgebra k Q) ((preprojectiveMk k Q) x) = (PathAlgebra.symmetrifyRetraction k) x

      On the class of a doubled path, the retraction Π_k(Q) →ₐ[k] kQ is TauCeti.PathAlgebra.symmetrifyRetraction.

      source
      @[simp]
      theorem TauCeti.preprojectiveToPathAlgebra_comp_pathAlgebraToPreprojective (k : Type w) (Q : Type u) [CommRing k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] :
      (preprojectiveToPathAlgebra k Q).comp (pathAlgebraToPreprojective k Q) = AlgHom.id k (pathAlgebra k Q)

      kQ is a retract of Π_k(Q): the map killing the formal reverses is a left inverse of the map kQ →ₐ[k] Π_k(Q).

      source
      @[simp]
      theorem TauCeti.preprojectiveToPathAlgebra_pathAlgebraToPreprojective (k : Type w) (Q : Type u) [CommRing k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] (x : pathAlgebra k Q) :
      (preprojectiveToPathAlgebra k Q) ((pathAlgebraToPreprojective k Q) x) = x

      The retraction Π_k(Q) →ₐ[k] kQ undoes the map kQ →ₐ[k] Π_k(Q).

      source
      theorem TauCeti.pathAlgebraToPreprojective_injective (k : Type w) (Q : Type u) [CommRing k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] :
      Function.Injective ⇑(pathAlgebraToPreprojective k Q)

      The path algebra kQ embeds in the preprojective algebra Π_k(Q).

      source
      theorem TauCeti.preprojectiveToPathAlgebra_surjective (k : Type w) (Q : Type u) [CommRing k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] :
      Function.Surjective ⇑(preprojectiveToPathAlgebra k Q)

      The path algebra kQ is a quotient of the preprojective algebra Π_k(Q).

      Finite preprojective algebras come from forests #

      source
      theorem TauCeti.isAcyclic_of_module_finite_preprojectiveAlgebra (k : Type w) {Q : Type u} [CommRing k] [Nontrivial k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] :
      Module.Finite k (preprojectiveAlgebra k Q) → Quiver.IsAcyclic Q

      A quiver whose preprojective algebra is a finite module has no oriented cycle.

      source
      theorem TauCeti.isAcyclic_reorient_of_module_finite_preprojectiveAlgebra (k : Type w) {Q : Type u} [CommRing k] [Nontrivial k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] :
      Module.Finite k (preprojectiveAlgebra k Q) → ∀ (σ : ⦃i j : Q⦄ → (i ⟶ j) → Bool), Quiver.IsAcyclic (Reorient Q σ)

      A quiver whose preprojective algebra is a finite module has a forest as underlying multigraph: no reorientation of it has an oriented cycle. In particular it has no loop, no two arrows joining the same pair of vertices, and no cycle through distinct vertices.

      source
      theorem TauCeti.not_module_finite_preprojectiveAlgebra_of_length_pos (k : Type w) {Q : Type u} [CommRing k] [Nontrivial k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] (σ : ⦃i j : Q⦄ → (i ⟶ j) → Bool) {a : Reorient Q σ} (p : Quiver.Path a a) (hp : 0 < p.length) :
      ¬Module.Finite k (preprojectiveAlgebra k Q)

      The preprojective algebra of a quiver with a cycle is not a finite module: if some reorientation of Q has an oriented cycle of positive length, then Π_k(Q) is not a finite k-module. Taking σ to turn no arrow around covers an oriented cycle of Q itself.