Documentation

TauCeti.RepresentationTheory.Quiver.PathAlgebra.Opposite

Opposites of path algebras #

For a quiver with finitely many vertices and involutive arrow reversal, reversing every path identifies its path algebra with its opposite algebra. This file constructs that identification directly on the path basis and records its action on paths, vertices, and arrows.

This identifies left modules with right modules over the same path algebra and transports reversal-invariant relations to the opposite algebra.

Main definitions #

source
noncomputable def TauCeti.PathAlgebra.reverseOpAlgEquiv (k : Type w) (Q : Type u) [CommSemiring k] [Quiver Q] [Quiver.HasInvolutiveReverse Q] [Finite Q] :
pathAlgebra k Q ≃ₐ[k] (pathAlgebra k Q)ᵐᵒᵖ

For a quiver with finitely many vertices and involutive arrow reversal, reversing paths identifies its path algebra with its opposite algebra.

Instances For
    source
    @[simp]
    theorem TauCeti.PathAlgebra.reverseOpAlgEquiv_ofPath (k : Type w) (Q : Type u) [CommSemiring k] [Quiver Q] [Quiver.HasInvolutiveReverse Q] [Finite Q] (x : Quiver.TotalPath Q) :
    (reverseOpAlgEquiv k Q) (ofPath x) = MulOpposite.op (ofPath x.reverse)

    The path-reversal isomorphism sends a basis path to the opposite of its reverse.

    source
    @[simp]
    theorem TauCeti.PathAlgebra.reverseOpAlgEquiv_symm_op_ofPath (k : Type w) (Q : Type u) [CommSemiring k] [Quiver Q] [Quiver.HasInvolutiveReverse Q] [Finite Q] (x : Quiver.TotalPath Q) :
    (reverseOpAlgEquiv k Q).symm (MulOpposite.op (ofPath x)) = ofPath x.reverse

    The inverse path-reversal isomorphism sends the opposite of a basis path to its reverse.

    source
    @[simp]
    theorem TauCeti.PathAlgebra.reverseOpAlgEquiv_vertexIdempotent (k : Type w) (Q : Type u) [CommSemiring k] [Quiver Q] [Quiver.HasInvolutiveReverse Q] [Finite Q] (a : Q) :
    (reverseOpAlgEquiv k Q) (vertexIdempotent k a) = MulOpposite.op (vertexIdempotent k a)

    Path reversal fixes vertex idempotents, up to passage to the opposite algebra.

    source
    theorem TauCeti.PathAlgebra.reverseOpAlgEquiv_ofArrow (k : Type w) (Q : Type u) [CommSemiring k] [Quiver Q] [Quiver.HasInvolutiveReverse Q] [Finite Q] {a b : Q} (e : a ⟶ b) :
    (reverseOpAlgEquiv k Q) (ofArrow e) = MulOpposite.op (ofArrow (Quiver.reverse e))

    Path reversal sends an arrow to the opposite of its reversed arrow. This is not a simp lemma, since TauCeti.PathAlgebra.ofArrow_eq_ofPath rewrites its left-hand side.

    source
    theorem TauCeti.PathAlgebra.reverseOpAlgEquiv_mem_opGrade (k : Type w) (Q : Type u) [CommSemiring k] [Quiver Q] [Quiver.HasInvolutiveReverse Q] [Finite Q] {n : ℕ} {x : pathAlgebra k Q} (hx : x ∈ grade k Q n) :
    (reverseOpAlgEquiv k Q) x ∈ opGrade k Q n

    Reversing paths preserves path length in the opposite path algebra.

    source
    theorem TauCeti.PathAlgebra.reverseOpAlgEquiv_symm_mem_grade (k : Type w) (Q : Type u) [CommSemiring k] [Quiver Q] [Quiver.HasInvolutiveReverse Q] [Finite Q] {n : ℕ} {x : (pathAlgebra k Q)ᵐᵒᵖ} (hx : x ∈ opGrade k Q n) :
    (reverseOpAlgEquiv k Q).symm x ∈ grade k Q n

    The inverse path-reversal comparison also preserves path length.