The additive preprojective algebra of a finite quiver

The additive preprojective algebra Π_k(Q) of a finite quiver Q is the path algebra of the doubled quiver Quiver.Symmetrify Q modulo the ideal generated by the sum, over the arrows a of Q, of the commutator of a with its formal reverse a*. Doubling adds to each arrow a : i ⟶ j of Q a formal reverse a* : j ⟶ i, so each arrow of Q gives two length-two loops of Quiver.Symmetrify Q: one at the head j of a, and one at its tail i.

Tau Ceti multiplies paths in the later-factor-first order, so the loop at the head of a — the one which traverses a* and then a — is the product ofArrow a * ofArrow (reverse a), and that is what the displayed word a a* in the literature means. This file names the two loops TauCeti.headBacktrackElem and TauCeti.tailBacktrackElem and proves the corner identities which locate them: a a* lies in the corner of the head of a, and a* a in the corner of its tail.

The relation itself is packaged twice. The global relator TauCeti.preprojectiveRelator is the single element ∑_a (a a* - a* a), and the local relator TauCeti.localPreprojectiveRelator k v is the vertex-corner expression

ρ_v = ∑_{head a = v} a a* - ∑_{tail a = v} a* a.

The two determine each other: ρ is the sum of the ρ_v, and each ρ_v is recovered from ρ by conjugating with the vertex idempotent e_v. Consequently the two-sided ideals they generate agree (TauCeti.preprojectiveIdeal_eq_span_range_localPreprojectiveRelator), so the preprojective algebra may be presented by the single global relation or by the family of local ones, and a map out of it may be built by checking either.

Main definitions

• TauCeti.doubledVertexIdempotent: the vertex idempotent of the doubled path algebra.
• TauCeti.headBacktrackElem and TauCeti.tailBacktrackElem: the two length-two loops a a* and a* a attached to an arrow a of Q.
• TauCeti.gaugedPreprojectiveRelator: the relator with scalar-labelled arrow contributions.
• TauCeti.gaugedPreprojectiveIdeal and TauCeti.gaugedPreprojectiveAlgebra: the relation ideal and quotient algebra for a gauged relator.
• TauCeti.gaugedPreprojectiveMk and TauCeti.gaugedPreprojectiveLift: the gauged quotient map and its universal-property lift.
• TauCeti.preprojectiveRelator: the global relator ∑_a (a a* - a* a).
• TauCeti.localPreprojectiveRelator: the local relator ρ_v at a vertex.
• TauCeti.preprojectiveIdeal: the two-sided ideal generated by the global relator.
• TauCeti.preprojectiveAlgebra: the preprojective algebra Π_k(Q), with quotient map TauCeti.preprojectiveMk.
• TauCeti.preprojectiveLift and TauCeti.preprojectiveLiftOfForallLocalPreprojectiveRelator: the universal property, checked on the global relator or on the local ones.

Main results

• TauCeti.sum_localPreprojectiveRelator: the global relator is the sum of the local ones.
• TauCeti.linearIndependent_backtrackElem: the head backtracks into a vertex and the tail backtracks out of it are linearly independent.
• TauCeti.gaugedPreprojectiveRelator_vertexCorner_eq_sum_sub_sum: the corner of the gauged relator at a vertex.
• TauCeti.preprojectiveRelator_vertexCorner_eq_localPreprojectiveRelator: conjugating the global relator by a vertex idempotent returns the local relator at that vertex.
• TauCeti.preprojectiveIdeal_eq_span_range_localPreprojectiveRelator: the global relation and the family of local relations generate the same two-sided ideal.
• TauCeti.sum_preprojectiveMk_headBacktrackElem_eq_sum_preprojectiveMk_tailBacktrackElem: the defining relation, read in Π_k(Q): at every vertex the incoming loops sum to the outgoing ones.
• TauCeti.preprojectiveLift_unique: the lift of a relation-killing map is the only one.

Implementation notes

The doubled quiver is Mathlib's Quiver.Symmetrify Q, which retains the multiple arrows and the loops of Q: nothing below assumes that Q comes from a simple graph. If Q has a loop a at v, then a a* and a* a are both loops at v, and both occur in the local relator at v, with opposite signs.

Vertices and arrows of Q enter the doubled quiver through Mathlib's inclusion prefunctor Quiver.Symmetrify.of, and formal reverses through Quiver.reverse. This is not cosmetic: Quiver.Symmetrify Q is definitionally Q, so a bare vertex v : Q would let unification pick the quiver structure of Q itself and silently produce an element of the undoubled path algebra. TauCeti.doubledVertexIdempotent pins the doubled structure once, and every statement below is phrased with it and with the two backtracks rather than with raw vertices and arrows.

References

See Crawley-Boevey, Quiver algebras, weighted projective lines, and the Deligne--Simpson problem, Section 1, and Etingof--Eu, Koszulity and the Hilbert series of preprojective algebras, Section 1.

Vertices and the two backtracks of an arrow

noncomputable def TauCeti.doubledVertexIdempotent (k : Type w) {Q : Type u} [Semiring k] [Quiver Q] (v : Q) : pathAlgebra k (Quiver.Symmetrify Q)

The vertex idempotent of the doubled path algebra at a vertex v of Q. This is TauCeti.PathAlgebra.vertexIdempotent for the quiver Quiver.Symmetrify Q; it carries a name of its own because the two vertex types are definitionally equal, so nothing but an explicit choice keeps the doubled quiver structure from being replaced by that of Q.

Equations

• TauCeti.doubledVertexIdempotent k v = TauCeti.PathAlgebra.vertexIdempotent k (Quiver.Symmetrify.of.obj v)

theorem TauCeti.doubledVertexIdempotent_def (k : Type w) {Q : Type u} [Semiring k] [Quiver Q] (v : Q) : doubledVertexIdempotent k v = PathAlgebra.vertexIdempotent k (Quiver.Symmetrify.of.obj v)

The doubled vertex idempotent is the vertex idempotent of the doubled quiver. This is the defining equation, exposed for use outside this module.

noncomputable def TauCeti.headBacktrackElem (k : Type w) {Q : Type u} [Semiring k] [Quiver Q] {i j : Q} (a : i ⟶ j) : pathAlgebra k (Quiver.Symmetrify Q)

The head backtrack of an arrow a : i ⟶ j: the length-two loop of the doubled quiver at the head j of a which traverses the formal reverse a* and then a. In Tau Ceti's later-factor-first convention this is the product ofArrow a * ofArrow (reverse a), which is the word displayed a a* in the literature.

Equations

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

noncomputable def TauCeti.tailBacktrackElem (k : Type w) {Q : Type u} [Semiring k] [Quiver Q] {i j : Q} (a : i ⟶ j) : pathAlgebra k (Quiver.Symmetrify Q)

The tail backtrack of an arrow a : i ⟶ j: the length-two loop of the doubled quiver at the tail i of a which traverses a and then its formal reverse a*. This is the word displayed a* a.

Equations

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

theorem TauCeti.headBacktrackElem_def (k : Type w) {Q : Type u} [Semiring k] [Quiver Q] {i j : Q} (a : i ⟶ j) : headBacktrackElem k a = PathAlgebra.ofPath ⟨Quiver.Symmetrify.of.obj j, ⟨Quiver.Symmetrify.of.obj j, (Quiver.reverse (Quiver.Symmetrify.of.map a)).toPath.comp (Quiver.Symmetrify.of.map a).toPath⟩⟩

The head backtrack is the basis element of the length-two path a* followed by a.

theorem TauCeti.tailBacktrackElem_def (k : Type w) {Q : Type u} [Semiring k] [Quiver Q] {i j : Q} (a : i ⟶ j) : tailBacktrackElem k a = PathAlgebra.ofPath ⟨Quiver.Symmetrify.of.obj i, ⟨Quiver.Symmetrify.of.obj i, (Quiver.Symmetrify.of.map a).toPath.comp (Quiver.reverse (Quiver.Symmetrify.of.map a)).toPath⟩⟩

The tail backtrack is the basis element of the length-two path a followed by a*.

@[simp]

theorem TauCeti.doubledVertexIdempotent_mul_headBacktrackElem (k : Type w) {Q : Type u} [Semiring k] [Quiver Q] {i j : Q} (a : i ⟶ j) : doubledVertexIdempotent k j * headBacktrackElem k a = headBacktrackElem k a

Left multiplication by the head vertex idempotent fixes the head backtrack, placing it in the head vertex corner.

@[simp]

theorem TauCeti.headBacktrackElem_mul_doubledVertexIdempotent (k : Type w) {Q : Type u} [Semiring k] [Quiver Q] {i j : Q} (a : i ⟶ j) : headBacktrackElem k a * doubledVertexIdempotent k j = headBacktrackElem k a

Right multiplication by the head vertex idempotent fixes the head backtrack, placing it in the head vertex corner.

@[simp]

theorem TauCeti.doubledVertexIdempotent_mul_tailBacktrackElem (k : Type w) {Q : Type u} [Semiring k] [Quiver Q] {i j : Q} (a : i ⟶ j) : doubledVertexIdempotent k i * tailBacktrackElem k a = tailBacktrackElem k a

Left multiplication by the tail vertex idempotent fixes the tail backtrack, placing it in the tail vertex corner.

@[simp]

theorem TauCeti.tailBacktrackElem_mul_doubledVertexIdempotent (k : Type w) {Q : Type u} [Semiring k] [Quiver Q] {i j : Q} (a : i ⟶ j) : tailBacktrackElem k a * doubledVertexIdempotent k i = tailBacktrackElem k a

Right multiplication by the tail vertex idempotent fixes the tail backtrack, placing it in the tail vertex corner.

@[simp]

theorem TauCeti.doubledVertexIdempotent_mul_headBacktrackElem_of_ne (k : Type w) {Q : Type u} [Semiring k] [Quiver Q] {i j u : Q} (a : i ⟶ j) (h : u ≠ j) : doubledVertexIdempotent k u * headBacktrackElem k a = 0

A vertex idempotent away from the head of a annihilates the head backtrack on the left.

@[simp]

theorem TauCeti.headBacktrackElem_mul_doubledVertexIdempotent_of_ne (k : Type w) {Q : Type u} [Semiring k] [Quiver Q] {i j u : Q} (a : i ⟶ j) (h : u ≠ j) : headBacktrackElem k a * doubledVertexIdempotent k u = 0

A vertex idempotent away from the head of a annihilates the head backtrack on the right.

@[simp]

theorem TauCeti.doubledVertexIdempotent_mul_tailBacktrackElem_of_ne (k : Type w) {Q : Type u} [Semiring k] [Quiver Q] {i j u : Q} (a : i ⟶ j) (h : u ≠ i) : doubledVertexIdempotent k u * tailBacktrackElem k a = 0

A vertex idempotent away from the tail of a annihilates the tail backtrack on the left.

@[simp]

theorem TauCeti.tailBacktrackElem_mul_doubledVertexIdempotent_of_ne (k : Type w) {Q : Type u} [Semiring k] [Quiver Q] {i j u : Q} (a : i ⟶ j) (h : u ≠ i) : tailBacktrackElem k a * doubledVertexIdempotent k u = 0

A vertex idempotent away from the tail of a annihilates the tail backtrack on the right.

theorem TauCeti.ofArrow_mul_ofArrow_reverse_eq_headBacktrackElem (k : Type w) {Q : Type u} [Semiring k] [Quiver Q] {i j : Q} (a : i ⟶ j) : PathAlgebra.ofArrow (Quiver.Symmetrify.of.map a) * PathAlgebra.ofArrow (Quiver.reverse (Quiver.Symmetrify.of.map a)) = headBacktrackElem k a

The displayed word a a* is the head backtrack under later-factor-first multiplication.

@[simp]

theorem TauCeti.ofPath_headBacktrack_eq_headBacktrackElem (k : Type w) {Q : Type u} [Semiring k] [Quiver Q] {i j : Q} (a : i ⟶ j) : PathAlgebra.ofPath ⟨Quiver.Symmetrify.of.obj j, ⟨Quiver.Symmetrify.of.obj j, (Quiver.reverse (Sum.inl a)).toPath.cons (Sum.inl a)⟩⟩ = headBacktrackElem k a

Simp-normal form of the head-backtrack path.

theorem TauCeti.ofArrow_reverse_mul_ofArrow_eq_tailBacktrackElem (k : Type w) {Q : Type u} [Semiring k] [Quiver Q] {i j : Q} (a : i ⟶ j) : PathAlgebra.ofArrow (Quiver.reverse (Quiver.Symmetrify.of.map a)) * PathAlgebra.ofArrow (Quiver.Symmetrify.of.map a) = tailBacktrackElem k a

The displayed word a* a is the tail backtrack under later-factor-first multiplication.

@[simp]

theorem TauCeti.ofPath_tailBacktrack_eq_tailBacktrackElem (k : Type w) {Q : Type u} [Semiring k] [Quiver Q] {i j : Q} (a : i ⟶ j) : PathAlgebra.ofPath ⟨Quiver.Symmetrify.of.obj i, ⟨Quiver.Symmetrify.of.obj i, (Quiver.Hom.toPath (Sum.inl a)).cons (Quiver.reverse (Sum.inl a))⟩⟩ = tailBacktrackElem k a

Simp-normal form of the tail-backtrack path.

theorem TauCeti.linearIndependent_backtrackElem (k : Type w) {Q : Type u} [Semiring k] [Quiver Q] (v : Q) : LinearIndependent k (Sum.elim (fun (x : (i : Q) × (i ⟶ v)) => headBacktrackElem k x.snd) fun (x : (j : Q) × (v ⟶ j)) => tailBacktrackElem k x.snd)

The backtracks at a vertex are linearly independent. The head backtracks a a* of the arrows a into v and the tail backtracks a* a of the arrows out of v are pairwise distinct paths of the doubled quiver, so they are a linearly independent family in its path algebra.

The global and local preprojective relators

noncomputable def TauCeti.gaugedPreprojectiveRelator (k : Type w) {Q : Type u} [Ring k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] (ε : ⦃i j : Q⦄ → (i ⟶ j) → k) : pathAlgebra k (Quiver.Symmetrify Q)

The gauged preprojective relator ρ_ε = ∑_a ε_a (a a* - a* a) attached to a labelling ε of the arrows of Q by scalars. The constant labelling 1 gives the preprojective relator.

Equations

• TauCeti.gaugedPreprojectiveRelator k ε = ∑ i : Q, ∑ j : Q, ∑ a : i ⟶ j, ε a • (TauCeti.headBacktrackElem k a - TauCeti.tailBacktrackElem k a)

theorem TauCeti.gaugedPreprojectiveRelator_def (k : Type w) {Q : Type u} [Ring k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] (ε : ⦃i j : Q⦄ → (i ⟶ j) → k) : gaugedPreprojectiveRelator k ε = ∑ i : Q, ∑ j : Q, ∑ a : i ⟶ j, ε a • (headBacktrackElem k a - tailBacktrackElem k a)

The gauged relator, unfolded as the weighted sum of the two backtracks over every arrow.

theorem TauCeti.gaugedPreprojectiveRelator_congr (k : Type w) {Q : Type u} [Ring k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] {ε ε' : ⦃i j : Q⦄ → (i ⟶ j) → k} (h : ∀ ⦃i j : Q⦄ (a : i ⟶ j), ε a = ε' a) : gaugedPreprojectiveRelator k ε = gaugedPreprojectiveRelator k ε'

Pointwise equal labellings give the same gauged relator.

noncomputable def TauCeti.preprojectiveRelator (k : Type w) (Q : Type u) [Ring k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] : pathAlgebra k (Quiver.Symmetrify Q)

The global preprojective relator ρ = ∑_a (a a* - a* a), summed over all arrows of Q.

Equations

• TauCeti.preprojectiveRelator k Q = TauCeti.gaugedPreprojectiveRelator k fun (x x_1 : Q) (x_2 : x ⟶ x_1) => 1

@[simp]

theorem TauCeti.gaugedPreprojectiveRelator_one (k : Type w) (Q : Type u) [Ring k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] : (gaugedPreprojectiveRelator k fun (x x_1 : Q) (x_2 : x ⟶ x_1) => 1) = preprojectiveRelator k Q

The constant gauge 1 is the preprojective relator.

theorem TauCeti.preprojectiveRelator_def (k : Type w) (Q : Type u) [Ring k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] : preprojectiveRelator k Q = ∑ i : Q, ∑ j : Q, ∑ a : i ⟶ j, (headBacktrackElem k a - tailBacktrackElem k a)

The global relator, unfolded: the sum over the arrows of Q of the difference of the two backtracks. This is the defining equation, exposed for use outside this module.

noncomputable def TauCeti.localPreprojectiveRelator (k : Type w) {Q : Type u} [Ring k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] (v : Q) : pathAlgebra k (Quiver.Symmetrify Q)

The local preprojective relator at a vertex v,

ρ_v = ∑_{head a = v} a a* - ∑_{tail a = v} a* a,

which lives in the corner cut out by e_v.

Equations

• TauCeti.localPreprojectiveRelator k v = ∑ i : Q, ∑ a : i ⟶ v, TauCeti.headBacktrackElem k a - ∑ j : Q, ∑ a : v ⟶ j, TauCeti.tailBacktrackElem k a

theorem TauCeti.localPreprojectiveRelator_def (k : Type w) {Q : Type u} [Ring k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] (v : Q) : localPreprojectiveRelator k v = ∑ i : Q, ∑ a : i ⟶ v, headBacktrackElem k a - ∑ j : Q, ∑ a : v ⟶ j, tailBacktrackElem k a

The local preprojective relator at a vertex, by its defining sum. This is the defining equation, exposed for use outside this module.

theorem TauCeti.sum_localPreprojectiveRelator (k : Type w) {Q : Type u} [Ring k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] : ∑ v : Q, localPreprojectiveRelator k v = preprojectiveRelator k Q

The global relator is the sum of the local ones: each arrow contributes its head backtrack to the relator at its head, and its tail backtrack to the relator at its tail.

@[simp]

theorem TauCeti.doubledVertexIdempotent_mul_localPreprojectiveRelator (k : Type w) {Q : Type u} [Ring k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] (v : Q) : doubledVertexIdempotent k v * localPreprojectiveRelator k v = localPreprojectiveRelator k v

Left multiplication by the idempotent at v fixes the local relator at v.

@[simp]

theorem TauCeti.localPreprojectiveRelator_mul_doubledVertexIdempotent (k : Type w) {Q : Type u} [Ring k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] (v : Q) : localPreprojectiveRelator k v * doubledVertexIdempotent k v = localPreprojectiveRelator k v

Right multiplication by the idempotent at v fixes the local relator at v.

@[simp]

theorem TauCeti.doubledVertexIdempotent_mul_localPreprojectiveRelator_of_ne (k : Type w) {Q : Type u} [Ring k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] {u v : Q} (h : u ≠ v) : doubledVertexIdempotent k u * localPreprojectiveRelator k v = 0

The local relator at v is annihilated by every other vertex idempotent: it lies in the corner at v.

@[simp]

theorem TauCeti.localPreprojectiveRelator_mul_doubledVertexIdempotent_of_ne (k : Type w) {Q : Type u} [Ring k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] {u v : Q} (h : u ≠ v) : localPreprojectiveRelator k v * doubledVertexIdempotent k u = 0

The local relator at v is annihilated on the right by every other vertex idempotent.

theorem TauCeti.preprojectiveRelator_vertexCorner_eq_localPreprojectiveRelator (k : Type w) {Q : Type u} [Ring k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] (v : Q) : doubledVertexIdempotent k v * preprojectiveRelator k Q * doubledVertexIdempotent k v = localPreprojectiveRelator k v

The local relator is the corner of the global one: conjugating ρ by the idempotent at v returns ρ_v. Together with TauCeti.sum_localPreprojectiveRelator this says that the single global relation and the family of local relations carry the same information.

theorem TauCeti.gaugedPreprojectiveRelator_vertexCorner_eq_sum_sub_sum (k : Type w) {Q : Type u} [CommRing k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] (ε : ⦃i j : Q⦄ → (i ⟶ j) → k) (v : Q) : doubledVertexIdempotent k v * gaugedPreprojectiveRelator k ε * doubledVertexIdempotent k v = ∑ i : Q, ∑ a : i ⟶ v, ε a • headBacktrackElem k a - ∑ j : Q, ∑ a : v ⟶ j, ε a • tailBacktrackElem k a

The corner of the gauged preprojective relator at a vertex: conjugating ρ_ε by the idempotent at v keeps the weighted head backtracks of the arrows into v and the weighted tail backtracks of the arrows out of v. For the constant gauge this is TauCeti.preprojectiveRelator_vertexCorner_eq_localPreprojectiveRelator.

The relation ideal

noncomputable def TauCeti.gaugedPreprojectiveIdeal (k : Type w) {Q : Type u} [Ring k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] (ε : ⦃i j : Q⦄ → (i ⟶ j) → k) : TwoSidedIdeal (pathAlgebra k (Quiver.Symmetrify Q))

The two-sided ideal generated by a gauged preprojective relator.

Equations

• TauCeti.gaugedPreprojectiveIdeal k ε = TwoSidedIdeal.span {TauCeti.gaugedPreprojectiveRelator k ε}

theorem TauCeti.gaugedPreprojectiveIdeal_eq_span (k : Type w) {Q : Type u} [Ring k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] (ε : ⦃i j : Q⦄ → (i ⟶ j) → k) : gaugedPreprojectiveIdeal k ε = TwoSidedIdeal.span {gaugedPreprojectiveRelator k ε}

The gauged relation ideal is the two-sided span of its gauged relator.

theorem TauCeti.gaugedPreprojectiveRelator_mem_gaugedPreprojectiveIdeal (k : Type w) {Q : Type u} [Ring k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] (ε : ⦃i j : Q⦄ → (i ⟶ j) → k) : gaugedPreprojectiveRelator k ε ∈ gaugedPreprojectiveIdeal k ε

noncomputable def TauCeti.preprojectiveIdeal (k : Type w) (Q : Type u) [Ring k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] : TwoSidedIdeal (pathAlgebra k (Quiver.Symmetrify Q))

The two-sided ideal of preprojective relations: the ideal generated by the global relator.

Equations

• TauCeti.preprojectiveIdeal k Q = TwoSidedIdeal.span {TauCeti.preprojectiveRelator k Q}

theorem TauCeti.preprojectiveIdeal_eq_span (k : Type w) (Q : Type u) [Ring k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] : preprojectiveIdeal k Q = TwoSidedIdeal.span {preprojectiveRelator k Q}

The relation ideal, unfolded: the two-sided span of the global relator. This is the defining equation, exposed for use outside this module.

theorem TauCeti.preprojectiveRelator_mem_preprojectiveIdeal (k : Type w) (Q : Type u) [Ring k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] : preprojectiveRelator k Q ∈ preprojectiveIdeal k Q

theorem TauCeti.localPreprojectiveRelator_mem_preprojectiveIdeal (k : Type w) {Q : Type u} [Ring k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] (v : Q) : localPreprojectiveRelator k v ∈ preprojectiveIdeal k Q

theorem TauCeti.preprojectiveIdeal_eq_span_range_localPreprojectiveRelator (k : Type w) (Q : Type u) [Ring k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] : preprojectiveIdeal k Q = TwoSidedIdeal.span (Set.range (localPreprojectiveRelator k))

The global relation and the local corner relations present the same algebra. The local relators generate the relation ideal because they are the corners of the global one, and the global relator lies in the ideal they generate because it is their sum.

The preprojective algebra

@[reducible, inline]

noncomputable abbrev TauCeti.gaugedPreprojectiveAlgebra (k : Type w) {Q : Type u} [CommRing k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] (ε : ⦃i j : Q⦄ → (i ⟶ j) → k) : Type (max (max (max u v) w) (max w v) u)

The gauged preprojective algebra Π_k(Q, ε): the path algebra of the doubled quiver modulo the gauged relator.

Equations

• TauCeti.gaugedPreprojectiveAlgebra k ε = (TauCeti.pathAlgebra k (Quiver.Symmetrify Q) ⧸ TwoSidedIdeal.asIdeal (TauCeti.gaugedPreprojectiveIdeal k ε))

noncomputable def TauCeti.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) : pathAlgebra k (Quiver.Symmetrify Q) →ₐ[k] gaugedPreprojectiveAlgebra k ε

The quotient map onto the gauged preprojective algebra.

Equations

• TauCeti.gaugedPreprojectiveMk k ε = Ideal.Quotient.mkₐ k (TwoSidedIdeal.asIdeal (TauCeti.gaugedPreprojectiveIdeal k ε))

theorem TauCeti.gaugedPreprojectiveMk_apply (k : Type w) {Q : Type u} [CommRing k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] (ε : ⦃i j : Q⦄ → (i ⟶ j) → k) (f : pathAlgebra k (Quiver.Symmetrify Q)) : (gaugedPreprojectiveMk k ε) f = (Ideal.Quotient.mk (TwoSidedIdeal.asIdeal (gaugedPreprojectiveIdeal k ε))) f

theorem TauCeti.gaugedPreprojectiveMk_surjective (k : Type w) {Q : Type u} [CommRing k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] (ε : ⦃i j : Q⦄ → (i ⟶ j) → k) : Function.Surjective ⇑(gaugedPreprojectiveMk k ε)

@[simp]

theorem TauCeti.gaugedPreprojectiveMk_eq_zero_iff (k : Type w) {Q : Type u} [CommRing k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] (ε : ⦃i j : Q⦄ → (i ⟶ j) → k) {f : pathAlgebra k (Quiver.Symmetrify Q)} : (gaugedPreprojectiveMk k ε) f = 0 ↔ f ∈ gaugedPreprojectiveIdeal k ε

@[simp]

theorem TauCeti.gaugedPreprojectiveMk_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) : (gaugedPreprojectiveMk k ε) (gaugedPreprojectiveRelator k ε) = 0

@[reducible, inline]

noncomputable abbrev TauCeti.preprojectiveAlgebra (k : Type w) (Q : Type u) [CommRing k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] : Type (max (max (max u v) w) (max w v) u)

The additive preprojective algebra Π_k(Q): the path algebra of the doubled quiver Quiver.Symmetrify Q modulo the preprojective relation. Its independence of the chosen orientation of the underlying graph is a theorem comparing the algebras of two different quivers, not part of this definition.

Equations

• TauCeti.preprojectiveAlgebra k Q = (TauCeti.pathAlgebra k (Quiver.Symmetrify Q) ⧸ TwoSidedIdeal.asIdeal (TauCeti.preprojectiveIdeal k Q))

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

The quotient map onto the preprojective algebra.

Equations

• TauCeti.preprojectiveMk k Q = Ideal.Quotient.mkₐ k (TwoSidedIdeal.asIdeal (TauCeti.preprojectiveIdeal k Q))

theorem TauCeti.preprojectiveMk_apply (k : Type w) (Q : Type u) [CommRing k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] (f : pathAlgebra k (Quiver.Symmetrify Q)) : (preprojectiveMk k Q) f = (Ideal.Quotient.mk (TwoSidedIdeal.asIdeal (preprojectiveIdeal k Q))) f

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

@[simp]

theorem TauCeti.preprojectiveMk_eq_zero_iff (k : Type w) (Q : Type u) [CommRing k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] {f : pathAlgebra k (Quiver.Symmetrify Q)} : (preprojectiveMk k Q) f = 0 ↔ f ∈ preprojectiveIdeal k Q

@[simp]

theorem TauCeti.preprojectiveMk_preprojectiveRelator (k : Type w) (Q : Type u) [CommRing k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] : (preprojectiveMk k Q) (preprojectiveRelator k Q) = 0

@[simp]

theorem TauCeti.preprojectiveMk_localPreprojectiveRelator (k : Type w) {Q : Type u} [CommRing k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] (v : Q) : (preprojectiveMk k Q) (localPreprojectiveRelator k v) = 0

theorem TauCeti.sum_preprojectiveMk_headBacktrackElem_eq_sum_preprojectiveMk_tailBacktrackElem (k : Type w) {Q : Type u} [CommRing k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] (v : Q) : ∑ i : Q, ∑ a : i ⟶ v, (preprojectiveMk k Q) (headBacktrackElem k a) = ∑ j : Q, ∑ a : v ⟶ j, (preprojectiveMk k Q) (tailBacktrackElem k a)

The defining relation of the preprojective algebra, read at a vertex v of Q: the head backtracks of the arrows into v sum to the tail backtracks of the arrows out of v.

The gauged universal property

theorem TauCeti.gaugedPreprojectiveIdeal_le_ker (k : Type w) {Q : Type u} {B : Type u_1} [CommRing k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] [Semiring B] [Algebra k B] (ε : ⦃i j : Q⦄ → (i ⟶ j) → k) (f : pathAlgebra k (Quiver.Symmetrify Q) →ₐ[k] B) (hf : f (gaugedPreprojectiveRelator k ε) = 0) : gaugedPreprojectiveIdeal k ε ≤ TwoSidedIdeal.ker f

An algebra map out of the doubled path algebra which kills a gauged relator kills the whole gauged relation ideal.

noncomputable def TauCeti.gaugedPreprojectiveLift (k : Type w) {Q : Type u} {B : Type u_1} [CommRing k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] [Semiring B] [Algebra k B] (ε : ⦃i j : Q⦄ → (i ⟶ j) → k) (f : pathAlgebra k (Quiver.Symmetrify Q) →ₐ[k] B) (hf : f (gaugedPreprojectiveRelator k ε) = 0) : gaugedPreprojectiveAlgebra k ε →ₐ[k] B

The universal property of the gauged preprojective algebra: an algebra map out of the doubled path algebra which kills the gauged relator descends to the quotient.

Equations

• TauCeti.gaugedPreprojectiveLift k ε f hf = Ideal.Quotient.liftₐ (TwoSidedIdeal.asIdeal (TauCeti.gaugedPreprojectiveIdeal k ε)) f ⋯

theorem TauCeti.gaugedPreprojectiveLift_comp_gaugedPreprojectiveMk (k : Type w) {Q : Type u} {B : Type u_1} [CommRing k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] [Semiring B] [Algebra k B] (ε : ⦃i j : Q⦄ → (i ⟶ j) → k) (f : pathAlgebra k (Quiver.Symmetrify Q) →ₐ[k] B) (hf : f (gaugedPreprojectiveRelator k ε) = 0) : (gaugedPreprojectiveLift k ε f hf).comp (gaugedPreprojectiveMk k ε) = f

@[simp]

theorem TauCeti.gaugedPreprojectiveLift_gaugedPreprojectiveMk (k : Type w) {Q : Type u} {B : Type u_1} [CommRing k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] [Semiring B] [Algebra k B] (ε : ⦃i j : Q⦄ → (i ⟶ j) → k) (f : pathAlgebra k (Quiver.Symmetrify Q) →ₐ[k] B) (hf : f (gaugedPreprojectiveRelator k ε) = 0) (x : pathAlgebra k (Quiver.Symmetrify Q)) : (gaugedPreprojectiveLift k ε f hf) ((gaugedPreprojectiveMk k ε) x) = f x

theorem TauCeti.gaugedPreprojectiveLift_unique (k : Type w) {Q : Type u} {B : Type u_1} [CommRing k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] [Semiring B] [Algebra k B] (ε : ⦃i j : Q⦄ → (i ⟶ j) → k) (f : pathAlgebra k (Quiver.Symmetrify Q) →ₐ[k] B) (hf : f (gaugedPreprojectiveRelator k ε) = 0) (g : gaugedPreprojectiveAlgebra k ε →ₐ[k] B) (hg : g.comp (gaugedPreprojectiveMk k ε) = f) : g = gaugedPreprojectiveLift k ε f hf

The gauged lift is the unique algebra map whose composite with the quotient map is f.

The universal property

theorem TauCeti.preprojectiveIdeal_le_ker {k : Type w} {Q : Type u} {B : Type u_1} [CommRing k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] [Semiring B] [Algebra k B] (f : pathAlgebra k (Quiver.Symmetrify Q) →ₐ[k] B) (hf : f (preprojectiveRelator k Q) = 0) : preprojectiveIdeal k Q ≤ TwoSidedIdeal.ker f

An algebra map out of the doubled path algebra which kills the global relator kills the whole relation ideal.

theorem TauCeti.preprojectiveIdeal_le_ker_of_forall_localPreprojectiveRelator {k : Type w} {Q : Type u} {B : Type u_1} [CommRing k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] [Semiring B] [Algebra k B] (f : pathAlgebra k (Quiver.Symmetrify Q) →ₐ[k] B) (hf : ∀ (v : Q), f (localPreprojectiveRelator k v) = 0) : preprojectiveIdeal k Q ≤ TwoSidedIdeal.ker f

An algebra map out of the doubled path algebra which kills every local relator kills the whole relation ideal. This is the form in which the relations are usually checked: one identity per vertex, each between elements of a single corner.

noncomputable def TauCeti.preprojectiveLift {k : Type w} {Q : Type u} {B : Type u_1} [CommRing k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] [Semiring B] [Algebra k B] (f : pathAlgebra k (Quiver.Symmetrify Q) →ₐ[k] B) (hf : f (preprojectiveRelator k Q) = 0) : preprojectiveAlgebra k Q →ₐ[k] B

The universal property of the preprojective algebra: an algebra map out of the doubled path algebra which kills the global relator descends to Π_k(Q).

Equations

• TauCeti.preprojectiveLift f hf = Ideal.Quotient.liftₐ (TwoSidedIdeal.asIdeal (TauCeti.preprojectiveIdeal k Q)) f ⋯

theorem TauCeti.preprojectiveLift_comp_preprojectiveMk {k : Type w} {Q : Type u} {B : Type u_1} [CommRing k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] [Semiring B] [Algebra k B] (f : pathAlgebra k (Quiver.Symmetrify Q) →ₐ[k] B) (hf : f (preprojectiveRelator k Q) = 0) : (preprojectiveLift f hf).comp (preprojectiveMk k Q) = f

@[simp]

theorem TauCeti.preprojectiveLift_preprojectiveMk {k : Type w} {Q : Type u} {B : Type u_1} [CommRing k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] [Semiring B] [Algebra k B] (f : pathAlgebra k (Quiver.Symmetrify Q) →ₐ[k] B) (hf : f (preprojectiveRelator k Q) = 0) (x : pathAlgebra k (Quiver.Symmetrify Q)) : (preprojectiveLift f hf) ((preprojectiveMk k Q) x) = f x

theorem TauCeti.preprojectiveLift_unique {k : Type w} {Q : Type u} {B : Type u_1} [CommRing k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] [Semiring B] [Algebra k B] (f : pathAlgebra k (Quiver.Symmetrify Q) →ₐ[k] B) (hf : f (preprojectiveRelator k Q) = 0) (g : preprojectiveAlgebra k Q →ₐ[k] B) (hg : g.comp (preprojectiveMk k Q) = f) : g = preprojectiveLift f hf

The lift is the only one: the quotient map is surjective, so an algebra map on Π_k(Q) is determined by its composite with it.

noncomputable def TauCeti.preprojectiveLiftOfForallLocalPreprojectiveRelator {k : Type w} {Q : Type u} {B : Type u_1} [CommRing k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] [Semiring B] [Algebra k B] (f : pathAlgebra k (Quiver.Symmetrify Q) →ₐ[k] B) (hf : ∀ (v : Q), f (localPreprojectiveRelator k v) = 0) : preprojectiveAlgebra k Q →ₐ[k] B

The local-relations form of the universal property: a map killing every vertex-corner relator descends to the preprojective algebra.

Equations

• TauCeti.preprojectiveLiftOfForallLocalPreprojectiveRelator f hf = TauCeti.preprojectiveLift f ⋯

theorem TauCeti.preprojectiveLiftOfForallLocalPreprojectiveRelator_comp_preprojectiveMk {k : Type w} {Q : Type u} {B : Type u_1} [CommRing k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] [Semiring B] [Algebra k B] (f : pathAlgebra k (Quiver.Symmetrify Q) →ₐ[k] B) (hf : ∀ (v : Q), f (localPreprojectiveRelator k v) = 0) : (preprojectiveLiftOfForallLocalPreprojectiveRelator f hf).comp (preprojectiveMk k Q) = f

@[simp]

theorem TauCeti.preprojectiveLiftOfForallLocalPreprojectiveRelator_preprojectiveMk {k : Type w} {Q : Type u} {B : Type u_1} [CommRing k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] [Semiring B] [Algebra k B] (f : pathAlgebra k (Quiver.Symmetrify Q) →ₐ[k] B) (hf : ∀ (v : Q), f (localPreprojectiveRelator k v) = 0) (x : pathAlgebra k (Quiver.Symmetrify Q)) : (preprojectiveLiftOfForallLocalPreprojectiveRelator f hf) ((preprojectiveMk k Q) x) = f x

theorem TauCeti.preprojectiveLiftOfForallLocalPreprojectiveRelator_unique {k : Type w} {Q : Type u} {B : Type u_1} [CommRing k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] [Semiring B] [Algebra k B] (f : pathAlgebra k (Quiver.Symmetrify Q) →ₐ[k] B) (hf : ∀ (v : Q), f (localPreprojectiveRelator k v) = 0) (g : preprojectiveAlgebra k Q →ₐ[k] B) (hg : g.comp (preprojectiveMk k Q) = f) : g = preprojectiveLiftOfForallLocalPreprojectiveRelator f hf

A lift constructed from the local relations is uniquely determined by its composite with the quotient map.