The signless preprojective relation

Let R be a quiver with a reversal of arrows, such as the doubled quiver of a simple graph. When the outgoing star at a vertex v is finite, the signless local relator at v is the sum of all length-two backtracks based at v,

s_v = ∑_{e : v ⟶ w} (v → w → v),

The quotient API additionally assumes that R has finitely many vertices and is locally finite; the signless preprojective algebra is then the path algebra of R modulo the two-sided ideal generated by all the s_v. For the doubled quiver of a simple graph G the relator is ∑_{j ∼ i} (i → j → i), the relation which Huerfano and Khovanov find in the quadratic dual of the zigzag algebra of G. Unlike the preprojective relator it carries no signs, and so involves no choice of orientation.

Over a coefficient ring in which 2 = 0 the sign is invisible: the signless and preprojective local relators are the same element, their relation ideals coincide, and the signless algebra of a symmetrified quiver is its preprojective algebra.

For a quiver Q the signless relator of Quiver.Symmetrify Q at v is ∑_{head a = v} a a* + ∑_{tail a = v} a* a, which differs from the local preprojective relator ρ_v = ∑_{head a = v} a a* - ∑_{tail a = v} a* a by the sign of the second sum. When Q is bipartite, that is its vertices carry a colouring c : Q → Bool whose two colours differ at the two ends of every arrow, the signs can be repaired by the arrow rescaling multiplying each arrow a of Q by 1 if its head has colour true and by -1 otherwise. Indeed that labelling turns the preprojective relator into ∑_v ±s_v, and its corner at v is ±s_v, so the two relations generate the same ideal. This gives an explicit isomorphism between the signless algebra of Quiver.Symmetrify Q and the preprojective algebra Π_k(Q). For a source--sink orientation, in which every arrow has its head coloured true, the rescaling is the identity.

Main definitions

• TauCeti.signlessPreprojectiveRelator: the signless local relator s_v.
• TauCeti.signlessPreprojectiveIdeal and TauCeti.signlessPreprojectiveAlgebra: the relation ideal and the quotient algebra, with quotient map TauCeti.signlessPreprojectiveMk and universal property TauCeti.signlessPreprojectiveLift.
• TauCeti.symmetrifySignlessPreprojectiveAlgebraEquiv: the signless algebra of the doubled quiver of a bipartite quiver is its preprojective algebra, by an explicit sign rescaling.

Main results

• TauCeti.signlessPreprojectiveRelator_of: for a symmetrified quiver it is the sum of the head backtracks into and the tail backtracks out of the vertex.
• TauCeti.signlessPreprojectiveRelator_congr: it does not depend on the finiteness structure chosen on the star.
• TauCeti.gaugedPreprojectiveRelator_bipartite_eq_sum_smul: the preprojective relator with arrows signed by the colour of their heads is a signed sum of the signless relators.
• TauCeti.gaugedPreprojectiveRelator_bipartite_vertexCorner_eq_smul: its corner at v is ±s_v.
• TauCeti.symmetrifySignlessPreprojectiveIdeal_eq_gaugedPreprojectiveIdeal: the two relations generate the same ideal.
• TauCeti.symmetrifySignlessPreprojectiveAlgebraEquiv_signlessPreprojectiveMk_of_forall_head: for a source--sink orientation the isomorphism is induced by the identity of path algebras.
• TauCeti.signlessPreprojectiveIdeal_eq_preprojectiveIdeal_of_two_eq_zero and TauCeti.signlessPreprojectiveAlgebraEquivPreprojectiveOfTwoEqZero: in characteristic two the signless and preprojective relations agree for every finite quiver.

Implementation notes

The relator is defined for any quiver with a reversal, in particular for TauCeti.DoubledQuiver G, whose arrows live in Type. The comparison with Π_k(Q) is stated for Quiver.Symmetrify Q, with Q in the universe of quivers accepted by TauCeti.preprojectiveAlgebra. The identification of the relator of TauCeti.DoubledQuiver G with the sum of the backtracks at v, TauCeti.signlessPreprojectiveRelator_vertex, lives downstream in TauCeti.RepresentationTheory.Quiver.Zigzag.Signless, so that this file does not depend on the zigzag theory.

References

S. Huerfano and M. Khovanov, A category for the adjoint representation, Section 3, https://arxiv.org/abs/math/0002060, for the signless relation of the quadratic dual of the zigzag algebra and its comparison with the preprojective relation for bipartite graphs. The preprojective conventions follow Crawley-Boevey, Quiver algebras, weighted projective lines, and the Deligne--Simpson problem, Section 1.

The signless relator

noncomputable def TauCeti.signlessPreprojectiveRelator (k : Type w) {R : Type u} [Semiring k] [Quiver R] [Quiver.HasReverse R] (v : R) [Fintype (Quiver.Star v)] : pathAlgebra k R

The signless local relator at a vertex v: the sum, over the arrows e : v ⟶ w, of the backtrack which traverses e and then its reverse.

Equations

• TauCeti.signlessPreprojectiveRelator k v = ∑ x : Quiver.Star v, TauCeti.PathAlgebra.ofPath ⟨v, ⟨v, x.snd.toPath.comp (Quiver.reverse x.snd).toPath⟩⟩

theorem TauCeti.signlessPreprojectiveRelator_def (k : Type w) {R : Type u} [Semiring k] [Quiver R] [Quiver.HasReverse R] (v : R) [Fintype (Quiver.Star v)] : signlessPreprojectiveRelator k v = ∑ x : Quiver.Star v, PathAlgebra.ofPath ⟨v, ⟨v, x.snd.toPath.comp (Quiver.reverse x.snd).toPath⟩⟩

The signless relator, by its defining sum.

@[simp]

theorem TauCeti.vertexIdempotent_mul_signlessPreprojectiveRelator (k : Type w) {R : Type u} [Semiring k] [Quiver R] [Quiver.HasReverse R] (v : R) [Fintype (Quiver.Star v)] : PathAlgebra.vertexIdempotent k v * signlessPreprojectiveRelator k v = signlessPreprojectiveRelator k v

@[simp]

theorem TauCeti.signlessPreprojectiveRelator_mul_vertexIdempotent (k : Type w) {R : Type u} [Semiring k] [Quiver R] [Quiver.HasReverse R] (v : R) [Fintype (Quiver.Star v)] : signlessPreprojectiveRelator k v * PathAlgebra.vertexIdempotent k v = signlessPreprojectiveRelator k v

@[simp]

theorem TauCeti.vertexIdempotent_mul_signlessPreprojectiveRelator_of_ne (k : Type w) {R : Type u} [Semiring k] [Quiver R] [Quiver.HasReverse R] {u v : R} [Fintype (Quiver.Star v)] (h : u ≠ v) : PathAlgebra.vertexIdempotent k u * signlessPreprojectiveRelator k v = 0

The signless relator at v lies in the corner at v: every other vertex idempotent annihilates it on the left.

@[simp]

theorem TauCeti.signlessPreprojectiveRelator_mul_vertexIdempotent_of_ne (k : Type w) {R : Type u} [Semiring k] [Quiver R] [Quiver.HasReverse R] {u v : R} [Fintype (Quiver.Star v)] (h : u ≠ v) : signlessPreprojectiveRelator k v * PathAlgebra.vertexIdempotent k u = 0

Every vertex idempotent other than e_v annihilates the signless relator at v on the right.

theorem TauCeti.signlessPreprojectiveRelator_congr (k : Type w) {R : Type u} [Semiring k] [Quiver R] [Quiver.HasReverse R] (v : R) (i₁ i₂ : Fintype (Quiver.Star v)) : signlessPreprojectiveRelator k v = signlessPreprojectiveRelator k v

The signless relator does not depend on the finiteness structure chosen on the star: any two of them enumerate the same backtracks.

theorem TauCeti.mapAlgHom_signlessPreprojectiveRelator (k : Type w) {R : Type u} [CommSemiring k] [Quiver R] [Quiver.HasReverse R] [Finite R] {v : R} {S : Type u_1} [Quiver S] [Quiver.HasReverse S] [Finite S] (φ : R ⥤q S) [φ.MapReverse] (hφobj : Function.Bijective φ.obj) (hφstar : Function.Bijective (φ.star v)) [Fintype (Quiver.Star v)] [Fintype (Quiver.Star (φ.obj v))] : (PathAlgebra.mapAlgHom k φ hφobj) (signlessPreprojectiveRelator k v) = signlessPreprojectiveRelator k (φ.obj v)

A reversal-preserving prefunctor that is bijective on vertices and on the star at v carries the signless relator at v to the signless relator at its image.

The signless algebra

noncomputable def TauCeti.signlessPreprojectiveIdeal (k : Type w) (R : Type u) [Ring k] [Quiver R] [Quiver.HasReverse R] [(x : R) → Fintype (Quiver.Star x)] : TwoSidedIdeal (pathAlgebra k R)

The two-sided ideal generated by the signless relators at all vertices.

Equations

• TauCeti.signlessPreprojectiveIdeal k R = TwoSidedIdeal.span (Set.range fun (v : R) => TauCeti.signlessPreprojectiveRelator k v)

theorem TauCeti.signlessPreprojectiveIdeal_eq_span (k : Type w) (R : Type u) [Ring k] [Quiver R] [Quiver.HasReverse R] [(x : R) → Fintype (Quiver.Star x)] : signlessPreprojectiveIdeal k R = TwoSidedIdeal.span (Set.range fun (v : R) => signlessPreprojectiveRelator k v)

The signless ideal is the two-sided span of the signless relators.

theorem TauCeti.signlessPreprojectiveRelator_mem_signlessPreprojectiveIdeal (k : Type w) {R : Type u} [Ring k] [Quiver R] [Quiver.HasReverse R] [(x : R) → Fintype (Quiver.Star x)] (v : R) : signlessPreprojectiveRelator k v ∈ signlessPreprojectiveIdeal k R

@[reducible, inline]

noncomputable abbrev TauCeti.signlessPreprojectiveAlgebra (k : Type w) (R : Type u) [CommRing k] [Quiver R] [Quiver.HasReverse R] [Finite R] [(x : R) → Fintype (Quiver.Star x)] : Type (max (max (max u v) w) (max w v) u)

The signless preprojective algebra: the path algebra of R modulo the signless relators.

Equations

• TauCeti.signlessPreprojectiveAlgebra k R = (TauCeti.pathAlgebra k R ⧸ TwoSidedIdeal.asIdeal (TauCeti.signlessPreprojectiveIdeal k R))

noncomputable def TauCeti.signlessPreprojectiveMk (k : Type w) (R : Type u) [CommRing k] [Quiver R] [Quiver.HasReverse R] [Finite R] [(x : R) → Fintype (Quiver.Star x)] : pathAlgebra k R →ₐ[k] signlessPreprojectiveAlgebra k R

The quotient map onto the signless preprojective algebra.

Equations

• TauCeti.signlessPreprojectiveMk k R = Ideal.Quotient.mkₐ k (TwoSidedIdeal.asIdeal (TauCeti.signlessPreprojectiveIdeal k R))

theorem TauCeti.signlessPreprojectiveMk_apply (k : Type w) (R : Type u) [CommRing k] [Quiver R] [Quiver.HasReverse R] [Finite R] [(x : R) → Fintype (Quiver.Star x)] (f : pathAlgebra k R) : (signlessPreprojectiveMk k R) f = (Ideal.Quotient.mk (TwoSidedIdeal.asIdeal (signlessPreprojectiveIdeal k R))) f

theorem TauCeti.signlessPreprojectiveMk_surjective (k : Type w) (R : Type u) [CommRing k] [Quiver R] [Quiver.HasReverse R] [Finite R] [(x : R) → Fintype (Quiver.Star x)] : Function.Surjective ⇑(signlessPreprojectiveMk k R)

@[simp]

theorem TauCeti.signlessPreprojectiveMk_eq_zero_iff (k : Type w) (R : Type u) [CommRing k] [Quiver R] [Quiver.HasReverse R] [Finite R] [(x : R) → Fintype (Quiver.Star x)] {f : pathAlgebra k R} : (signlessPreprojectiveMk k R) f = 0 ↔ f ∈ signlessPreprojectiveIdeal k R

@[simp]

theorem TauCeti.signlessPreprojectiveMk_signlessPreprojectiveRelator (k : Type w) {R : Type u} [CommRing k] [Quiver R] [Quiver.HasReverse R] [Finite R] [(x : R) → Fintype (Quiver.Star x)] (v : R) : (signlessPreprojectiveMk k R) (signlessPreprojectiveRelator k v) = 0

The defining relation of the signless algebra: the backtracks at every vertex sum to zero.

theorem TauCeti.signlessPreprojectiveIdeal_le_ker {k : Type w} {R : Type u} {B : Type u_1} [CommRing k] [Quiver R] [Quiver.HasReverse R] [Finite R] [(x : R) → Fintype (Quiver.Star x)] [Semiring B] [Algebra k B] (f : pathAlgebra k R →ₐ[k] B) (hf : ∀ (v : R), f (signlessPreprojectiveRelator k v) = 0) : signlessPreprojectiveIdeal k R ≤ TwoSidedIdeal.ker f

An algebra map out of the path algebra which kills every signless relator kills the signless ideal.

noncomputable def TauCeti.signlessPreprojectiveLift {k : Type w} {R : Type u} {B : Type u_1} [CommRing k] [Quiver R] [Quiver.HasReverse R] [Finite R] [(x : R) → Fintype (Quiver.Star x)] [Semiring B] [Algebra k B] (f : pathAlgebra k R →ₐ[k] B) (hf : ∀ (v : R), f (signlessPreprojectiveRelator k v) = 0) : signlessPreprojectiveAlgebra k R →ₐ[k] B

The universal property of the signless algebra: an algebra map out of the path algebra which kills every signless relator descends to the quotient.

Equations

• TauCeti.signlessPreprojectiveLift f hf = Ideal.Quotient.liftₐ (TwoSidedIdeal.asIdeal (TauCeti.signlessPreprojectiveIdeal k R)) f ⋯

theorem TauCeti.signlessPreprojectiveLift_comp_signlessPreprojectiveMk {k : Type w} {R : Type u} {B : Type u_1} [CommRing k] [Quiver R] [Quiver.HasReverse R] [Finite R] [(x : R) → Fintype (Quiver.Star x)] [Semiring B] [Algebra k B] (f : pathAlgebra k R →ₐ[k] B) (hf : ∀ (v : R), f (signlessPreprojectiveRelator k v) = 0) : (signlessPreprojectiveLift f hf).comp (signlessPreprojectiveMk k R) = f

The lift descends f: composing it with the quotient map recovers f.

@[simp]

theorem TauCeti.signlessPreprojectiveLift_signlessPreprojectiveMk {k : Type w} {R : Type u} {B : Type u_1} [CommRing k] [Quiver R] [Quiver.HasReverse R] [Finite R] [(x : R) → Fintype (Quiver.Star x)] [Semiring B] [Algebra k B] (f : pathAlgebra k R →ₐ[k] B) (hf : ∀ (v : R), f (signlessPreprojectiveRelator k v) = 0) (x : pathAlgebra k R) : (signlessPreprojectiveLift f hf) ((signlessPreprojectiveMk k R) x) = f x

Pointwise, the lift sends the quotient class of x to f x.

theorem TauCeti.signlessPreprojectiveLift_unique {k : Type w} {R : Type u} {B : Type u_1} [CommRing k] [Quiver R] [Quiver.HasReverse R] [Finite R] [(x : R) → Fintype (Quiver.Star x)] [Semiring B] [Algebra k B] (f : pathAlgebra k R →ₐ[k] B) (hf : ∀ (v : R), f (signlessPreprojectiveRelator k v) = 0) (g : signlessPreprojectiveAlgebra k R →ₐ[k] B) (hg : g.comp (signlessPreprojectiveMk k R) = f) : g = signlessPreprojectiveLift f hf

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

Symmetrified quivers

theorem TauCeti.signlessPreprojectiveRelator_of (k : Type w) {Q : Type u} [Semiring k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] (v : Q) : signlessPreprojectiveRelator k (Quiver.Symmetrify.of.obj v) = ∑ i : Q, ∑ a : i ⟶ v, headBacktrackElem k a + ∑ j : Q, ∑ a : v ⟶ j, tailBacktrackElem k a

The signless relator of a symmetrified quiver at v is the sum of the head backtracks a a* of the arrows into v and the tail backtracks a* a of the arrows out of v: the local preprojective relator with its sign removed.

theorem TauCeti.gaugedPreprojectiveRelator_bipartite_eq_sum_smul (k : Type w) {Q : Type u} [CommRing k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] {c : Q → Bool} (hc : ∀ ⦃i j : Q⦄ (a : i ⟶ j), c i ≠ c j) : (gaugedPreprojectiveRelator k fun (x j : Q) (x_1 : x ⟶ j) => if c j = true then 1 else -1) = ∑ v : Q, (if c v = true then 1 else -1) • signlessPreprojectiveRelator k (Quiver.Symmetrify.of.obj v)

The colour-signed preprojective relator is a signed sum of signless relators. Label each arrow of Q by 1 or -1 according to the colour of its head. When the colours differ at the two ends of every arrow, the gauged preprojective relator for that labelling is ∑_v ±s_v, the sign at v being 1 or -1 according to the colour of v.

theorem TauCeti.gaugedPreprojectiveRelator_bipartite_vertexCorner_eq_smul (k : Type w) {Q : Type u} [CommRing k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] {c : Q → Bool} (hc : ∀ ⦃i j : Q⦄ (a : i ⟶ j), c i ≠ c j) (v : Q) : (PathAlgebra.vertexIdempotent k (Quiver.Symmetrify.of.obj v) * gaugedPreprojectiveRelator k fun (x j : Q) (x_1 : x ⟶ j) => if c j = true then 1 else -1) * PathAlgebra.vertexIdempotent k (Quiver.Symmetrify.of.obj v) = (if c v = true then 1 else -1) • signlessPreprojectiveRelator k (Quiver.Symmetrify.of.obj v)

The corner at v of the colour-signed preprojective relator is ±s_v.

theorem TauCeti.symmetrifySignlessPreprojectiveIdeal_eq_gaugedPreprojectiveIdeal (k : Type w) {Q : Type u} [CommRing k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] {c : Q → Bool} (hc : ∀ ⦃i j : Q⦄ (a : i ⟶ j), c i ≠ c j) : signlessPreprojectiveIdeal k (Quiver.Symmetrify Q) = gaugedPreprojectiveIdeal k fun (x j : Q) (x_1 : x ⟶ j) => if c j = true then 1 else -1

For a bipartite quiver the signless relation and the colour-signed preprojective relation generate the same ideal.

noncomputable def TauCeti.symmetrifySignlessPreprojectiveAlgebraEquiv (k : Type w) {Q : Type u} [CommRing k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] {c : Q → Bool} (hc : ∀ ⦃i j : Q⦄ (a : i ⟶ j), c i ≠ c j) : signlessPreprojectiveAlgebra k (Quiver.Symmetrify Q) ≃ₐ[k] preprojectiveAlgebra k Q

The signless algebra of a bipartite quiver is its preprojective algebra. For a colouring c of the vertices of Q whose colours differ at the two ends of every arrow, the isomorphism multiplies each arrow of Q by 1 or -1 according to the colour of its head, and fixes the formal reverses.

Equations

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

@[simp]

theorem TauCeti.symmetrifySignlessPreprojectiveAlgebraEquiv_signlessPreprojectiveMk (k : Type w) {Q : Type u} [CommRing k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] {c : Q → Bool} (hc : ∀ ⦃i j : Q⦄ (a : i ⟶ j), c i ≠ c j) (x : pathAlgebra k (Quiver.Symmetrify Q)) : (symmetrifySignlessPreprojectiveAlgebraEquiv k hc) ((signlessPreprojectiveMk k (Quiver.Symmetrify Q)) x) = (preprojectiveMk k Q) ((PathAlgebra.rescale (doubledLabelling k fun (x j : Q) (x_1 : x ⟶ j) => if c j = true then 1 else -1)) x)

The comparison isomorphism is the explicit sign rescaling: it multiplies each arrow of Q by 1 or -1 according to the colour of its head, fixes the formal reverses, and passes to the preprojective quotient.

@[simp]

theorem TauCeti.symmetrifySignlessPreprojectiveAlgebraEquiv_symm_preprojectiveMk (k : Type w) {Q : Type u} [CommRing k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] {c : Q → Bool} (hc : ∀ ⦃i j : Q⦄ (a : i ⟶ j), c i ≠ c j) (x : pathAlgebra k (Quiver.Symmetrify Q)) : (symmetrifySignlessPreprojectiveAlgebraEquiv k hc).symm ((preprojectiveMk k Q) x) = (signlessPreprojectiveMk k (Quiver.Symmetrify Q)) ((PathAlgebra.rescale (doubledLabelling k fun (x j : Q) (x_1 : x ⟶ j) => if c j = true then 1 else -1)) x)

The inverse comparison isomorphism applies the same involutive sign rescaling to a preprojective quotient representative.

theorem TauCeti.symmetrifySignlessPreprojectiveAlgebraEquiv_signlessPreprojectiveMk_of_forall_head (k : Type w) {Q : Type u} [CommRing k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] {c : Q → Bool} (hc : ∀ ⦃i j : Q⦄ (a : i ⟶ j), c i ≠ c j) (hhead : ∀ ⦃i j : Q⦄ (a : i ⟶ j), c j = true) (x : pathAlgebra k (Quiver.Symmetrify Q)) : (symmetrifySignlessPreprojectiveAlgebraEquiv k hc) ((signlessPreprojectiveMk k (Quiver.Symmetrify Q)) x) = (preprojectiveMk k Q) x

For a source--sink orientation no rescaling is needed: if every arrow of Q ends at a vertex coloured true, the comparison isomorphism is induced by the identity of the doubled path algebra.

theorem TauCeti.symmetrifySignlessPreprojectiveAlgebraEquiv_symm_preprojectiveMk_of_forall_head (k : Type w) {Q : Type u} [CommRing k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] {c : Q → Bool} (hc : ∀ ⦃i j : Q⦄ (a : i ⟶ j), c i ≠ c j) (hhead : ∀ {i j : Q} (a : i ⟶ j), c j = true) (x : pathAlgebra k (Quiver.Symmetrify Q)) : (symmetrifySignlessPreprojectiveAlgebraEquiv k hc).symm ((preprojectiveMk k Q) x) = (signlessPreprojectiveMk k (Quiver.Symmetrify Q)) x

For a source--sink orientation, the inverse comparison isomorphism is also induced by the identity of the doubled path algebra.

Characteristic two

@[simp]

theorem TauCeti.signlessPreprojectiveRelator_eq_localPreprojectiveRelator_of_two_eq_zero (k : Type w) {Q : Type u} [CommRing k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] (h2 : 2 = 0) (v : Q) : signlessPreprojectiveRelator k (Quiver.Symmetrify.of.obj v) = localPreprojectiveRelator k v

In characteristic two the signless relator is the preprojective relator. The two differ only in the sign of the tail backtracks.

@[simp]

theorem TauCeti.signlessPreprojectiveIdeal_eq_preprojectiveIdeal_of_two_eq_zero (k : Type w) {Q : Type u} [CommRing k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] (h2 : 2 = 0) : signlessPreprojectiveIdeal k (Quiver.Symmetrify Q) = preprojectiveIdeal k Q

In characteristic two the signless and the preprojective relation ideals coincide, for every finite quiver, bipartite or not.

noncomputable def TauCeti.signlessPreprojectiveAlgebraEquivPreprojectiveOfTwoEqZero (k : Type w) {Q : Type u} [CommRing k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] (h2 : 2 = 0) : signlessPreprojectiveAlgebra k (Quiver.Symmetrify Q) ≃ₐ[k] preprojectiveAlgebra k Q

In characteristic two the signless algebra of a doubled quiver is its preprojective algebra, by the identity of the doubled path algebra.

Equations

• TauCeti.signlessPreprojectiveAlgebraEquivPreprojectiveOfTwoEqZero k h2 = Ideal.quotientEquivAlgOfEq k ⋯

@[simp]

theorem TauCeti.signlessPreprojectiveAlgebraEquivPreprojectiveOfTwoEqZero_signlessPreprojectiveMk (k : Type w) {Q : Type u} [CommRing k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] (h2 : 2 = 0) (x : pathAlgebra k (Quiver.Symmetrify Q)) : (signlessPreprojectiveAlgebraEquivPreprojectiveOfTwoEqZero k h2) ((signlessPreprojectiveMk k (Quiver.Symmetrify Q)) x) = (preprojectiveMk k Q) x

The characteristic-two comparison is induced by the identity of the doubled path algebra.

@[simp]

theorem TauCeti.signlessPreprojectiveAlgebraEquivPreprojectiveOfTwoEqZero_symm_preprojectiveMk (k : Type w) {Q : Type u} [CommRing k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] (h2 : 2 = 0) (x : pathAlgebra k (Quiver.Symmetrify Q)) : (signlessPreprojectiveAlgebraEquivPreprojectiveOfTwoEqZero k h2).symm ((preprojectiveMk k Q) x) = (signlessPreprojectiveMk k (Quiver.Symmetrify Q)) x

The inverse of the characteristic-two comparison is also induced by the identity of the doubled path algebra.