Gauge independence of the additive preprojective algebra

The additive preprojective relator of a finite quiver Q is ρ = ∑_a (a a* - a* a), one signed commutator for each arrow a of Q. The choice of sign is a choice of orientation: an arrow and its formal reverse enter ρ with opposite signs, and reversing the orientation of a exchanges the two. The basic preprojective module records the whole family of gauged relators

ρ_ε = ∑_a ε_a (a a* - a* a),

one for each labelling ε of the arrows of Q by scalars; this file proves that whenever two labellings differ by a labelling by units the resulting quotients are isomorphic k-algebras. A labelling ε with values in {1, -1} records the sign with which each edge of the doubled quiver enters the relator, so what is proved here is independence of the presented algebra under a change of those signs, for one fixed quiver Q and hence one fixed doubled quiver. The isomorphism is the explicit arrow rescaling TauCeti.PathAlgebra.rescale, which fixes every vertex idempotent and multiplies each arrow of Q by the unit relating the two labellings; nothing is proved by declaring the defining sum to be orientation-free. Comparing TauCeti.preprojectiveAlgebra k Q with the preprojective algebra of a reoriented quiver Q' is a different statement, which this file does not state and does not prove; see the implementation notes.

The relator is genuinely a sum over the oriented edges of the doubled quiver against an antisymmetric labelling: TauCeti.gaugedPreprojectiveRelator_eq_sum_backtracks rewrites ρ_ε as the paired contributions of a and a* for each original arrow a, whenever ε negates under reversal. The - sign in ρ_ε is exactly the antisymmetry of the labelling.

Main definitions

• TauCeti.gaugedPreprojectiveRelator: the gauged relator ρ_ε.
• TauCeti.gaugedPreprojectiveIdeal, TauCeti.gaugedPreprojectiveAlgebra, TauCeti.gaugedPreprojectiveMk and TauCeti.gaugedPreprojectiveLift: the quotient it presents, with its quotient map and universal property.
• TauCeti.doubledLabelling: the labelling of the doubled quiver carrying a labelling of Q on the arrows of Q and 1 on their formal reverses. Rescaling by it is the gauge transformation.

Main results

• TauCeti.gaugedPreprojectiveRelator_one: at the constant labelling 1 the gauged relator is the preprojective relator, so the gauged algebras extend TauCeti.preprojectiveAlgebra.
• TauCeti.rescale_gaugedPreprojectiveRelator: rescaling the arrows of Q by u and fixing their reverses carries ρ_ε to ρ_{uε}.
• TauCeti.gaugedPreprojectiveAlgebraEquiv: gauge independence, two labellings differing by units present isomorphic algebras.
• TauCeti.preprojectiveAlgebraEquivGauged: every unit-valued gauge presents the preprojective algebra itself.
• TauCeti.gaugedPreprojectiveRelator_eq_sum_backtracks: the gauged relator pairs the two oriented-edge backtracks over each original arrow, for antisymmetric ε.

Implementation notes

Reversing the orientation of an arrow of Q is here a change of the labelling ε, not a change of the quiver: the results below establish gauge independence for the labellings of one fixed quiver and hence in one fixed doubled path algebra. The reorientation form of orientation independence, which compares Q with an explicit Reorient Q σ, is proved in TauCeti.RepresentationTheory.Quiver.Preprojective.Orientation; it consumes the gauge isomorphism below after identifying the two doubled path algebras.

References

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

The gauged relator as an oriented-edge sum

theorem TauCeti.gaugedPreprojectiveRelator_eq_sum_backtracks (k : Type w) {Q : Type u} [Ring k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] (ε : ⦃x y : Quiver.Symmetrify Q⦄ → (x ⟶ y) → k) (hε : ∀ ⦃i j : Q⦄ (a : i ⟶ j), ε (Quiver.reverse (Quiver.Symmetrify.of.map a)) = -ε (Quiver.Symmetrify.of.map a)) : (gaugedPreprojectiveRelator k fun (x x_1 : Q) (a : x ⟶ x_1) => ε (Quiver.Symmetrify.of.map a)) = ∑ i : Q, ∑ j : Q, ∑ a : i ⟶ j, (ε (Quiver.Symmetrify.of.map a) • headBacktrackElem k a + ε (Quiver.reverse (Quiver.Symmetrify.of.map a)) • tailBacktrackElem k a)

The gauged relator is a sum over the oriented edges of the doubled quiver. For a labelling ε which negates under reversal, the right-hand side pairs the two doubled arrows over each arrow a of Q: a and its formal reverse a* contribute ε_a (a a*) and -ε_a (a* a). The subtraction in ρ_ε is the antisymmetry of ε.

The gauge transformation

def TauCeti.doubledLabelling (k : Type w) {Q : Type u} [Quiver Q] [One k] (u : ⦃i j : Q⦄ → (i ⟶ j) → k) ⦃x y : Quiver.Symmetrify Q⦄ : (x ⟶ y) → k

The gauge labelling of the doubled quiver attached to a labelling u of the arrows of Q: it carries u on the arrows of Q and 1 on their formal reverses. Rescaling by it multiplies both backtracks of an arrow a by u a.

Equations

• TauCeti.doubledLabelling k u b = Sum.elim (fun (a : x✝¹ ⟶ x✝) => u a) (fun (x : x✝ ⟶ x✝¹) => 1) b

@[simp]

theorem TauCeti.doubledLabelling_one (k : Type w) {Q : Type u} [Quiver Q] [One k] : (doubledLabelling k fun (x x_1 : Q) (x_2 : x ⟶ x_1) => 1) = fun (x x_1 : Quiver.Symmetrify Q) (x_2 : x ⟶ x_1) => 1

The constant labelling one extends to the constant labelling one on the doubled quiver.

@[simp]

theorem TauCeti.doubledLabelling_of {k : Type w} {Q : Type u} [Quiver Q] [One k] (u : ⦃i j : Q⦄ → (i ⟶ j) → k) {i j : Q} (a : i ⟶ j) : doubledLabelling k u (Quiver.Symmetrify.of.map a) = u a

The gauge labelling on an arrow of Q is the given label.

@[simp]

theorem TauCeti.doubledLabelling_reverse_of {k : Type w} {Q : Type u} [Quiver Q] [One k] (u : ⦃i j : Q⦄ → (i ⟶ j) → k) {i j : Q} (a : i ⟶ j) : doubledLabelling k u (Quiver.reverse (Quiver.Symmetrify.of.map a)) = 1

The gauge labelling on the formal reverse of an arrow of Q is one.

@[simp]

theorem TauCeti.doubledLabelling_mul (k : Type w) {Q : Type u} [Quiver Q] [MulOneClass k] (u u' : ⦃i j : Q⦄ → (i ⟶ j) → k) ⦃x y : Quiver.Symmetrify Q⦄ (b : x ⟶ y) : doubledLabelling k (fun (x x_1 : Q) (a : x ⟶ x_1) => u a * u' a) b = doubledLabelling k u b * doubledLabelling k u' b

Pointwise multiplication of labels on the original arrows becomes pointwise multiplication of their gauge labellings on the doubled quiver.

@[simp]

theorem TauCeti.rescale_doubledLabelling_headBacktrackElem (k : Type w) {Q : Type u} [Quiver Q] [CommSemiring k] [Finite Q] (u : ⦃i j : Q⦄ → (i ⟶ j) → k) {i j : Q} (a : i ⟶ j) : (PathAlgebra.rescale (doubledLabelling k u)) (headBacktrackElem k a) = u a • headBacktrackElem k a

Rescaling by a gauge labelling multiplies the head backtrack of a by the label of a.

@[simp]

theorem TauCeti.rescale_doubledLabelling_tailBacktrackElem (k : Type w) {Q : Type u} [Quiver Q] [CommSemiring k] [Finite Q] (u : ⦃i j : Q⦄ → (i ⟶ j) → k) {i j : Q} (a : i ⟶ j) : (PathAlgebra.rescale (doubledLabelling k u)) (tailBacktrackElem k a) = u a • tailBacktrackElem k a

Rescaling by a gauge labelling multiplies the tail backtrack of a by the label of a.

theorem TauCeti.rescale_gaugedPreprojectiveRelator (k : Type w) {Q : Type u} [Quiver Q] [CommRing k] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] (u ε : ⦃i j : Q⦄ → (i ⟶ j) → k) : (PathAlgebra.rescale (doubledLabelling k u)) (gaugedPreprojectiveRelator k ε) = gaugedPreprojectiveRelator k fun (x x_1 : Q) (a : x ⟶ x_1) => u a * ε a

The gauge transformation acts on the gauged relators: rescaling the arrows of Q by u and fixing their formal reverses carries ρ_ε to ρ_{uε}.

@[simp]

theorem TauCeti.rescale_doubledLabelling_comp (k : Type w) {Q : Type u} [Quiver Q] [CommSemiring k] [Finite Q] (u u' : ⦃i j : Q⦄ → (i ⟶ j) → k) : (PathAlgebra.rescale (doubledLabelling k u)).comp (PathAlgebra.rescale (doubledLabelling k u')) = PathAlgebra.rescale (doubledLabelling k fun (x x_1 : Q) (a : x ⟶ x_1) => u a * u' a)

Gauge rescalings compose by multiplying their labellings pointwise.

theorem TauCeti.rescale_doubledLabelling_rescale_doubledLabelling (k : Type w) {Q : Type u} [Quiver Q] [CommSemiring k] [Finite Q] (u u' : ⦃i j : Q⦄ → (i ⟶ j) → k) (h : ∀ ⦃i j : Q⦄ (a : i ⟶ j), u a * u' a = 1) (z : pathAlgebra k (Quiver.Symmetrify Q)) : (PathAlgebra.rescale (doubledLabelling k u)) ((PathAlgebra.rescale (doubledLabelling k u')) z) = z

Two gauge rescalings whose labellings are pointwise inverse undo one another.

Gauge independence

noncomputable def TauCeti.gaugedPreprojectiveAlgebraEquiv (k : Type w) {Q : Type u} [CommRing k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] (ε ε' : ⦃i j : Q⦄ → (i ⟶ j) → k) (u : ⦃i j : Q⦄ → (i ⟶ j) → kˣ) (h : ∀ ⦃i j : Q⦄ (a : i ⟶ j), ε' a = ↑(u a) * ε a) : gaugedPreprojectiveAlgebra k ε ≃ₐ[k] gaugedPreprojectiveAlgebra k ε'

Gauge independence of the preprojective algebra. Two labellings of the arrows of Q which differ by a labelling u by units present isomorphic algebras: the isomorphism is the arrow rescaling by u, which fixes every vertex idempotent and multiplies each arrow of Q by u, leaving its formal reverse alone. Taking u to be -1 on one arrow and 1 on the others flips the sign with which that arrow enters the relator, which is what reversing its orientation produces once the two doubled quivers are identified; that identification is not carried out here, so this is a statement about two labellings of the one quiver Q, not about two quivers. See the implementation notes.

Equations

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

@[simp]

theorem TauCeti.gaugedPreprojectiveAlgebraEquiv_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) (u : ⦃i j : Q⦄ → (i ⟶ j) → kˣ) (h : ∀ ⦃i j : Q⦄ (a : i ⟶ j), ε' a = ↑(u a) * ε a) (x : pathAlgebra k (Quiver.Symmetrify Q)) : (gaugedPreprojectiveAlgebraEquiv k ε ε' u h) ((gaugedPreprojectiveMk k ε) x) = (gaugedPreprojectiveMk k ε') ((PathAlgebra.rescale (doubledLabelling k fun (x x_1 : Q) (a : x ⟶ x_1) => ↑(u a))) x)

The gauge isomorphism is the arrow rescaling: on an arbitrary quotient representative, it applies the path-algebra rescaling and then the target quotient map.

@[simp]

theorem TauCeti.gaugedPreprojectiveAlgebraEquiv_symm_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) (u : ⦃i j : Q⦄ → (i ⟶ j) → kˣ) (h : ∀ ⦃i j : Q⦄ (a : i ⟶ j), ε' a = ↑(u a) * ε a) (x : pathAlgebra k (Quiver.Symmetrify Q)) : (gaugedPreprojectiveAlgebraEquiv k ε ε' u h).symm ((gaugedPreprojectiveMk k ε') x) = (gaugedPreprojectiveMk k ε) ((PathAlgebra.rescale (doubledLabelling k fun (x x_1 : Q) (a : x ⟶ x_1) => ↑(u a)⁻¹)) x)

The inverse gauge isomorphism is rescaling by the pointwise inverse units.

noncomputable def TauCeti.preprojectiveAlgebraEquivGaugedOne (k : Type w) {Q : Type u} [CommRing k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] : preprojectiveAlgebra k Q ≃ₐ[k] gaugedPreprojectiveAlgebra k fun (x x_1 : Q) (x_2 : x ⟶ x_1) => 1

The canonical identification of the original presentation with the constant gauge 1.

Equations

• TauCeti.preprojectiveAlgebraEquivGaugedOne k = Ideal.quotientEquivAlgOfEq k ⋯

@[simp]

theorem TauCeti.preprojectiveAlgebraEquivGaugedOne_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)) : (preprojectiveAlgebraEquivGaugedOne k) ((preprojectiveMk k Q) x) = (gaugedPreprojectiveMk k fun (x x_1 : Q) (x_2 : x ⟶ x_1) => 1) x

The constant-gauge identification preserves the quotient generators.

@[simp]

theorem TauCeti.preprojectiveAlgebraEquivGaugedOne_symm_gaugedPreprojectiveMk (k : Type w) {Q : Type u} [CommRing k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] (x : pathAlgebra k (Quiver.Symmetrify Q)) : (preprojectiveAlgebraEquivGaugedOne k).symm ((gaugedPreprojectiveMk k fun (x x_1 : Q) (x_2 : x ⟶ x_1) => 1) x) = (preprojectiveMk k Q) x

The inverse constant-gauge identification preserves the quotient generators.

noncomputable def TauCeti.preprojectiveAlgebraEquivGauged (k : Type w) {Q : Type u} [CommRing k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] (ε : ⦃i j : Q⦄ → (i ⟶ j) → k) (u : ⦃i j : Q⦄ → (i ⟶ j) → kˣ) (h : ∀ ⦃i j : Q⦄ (a : i ⟶ j), ε a = ↑(u a)) : preprojectiveAlgebra k Q ≃ₐ[k] gaugedPreprojectiveAlgebra k ε

Every unit-valued gauge presents the preprojective algebra. In particular a labelling of the arrows of Q by signs presents Π_k(Q) for every choice of signs.

Equations

• TauCeti.preprojectiveAlgebraEquivGauged k ε u h = (TauCeti.preprojectiveAlgebraEquivGaugedOne k).trans (TauCeti.gaugedPreprojectiveAlgebraEquiv k (fun (x x_1 : Q) (x_2 : x ⟶ x_1) => 1) ε u ⋯)

@[simp]

theorem TauCeti.preprojectiveAlgebraEquivGauged_preprojectiveMk (k : Type w) {Q : Type u} [CommRing k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] (ε : ⦃i j : Q⦄ → (i ⟶ j) → k) (u : ⦃i j : Q⦄ → (i ⟶ j) → kˣ) (h : ∀ ⦃i j : Q⦄ (a : i ⟶ j), ε a = ↑(u a)) (x : pathAlgebra k (Quiver.Symmetrify Q)) : (preprojectiveAlgebraEquivGauged k ε u h) ((preprojectiveMk k Q) x) = (gaugedPreprojectiveMk k ε) ((PathAlgebra.rescale (doubledLabelling k fun (x x_1 : Q) (a : x ⟶ x_1) => ↑(u a))) x)

The isomorphism onto a unit-valued gauge applies arrow rescaling to an arbitrary quotient representative and then takes its class in the gauged quotient.

@[simp]

theorem TauCeti.preprojectiveAlgebraEquivGauged_symm_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) (u : ⦃i j : Q⦄ → (i ⟶ j) → kˣ) (h : ∀ ⦃i j : Q⦄ (a : i ⟶ j), ε a = ↑(u a)) (x : pathAlgebra k (Quiver.Symmetrify Q)) : (preprojectiveAlgebraEquivGauged k ε u h).symm ((gaugedPreprojectiveMk k ε) x) = (preprojectiveMk k Q) ((PathAlgebra.rescale (doubledLabelling k fun (x x_1 : Q) (a : x ⟶ x_1) => ↑(u a)⁻¹)) x)

The inverse isomorphism from a unit-valued gauge, computed on quotient generators.