Orientation independence of the additive preprojective algebra

The additive preprojective algebra Π_k(Q) is built from the doubled quiver of Q, so it ought not to depend on which of the two directions of each edge was chosen as the arrow of Q. That independence is not a formality: the defining relator

ρ = ∑_a (a a* - a* a)

pairs each arrow with its formal reverse with a sign, and turning an arrow around exchanges the two backtracks, hence negates the corresponding summand. This file proves the independence by exhibiting the isomorphism which repairs that sign.

Fix a Bool-valued labelling σ of the arrows of Q and let Reorient Q σ be the quiver of TauCeti.Reorient, obtained by turning around exactly the arrows labelled true. The two doubled quivers are identified by TauCeti.reorientSymmetrify, hence the two doubled path algebras by TauCeti.reorientDoubledEquiv. Under that identification the relator of Reorient Q σ becomes the gauged relator ρ_ε = ∑_a ε_a (a a* - a* a) of Q, with ε_a = -1 exactly when σ turns a around (TauCeti.reorientDoubledEquiv_preprojectiveRelator), and matching the relations one vertex at a time (TauCeti.reorientDoubledEquiv_localPreprojectiveRelator). Composing with the gauge isomorphism of TauCeti.RepresentationTheory.Quiver.Preprojective.Gauge, which rescales the sign-flipped arrows by -1 and fixes their formal reverses, gives

Π_k(Reorient Q σ) ≃ₐ[k] Π_k(Q).

Turning around a single arrow is the case of a labelling supported on one arrow; an arbitrary σ performs an arbitrary composite of such flips in one step, so the isomorphism above compares Q with the explicit quiver Reorient Q σ. Nothing is assumed about the characteristic of k: in characteristic two the sign is invisible, and the same statement is obtained from the same proof.

Main definitions

• TauCeti.reorientSign and TauCeti.reorientSignUnit: the labelling by -1 on the arrows σ turns around and by 1 elsewhere, valued in k and in kˣ.
• TauCeti.reorientDoubledEquiv: the isomorphism of doubled path algebras induced by the comparison of doubled quivers.
• TauCeti.reorientPreprojectiveAlgebraEquivGauged: the reoriented preprojective algebra, presented by the signed relator of Q.
• TauCeti.reorientPreprojectiveAlgebraEquiv: orientation independence.

Main results

• TauCeti.reorientDoubledEquiv_headBacktrackElem_flip and TauCeti.reorientDoubledEquiv_tailBacktrackElem_flip: turning an arrow around exchanges its two backtracks. This is the sign.
• TauCeti.reorientDoubledEquiv_preprojectiveRelator: the relator of a reorientation is the signed relator of Q.
• TauCeti.reorientDoubledEquiv_localPreprojectiveRelator: the same, vertex by vertex.
• TauCeti.reorientPreprojectiveAlgebraEquiv_preprojectiveMk: the isomorphism, computed on an arbitrary quotient representative, as the doubled-quiver identification followed by the rescaling by -1 of the turned-around arrows.
• TauCeti.reorientPreprojectiveAlgebraEquiv_preprojectiveMk_ofArrow_keep and its three companions: the isomorphism, computed on each of the four kinds of generator. An arrow σ leaves alone and its formal reverse are fixed, a turned-around arrow is carried to a formal reverse, and the formal reverse of a turned-around arrow is carried to the negative of an arrow.

Implementation notes

The counting step is TauCeti.reorientDoubledEquiv_preprojectiveRelator. A turned-around arrow a : j ⟶ i of Q is an arrow i ⟶ j of Reorient Q σ, so its contribution to the relator of the reorientation sits in the (i, j) hom set while its contribution to the signed relator of Q sits in the (j, i) one. The two agree only after the two vertex summations are exchanged, which is what the transposition step of the proof does; the equality does not hold hom set by hom set.

References

See Crawley-Boevey, Quiver algebras, weighted projective lines, and the Deligne--Simpson problem, Section 1.

def TauCeti.reorientSign (k : Type w) {Q : Type u} [One k] [Neg k] [Quiver Q] (σ : ⦃i j : Q⦄ → (i ⟶ j) → Bool) ⦃i j : Q⦄ (a : i ⟶ j) : k

The sign labelling attached to a reorientation: an arrow which σ turns around enters the preprojective relator with the opposite sign, and every other arrow keeps its sign.

Equations

• TauCeti.reorientSign k σ a = if σ a = true then -1 else 1

@[simp]

theorem TauCeti.reorientSign_of_true (k : Type w) {Q : Type u} [One k] [Neg k] [Quiver Q] {σ : ⦃i j : Q⦄ → (i ⟶ j) → Bool} {i j : Q} {a : i ⟶ j} (h : σ a = true) : reorientSign k σ a = -1

A turned-around arrow gets the sign -1.

@[simp]

theorem TauCeti.reorientSign_of_false (k : Type w) {Q : Type u} [One k] [Neg k] [Quiver Q] {σ : ⦃i j : Q⦄ → (i ⟶ j) → Bool} {i j : Q} {a : i ⟶ j} (h : ¬σ a = true) : reorientSign k σ a = 1

An arrow σ leaves alone keeps the sign 1.

def TauCeti.reorientSignUnit (k : Type w) {Q : Type u} [Monoid k] [HasDistribNeg k] [Quiver Q] (σ : ⦃i j : Q⦄ → (i ⟶ j) → Bool) ⦃i j : Q⦄ (a : i ⟶ j) : kˣ

The sign labelling, valued in the units of k.

Equations

• TauCeti.reorientSignUnit k σ a = if σ a = true then -1 else 1

@[simp]

theorem TauCeti.reorientSignUnit_inv (k : Type w) {Q : Type u} [Monoid k] [HasDistribNeg k] [Quiver Q] (σ : ⦃i j : Q⦄ → (i ⟶ j) → Bool) ⦃i j : Q⦄ (a : i ⟶ j) : (reorientSignUnit k σ a)⁻¹ = reorientSignUnit k σ a

The sign labelling takes values in {1, -1}, so it is its own inverse.

theorem TauCeti.reorientSign_eq_coe_reorientSignUnit (k : Type w) {Q : Type u} [Monoid k] [HasDistribNeg k] [Quiver Q] (σ : ⦃i j : Q⦄ → (i ⟶ j) → Bool) ⦃i j : Q⦄ (a : i ⟶ j) : reorientSign k σ a = ↑(reorientSignUnit k σ a)

The sign labelling is the unit-valued one.

The induced isomorphism of doubled path algebras

noncomputable def TauCeti.reorientDoubledEquiv (k : Type w) {Q : Type u} [CommSemiring k] [Quiver Q] [Finite Q] (σ : ⦃i j : Q⦄ → (i ⟶ j) → Bool) : pathAlgebra k (Quiver.Symmetrify (Reorient Q σ)) ≃ₐ[k] pathAlgebra k (Quiver.Symmetrify Q)

The isomorphism of doubled path algebras attached to a reorientation: the path algebra of Symmetrify (Reorient Q σ) and the path algebra of Symmetrify Q are identified along the comparison of doubled quivers, which is the identity on vertices.

Equations

• TauCeti.reorientDoubledEquiv k σ = TauCeti.PathAlgebra.mapAlgEquiv k (TauCeti.reorientSymmetrify σ) (TauCeti.reorientSymmetrifyInv σ) ⋯ ⋯

theorem TauCeti.reorientDoubledEquiv_ofArrow (k : Type w) {Q : Type u} [CommSemiring k] [Quiver Q] [Finite Q] (σ : ⦃i j : Q⦄ → (i ⟶ j) → Bool) {x y : Quiver.Symmetrify (Reorient Q σ)} (b : x ⟶ y) : (reorientDoubledEquiv k σ) (PathAlgebra.ofArrow b) = PathAlgebra.ofArrow ((reorientSymmetrify σ).map b)

Pushing an arrow of the doubled reoriented quiver along the comparison carries it to the image arrow. Deliberately not a simp lemma, TauCeti.PathAlgebra.ofArrow_eq_ofPath already rewriting its left-hand side.

theorem TauCeti.reorientDoubledEquiv_ofArrow_normalized (k : Type w) {Q : Type u} [CommSemiring k] [Quiver Q] [Finite Q] (σ : ⦃i j : Q⦄ → (i ⟶ j) → Bool) {x y : Quiver.Symmetrify (Reorient Q σ)} (b : x ⟶ y) : (reorientDoubledEquiv k σ) (PathAlgebra.ofArrow b) = PathAlgebra.ofArrow (Quiver.homOfEq ((reorientSymmetrify σ).map b) ⋯ ⋯)

The arrow computation for the doubled path-algebra comparison, with its object map normalized to the vertices of the reoriented quiver.

@[simp]

theorem TauCeti.reorientDoubledEquiv_headBacktrackElem_keep (k : Type w) {Q : Type u} [CommSemiring k] [Quiver Q] [Finite Q] (σ : ⦃i j : Q⦄ → (i ⟶ j) → Bool) {i j : Q} (a : i ⟶ j) (ha : ¬σ a = true) : (reorientDoubledEquiv k σ) (headBacktrackElem k (reorientKeep σ a ha)) = headBacktrackElem k a

An arrow which σ leaves alone keeps its head backtrack.

@[simp]

theorem TauCeti.reorientDoubledEquiv_tailBacktrackElem_keep (k : Type w) {Q : Type u} [CommSemiring k] [Quiver Q] [Finite Q] (σ : ⦃i j : Q⦄ → (i ⟶ j) → Bool) {i j : Q} (a : i ⟶ j) (ha : ¬σ a = true) : (reorientDoubledEquiv k σ) (tailBacktrackElem k (reorientKeep σ a ha)) = tailBacktrackElem k a

An arrow which σ leaves alone keeps its tail backtrack.

@[simp]

theorem TauCeti.reorientDoubledEquiv_headBacktrackElem_flip (k : Type w) {Q : Type u} [CommSemiring k] [Quiver Q] [Finite Q] (σ : ⦃i j : Q⦄ → (i ⟶ j) → Bool) {i j : Q} (a : j ⟶ i) (ha : σ a = true) : (reorientDoubledEquiv k σ) (headBacktrackElem k (reorientFlip σ a ha)) = tailBacktrackElem k a

Turning an arrow around exchanges its two backtracks: the head backtrack of the turned-around arrow is the tail backtrack of the original.

@[simp]

theorem TauCeti.reorientDoubledEquiv_tailBacktrackElem_flip (k : Type w) {Q : Type u} [CommSemiring k] [Quiver Q] [Finite Q] (σ : ⦃i j : Q⦄ → (i ⟶ j) → Bool) {i j : Q} (a : j ⟶ i) (ha : σ a = true) : (reorientDoubledEquiv k σ) (tailBacktrackElem k (reorientFlip σ a ha)) = headBacktrackElem k a

Turning an arrow around exchanges its two backtracks: the tail backtrack of the turned-around arrow is the head backtrack of the original.

@[simp]

theorem TauCeti.reorientDoubledEquiv_doubledVertexIdempotent (k : Type w) {Q : Type u} [CommSemiring k] [Quiver Q] [Finite Q] (σ : ⦃i j : Q⦄ → (i ⟶ j) → Bool) (v : Q) : (reorientDoubledEquiv k σ) (doubledVertexIdempotent k (reorientVertex σ v)) = doubledVertexIdempotent k v

The comparison of doubled path algebras matches the vertex idempotents.

theorem TauCeti.reorientDoubledEquiv_sub_keep (k : Type w) {Q : Type u} [CommRing k] [Quiver Q] [Finite Q] (σ : ⦃i j : Q⦄ → (i ⟶ j) → Bool) {i j : Q} (a : i ⟶ j) (ha : ¬σ a = true) : (reorientDoubledEquiv k σ) (headBacktrackElem k (reorientKeep σ a ha) - tailBacktrackElem k (reorientKeep σ a ha)) = reorientSign k σ a • (headBacktrackElem k a - tailBacktrackElem k a)

An arrow which σ leaves alone contributes its own difference of backtracks.

theorem TauCeti.reorientDoubledEquiv_sub_flip (k : Type w) {Q : Type u} [CommRing k] [Quiver Q] [Finite Q] (σ : ⦃i j : Q⦄ → (i ⟶ j) → Bool) {i j : Q} (a : j ⟶ i) (ha : σ a = true) : (reorientDoubledEquiv k σ) (headBacktrackElem k (reorientFlip σ a ha) - tailBacktrackElem k (reorientFlip σ a ha)) = reorientSign k σ a • (headBacktrackElem k a - tailBacktrackElem k a)

An arrow which σ turns around contributes the negative of its difference of backtracks: turning the arrow around exchanges its head and tail backtracks.

The relator of a reorientation is a signed relator

theorem TauCeti.reorientDoubledEquiv_preprojectiveRelator (k : Type w) {Q : Type u} [CommRing k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] (σ : ⦃i j : Q⦄ → (i ⟶ j) → Bool) : (reorientDoubledEquiv k σ) (preprojectiveRelator k (Reorient Q σ)) = gaugedPreprojectiveRelator k (reorientSign k σ)

The preprojective relator of a reorientation is the signed relator of the original quiver. Under the identification of the two doubled path algebras, the relator ∑_a (a a* - a* a) of Reorient Q σ becomes ∑_a ε_a (a a* - a* a), where ε is -1 exactly on the arrows σ turns around.

theorem TauCeti.reorientDoubledEquiv_localPreprojectiveRelator (k : Type w) {Q : Type u} [CommRing k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] (σ : ⦃i j : Q⦄ → (i ⟶ j) → Bool) (v : Q) : (reorientDoubledEquiv k σ) (localPreprojectiveRelator k (reorientVertex σ v)) = doubledVertexIdempotent k v * gaugedPreprojectiveRelator k (reorientSign k σ) * doubledVertexIdempotent k v

The local relations of a reorientation are the local signed relations. The corner of the relator at a vertex v of Reorient Q σ is carried to the corner at v of the signed relator, so the identification matches the relations one vertex at a time and not merely their sum.

Orientation independence

noncomputable def TauCeti.reorientPreprojectiveAlgebraEquivGauged (k : Type w) {Q : Type u} [CommRing k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] (σ : ⦃i j : Q⦄ → (i ⟶ j) → Bool) : preprojectiveAlgebra k (Reorient Q σ) ≃ₐ[k] gaugedPreprojectiveAlgebra k (reorientSign k σ)

The preprojective algebra of a reorientation, presented by the signed relator of the original quiver.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def TauCeti.reorientPreprojectiveAlgebraEquiv (k : Type w) {Q : Type u} [CommRing k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] (σ : ⦃i j : Q⦄ → (i ⟶ j) → Bool) : preprojectiveAlgebra k (Reorient Q σ) ≃ₐ[k] preprojectiveAlgebra k Q

Orientation independence of the additive preprojective algebra. Turning around any set of arrows of Q gives an isomorphic preprojective algebra: the doubled quivers are identified, and the resulting change of sign in the relator is undone by rescaling the turned-around arrows by -1. No hypothesis on the characteristic is needed.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.reorientPreprojectiveAlgebraEquivGauged_preprojectiveMk (k : Type w) {Q : Type u} [CommRing k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] (σ : ⦃i j : Q⦄ → (i ⟶ j) → Bool) (x : pathAlgebra k (Quiver.Symmetrify (Reorient Q σ))) : (reorientPreprojectiveAlgebraEquivGauged k σ) ((preprojectiveMk k (Reorient Q σ)) x) = (gaugedPreprojectiveMk k (reorientSign k σ)) ((reorientDoubledEquiv k σ) x)

The presentation of the reoriented algebra by the signed relator, computed on an arbitrary quotient representative.

@[simp]

theorem TauCeti.reorientPreprojectiveAlgebraEquiv_preprojectiveMk (k : Type w) {Q : Type u} [CommRing k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] (σ : ⦃i j : Q⦄ → (i ⟶ j) → Bool) (x : pathAlgebra k (Quiver.Symmetrify (Reorient Q σ))) : (reorientPreprojectiveAlgebraEquiv k σ) ((preprojectiveMk k (Reorient Q σ)) x) = (preprojectiveMk k Q) ((PathAlgebra.rescale (doubledLabelling k fun (x x_1 : Q) (a : x ⟶ x_1) => reorientSign k σ a)) ((reorientDoubledEquiv k σ) x))

The orientation-independence isomorphism, computed on generators: it identifies the two doubled path algebras and then rescales, by -1, exactly the arrows σ turns around, leaving every formal reverse alone. This is the explicit map, in the form which makes the sign visible.

The four equations below compute the isomorphism on the generators of the reoriented algebra, which are the arrows of Symmetrify (Reorient Q σ). They are deliberately not simp lemmas, TauCeti.PathAlgebra.ofArrow_eq_ofPath and Quiver.Symmetrify.of_map already rewriting their left-hand sides. Each proof computes the image through TauCeti.reorientDoubledEquiv_ofArrow_normalized, so the object map is rewritten explicitly rather than discharged by definitional equality.

theorem TauCeti.reorientPreprojectiveAlgebraEquiv_preprojectiveMk_ofArrow_keep (k : Type w) {Q : Type u} [CommRing k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] (σ : ⦃i j : Q⦄ → (i ⟶ j) → Bool) {i j : Q} (a : i ⟶ j) (ha : ¬σ a = true) : (reorientPreprojectiveAlgebraEquiv k σ) ((preprojectiveMk k (Reorient Q σ)) (PathAlgebra.ofArrow (Quiver.Symmetrify.of.map (reorientKeep σ a ha)))) = (preprojectiveMk k Q) (PathAlgebra.ofArrow (Quiver.Symmetrify.of.map a))

The isomorphism fixes an arrow which σ leaves alone.

theorem TauCeti.reorientPreprojectiveAlgebraEquiv_preprojectiveMk_ofArrow_reverse_keep (k : Type w) {Q : Type u} [CommRing k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] (σ : ⦃i j : Q⦄ → (i ⟶ j) → Bool) {i j : Q} (a : i ⟶ j) (ha : ¬σ a = true) : (reorientPreprojectiveAlgebraEquiv k σ) ((preprojectiveMk k (Reorient Q σ)) (PathAlgebra.ofArrow (Quiver.reverse (Quiver.Symmetrify.of.map (reorientKeep σ a ha))))) = (preprojectiveMk k Q) (PathAlgebra.ofArrow (Quiver.reverse (Quiver.Symmetrify.of.map a)))

The isomorphism fixes the formal reverse of an arrow which σ leaves alone.

theorem TauCeti.reorientPreprojectiveAlgebraEquiv_preprojectiveMk_ofArrow_flip (k : Type w) {Q : Type u} [CommRing k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] (σ : ⦃i j : Q⦄ → (i ⟶ j) → Bool) {i j : Q} (a : j ⟶ i) (ha : σ a = true) : (reorientPreprojectiveAlgebraEquiv k σ) ((preprojectiveMk k (Reorient Q σ)) (PathAlgebra.ofArrow (Quiver.Symmetrify.of.map (reorientFlip σ a ha)))) = (preprojectiveMk k Q) (PathAlgebra.ofArrow (Quiver.reverse (Quiver.Symmetrify.of.map a)))

The isomorphism exchanges a turned-around arrow with a formal reverse, without a sign: the arrow of Reorient Q σ carried by a turned-around arrow a of Q goes to the formal reverse of a.

theorem TauCeti.reorientPreprojectiveAlgebraEquiv_preprojectiveMk_ofArrow_reverse_flip (k : Type w) {Q : Type u} [CommRing k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] (σ : ⦃i j : Q⦄ → (i ⟶ j) → Bool) {i j : Q} (a : j ⟶ i) (ha : σ a = true) : (reorientPreprojectiveAlgebraEquiv k σ) ((preprojectiveMk k (Reorient Q σ)) (PathAlgebra.ofArrow (Quiver.reverse (Quiver.Symmetrify.of.map (reorientFlip σ a ha))))) = -(preprojectiveMk k Q) (PathAlgebra.ofArrow (Quiver.Symmetrify.of.map a))

The isomorphism negates the formal reverse of a turned-around arrow. This is the one generator carrying the sign which repairs the change of orientation; every other generator above is carried to a generator on the nose.