The opposite of a preprojective algebra

Reversing every path of the doubled quiver preserves each of the two backtracks attached to an original arrow. It therefore preserves every gauged preprojective relator ρ_ε, whatever the labelling ε, and descends to an isomorphism from the gauged preprojective algebra to its opposite. Specializing to the constant labelling 1 gives the same isomorphism for the additive preprojective algebra. On a path class the isomorphism takes the class of the path to the opposite of the class of its reverse. The same palindromy fixes the signless local relator of any quiver with an involutive reversal, since each of its summands is a backtrack.

Main results

• TauCeti.reverseOpAlgEquiv_gaugedPreprojectiveRelator: path reversal preserves every gauged preprojective relator, up to passage to the opposite algebra.
• TauCeti.reverseOpAlgEquiv_preprojectiveRelator and TauCeti.reverseOpAlgEquiv_localPreprojectiveRelator: the same statement for the preprojective relator and for each local relator.
• TauCeti.gaugedPreprojectiveOpAlgEquiv: every gauged preprojective algebra is isomorphic to its opposite.
• TauCeti.preprojectiveOpAlgEquiv: the preprojective algebra is isomorphic to its opposite.
• TauCeti.reverseOpAlgEquiv_signlessPreprojectiveRelator: path reversal preserves every signless local relator, up to passage to the opposite algebra.

References

The preprojective presentation and its signs follow Crawley-Boevey, Quiver algebras, weighted projective lines, and the Deligne--Simpson problem, Section 1.

@[simp]

theorem TauCeti.reverseOpAlgEquiv_headBacktrackElem (k : Type w) {Q : Type u} [CommSemiring k] [Quiver Q] [Finite Q] {i j : Q} (a : i ⟶ j) : (PathAlgebra.reverseOpAlgEquiv k (Quiver.Symmetrify Q)) (headBacktrackElem k a) = MulOpposite.op (headBacktrackElem k a)

Reversal fixes the head backtrack of an original arrow, up to passage to the opposite path algebra.

@[simp]

theorem TauCeti.reverseOpAlgEquiv_tailBacktrackElem (k : Type w) {Q : Type u} [CommSemiring k] [Quiver Q] [Finite Q] {i j : Q} (a : i ⟶ j) : (PathAlgebra.reverseOpAlgEquiv k (Quiver.Symmetrify Q)) (tailBacktrackElem k a) = MulOpposite.op (tailBacktrackElem k a)

Reversal fixes the tail backtrack of an original arrow, up to passage to the opposite path algebra.

@[simp]

theorem TauCeti.reverseOpAlgEquiv_doubledVertexIdempotent (k : Type w) {Q : Type u} [CommSemiring k] [Quiver Q] [Finite Q] (i : Q) : (PathAlgebra.reverseOpAlgEquiv k (Quiver.Symmetrify Q)) (doubledVertexIdempotent k i) = MulOpposite.op (doubledVertexIdempotent k i)

Reversal fixes the vertex idempotent of the doubled quiver, up to passage to the opposite path algebra.

@[simp]

theorem TauCeti.reverseOpAlgEquiv_gaugedPreprojectiveRelator (k : Type w) {Q : Type u} [CommRing k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] (ε : ⦃i j : Q⦄ → (i ⟶ j) → k) : (PathAlgebra.reverseOpAlgEquiv k (Quiver.Symmetrify Q)) (gaugedPreprojectiveRelator k ε) = MulOpposite.op (gaugedPreprojectiveRelator k ε)

Path reversal preserves every gauged preprojective relator, up to passage to the opposite path algebra. Both backtracks of every arrow are palindromic, so each signed difference is fixed however its coefficient is chosen.

@[simp]

theorem TauCeti.reverseOpAlgEquiv_preprojectiveRelator (k : Type w) (Q : Type u) [CommRing k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] : (PathAlgebra.reverseOpAlgEquiv k (Quiver.Symmetrify Q)) (preprojectiveRelator k Q) = MulOpposite.op (preprojectiveRelator k Q)

Path reversal preserves the preprojective relator, up to passage to the opposite path algebra. This is the constant labelling 1 of the gauged statement.

@[simp]

theorem TauCeti.reverseOpAlgEquiv_localPreprojectiveRelator (k : Type w) (Q : Type u) [CommRing k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] (v : Q) : (PathAlgebra.reverseOpAlgEquiv k (Quiver.Symmetrify Q)) (localPreprojectiveRelator k v) = MulOpposite.op (localPreprojectiveRelator k v)

Path reversal preserves each local preprojective relator, up to passage to the opposite path algebra.

@[simp]

theorem TauCeti.reverseOpAlgEquiv_signlessPreprojectiveRelator (k : Type w) {R : Type u} [CommSemiring k] [Quiver R] [Quiver.HasInvolutiveReverse R] [Finite R] (v : R) [Fintype (Quiver.Star v)] : (PathAlgebra.reverseOpAlgEquiv k R) (signlessPreprojectiveRelator k v) = MulOpposite.op (signlessPreprojectiveRelator k v)

Path reversal preserves every signless local relator, up to passage to the opposite path algebra. Each summand traverses an arrow and returns along its reverse, so it is a palindrome.

noncomputable def TauCeti.gaugedPreprojectiveOpAlgEquiv (k : Type w) {Q : Type u} [CommRing k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] (ε : ⦃i j : Q⦄ → (i ⟶ j) → k) : gaugedPreprojectiveAlgebra k ε ≃ₐ[k] (gaugedPreprojectiveAlgebra k ε)ᵐᵒᵖ

A gauged preprojective algebra is isomorphic to its opposite algebra. The isomorphism is induced by reversing every path of the doubled quiver, which fixes both backtracks of every arrow and hence the gauged relator, whatever the labelling.

@[simp]

theorem TauCeti.gaugedPreprojectiveOpAlgEquiv_gaugedPreprojectiveMk (k : Type w) {Q : Type u} [CommRing k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] (ε : ⦃i j : Q⦄ → (i ⟶ j) → k) (x : pathAlgebra k (Quiver.Symmetrify Q)) : (gaugedPreprojectiveOpAlgEquiv k ε) ((gaugedPreprojectiveMk k ε) x) = (AlgHom.op (gaugedPreprojectiveMk k ε)) ((PathAlgebra.reverseOpAlgEquiv k (Quiver.Symmetrify Q)) x)

On an arbitrary path-algebra representative, the gauged opposite-algebra isomorphism reverses the representative before applying the opposite of the quotient map.

@[simp]

theorem TauCeti.gaugedPreprojectiveOpAlgEquiv_symm_op_gaugedPreprojectiveMk (k : Type w) {Q : Type u} [CommRing k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] (ε : ⦃i j : Q⦄ → (i ⟶ j) → k) (x : pathAlgebra k (Quiver.Symmetrify Q)) : (gaugedPreprojectiveOpAlgEquiv k ε).symm (MulOpposite.op ((gaugedPreprojectiveMk k ε) x)) = (gaugedPreprojectiveMk k ε) (MulOpposite.unop ((PathAlgebra.reverseOpAlgEquiv k (Quiver.Symmetrify Q)) x))

On the opposite of an arbitrary path-algebra representative, the inverse gauged opposite-algebra isomorphism reverses the representative before applying the quotient map.

noncomputable def TauCeti.preprojectiveOpAlgEquiv (k : Type w) (Q : Type u) [CommRing k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] : preprojectiveAlgebra k Q ≃ₐ[k] (preprojectiveAlgebra k Q)ᵐᵒᵖ

The additive preprojective algebra is isomorphic to its opposite algebra. The isomorphism is induced by reversing every path of the doubled quiver; it is the constant labelling 1 of TauCeti.gaugedPreprojectiveOpAlgEquiv, transported along the identification of the two presentations.

@[simp]

theorem TauCeti.preprojectiveOpAlgEquiv_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)) : (preprojectiveOpAlgEquiv k Q) ((preprojectiveMk k Q) x) = (AlgHom.op (preprojectiveMk k Q)) ((PathAlgebra.reverseOpAlgEquiv k (Quiver.Symmetrify Q)) x)

On an arbitrary path-algebra representative, the opposite-algebra isomorphism reverses the representative before applying the opposite of the quotient map.

@[simp]

theorem TauCeti.preprojectiveOpAlgEquiv_symm_op_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)) : (preprojectiveOpAlgEquiv k Q).symm (MulOpposite.op ((preprojectiveMk k Q) x)) = (preprojectiveMk k Q) (MulOpposite.unop ((PathAlgebra.reverseOpAlgEquiv k (Quiver.Symmetrify Q)) x))

On the opposite of an arbitrary path-algebra representative, the inverse opposite-algebra isomorphism reverses the representative before applying the quotient map.

theorem TauCeti.preprojectiveOpAlgEquiv_preprojectiveMk_ofPath (k : Type w) (Q : Type u) [CommRing k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] (x : Quiver.TotalPath (Quiver.Symmetrify Q)) : (preprojectiveOpAlgEquiv k Q) ((preprojectiveMk k Q) (PathAlgebra.ofPath x)) = MulOpposite.op ((preprojectiveMk k Q) (PathAlgebra.ofPath x.reverse))

On a path class, the opposite-algebra isomorphism takes the opposite of the class of the reversed path.

theorem TauCeti.preprojectiveOpAlgEquiv_symm_op_preprojectiveMk_ofPath (k : Type w) (Q : Type u) [CommRing k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] (x : Quiver.TotalPath (Quiver.Symmetrify Q)) : (preprojectiveOpAlgEquiv k Q).symm (MulOpposite.op ((preprojectiveMk k Q) (PathAlgebra.ofPath x))) = (preprojectiveMk k Q) (PathAlgebra.ofPath x.reverse)

The inverse opposite-algebra isomorphism reverses a path representative as well.

theorem TauCeti.preprojectiveOpAlgEquiv_preprojectiveMk_doubledVertexIdempotent (k : Type w) (Q : Type u) [CommRing k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] (i : Q) : (preprojectiveOpAlgEquiv k Q) ((preprojectiveMk k Q) (doubledVertexIdempotent k i)) = MulOpposite.op ((preprojectiveMk k Q) (doubledVertexIdempotent k i))

The opposite-algebra isomorphism fixes every vertex idempotent class, up to passage to the opposite algebra.

theorem TauCeti.preprojectiveOpAlgEquiv_preprojectiveMk_ofArrow (k : Type w) (Q : Type u) [CommRing k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] {i j : Quiver.Symmetrify Q} (a : i ⟶ j) : (preprojectiveOpAlgEquiv k Q) ((preprojectiveMk k Q) (PathAlgebra.ofArrow a)) = MulOpposite.op ((preprojectiveMk k Q) (PathAlgebra.ofArrow (Quiver.reverse a)))

The opposite-algebra isomorphism sends a doubled arrow class to the opposite of the class of its formal reverse.