Signless and preprojective relations of an oriented graph

A two-colouring of a simple graph gives a source--sink orientation by directing every edge toward its true endpoint. Symmetrifying any orientation of the graph recovers the doubled quiver. Under that identification, the signless relation of the graph becomes the signless relation of the symmetrified orientation, and rescaling each arrow of the orientation by the sign of the colour of its head identifies the signless preprojective algebra of the doubled graph with the additive preprojective algebra of the orientation.

For the source--sink orientation, every arrow of the oriented quiver goes from a false vertex to a true vertex, so the signless/preprojective comparison needs no further arrow rescaling. Thus the signless preprojective algebra of the doubled graph is explicitly isomorphic to the additive preprojective algebra of its source--sink orientation by the identity of the symmetrified path algebra.

Conversely, suppose that a unit gauge makes every corner of the preprojective relator a scalar multiple of the corresponding signless relator. The comparison scalars change sign along every edge. A non-bipartite graph has an odd closed walk, which would therefore force 2 = 0. Over a coefficient ring in which 2 ≠ 0, a non-bipartite graph therefore admits no such comparison, for any choice of orientation.

Main definitions

• SimpleGraph.Coloring.sourceSink: the orientation directed toward colour true.
• TauCeti.DoubledQuiver.orientationPathAlgebraEquiv: the path-algebra comparison induced by restoring an orientation.
• TauCeti.DoubledQuiver.orientationSignlessPreprojectiveAlgebraEquiv: the induced comparison between the signless algebra of the doubled graph and the signless algebra of a symmetrified orientation.
• SimpleGraph.Coloring.signlessPreprojectiveAlgebraEquiv and SimpleGraph.IsBipartite.signlessPreprojectiveAlgebraEquiv: the comparison between the graph's signless algebra and the preprojective algebra of any orientation.
• SimpleGraph.Coloring.sourceSinkSignlessPreprojectiveAlgebraEquiv: the comparison between the graph's signless algebra and the preprojective algebra of the source--sink orientation.
• TauCeti.DoubledQuiver.Orientation.not_exists_forall_vertexCorner_eq_smul_of_not_isBipartite: over coefficients with 2 ≠ 0, a non-bipartite graph admits no cornerwise unit-gauge comparison.

References

S. Huerfano and M. Khovanov, A category for the adjoint representation, Section 3, https://arxiv.org/abs/math/0002060, for the signless relation and its comparison with the preprojective relation of a bipartite graph.

noncomputable def TauCeti.DoubledQuiver.orientationPathAlgebraEquiv {V : Type u} {G : SimpleGraph V} (o : Orientation G) (k : Type w) [CommSemiring k] [Finite V] : pathAlgebra k (DoubledQuiver G) ≃ₐ[k] pathAlgebra k (Quiver.Symmetrify (OrientedQuiver G o))

The path-algebra isomorphism which restores an orientation of a graph. It sends every doubled arrow to the corresponding positive or negative arrow in the symmetrification.

theorem TauCeti.DoubledQuiver.orientationPathAlgebraEquiv_apply {V : Type u} {G : SimpleGraph V} (o : Orientation G) (k : Type w) [CommSemiring k] [Finite V] (x : pathAlgebra k (DoubledQuiver G)) : (orientationPathAlgebraEquiv o k) x = (PathAlgebra.mapAlgHom k (unsymmetrifyMap G o) ⋯) x

The orientation path-algebra comparison is induced by the inverse orientation prefunctor.

@[simp]

theorem TauCeti.DoubledQuiver.orientationPathAlgebraEquiv_ofPath {V : Type u} {G : SimpleGraph V} (o : Orientation G) (k : Type w) [CommSemiring k] [Finite V] (x : Quiver.TotalPath (DoubledQuiver G)) : (orientationPathAlgebraEquiv o k) (PathAlgebra.ofPath x) = PathAlgebra.ofPath ((unsymmetrifyMap G o).mapTotalPath x)

The orientation path-algebra comparison sends a basis path to the path obtained by restoring the orientation of each arrow.

theorem TauCeti.DoubledQuiver.orientationPathAlgebraEquiv_symm_apply {V : Type u} {G : SimpleGraph V} (o : Orientation G) (k : Type w) [CommSemiring k] [Finite V] (x : pathAlgebra k (Quiver.Symmetrify (OrientedQuiver G o))) : (orientationPathAlgebraEquiv o k).symm x = (PathAlgebra.mapAlgHom k (symmetrifyMap G o) ⋯) x

The inverse orientation path-algebra comparison is induced by forgetting the orientation.

@[simp]

theorem TauCeti.DoubledQuiver.orientationPathAlgebraEquiv_symm_ofPath {V : Type u} {G : SimpleGraph V} (o : Orientation G) (k : Type w) [CommSemiring k] [Finite V] (x : Quiver.TotalPath (Quiver.Symmetrify (OrientedQuiver G o))) : (orientationPathAlgebraEquiv o k).symm (PathAlgebra.ofPath x) = PathAlgebra.ofPath ((symmetrifyMap G o).mapTotalPath x)

The inverse path-algebra comparison sends a basis path to the path obtained by forgetting the chosen orientation of each arrow.

@[simp]

theorem TauCeti.DoubledQuiver.orientationPathAlgebraEquiv_signlessPreprojectiveRelator {V : Type u} {G : SimpleGraph V} (o : Orientation G) (k : Type w) [CommSemiring k] [Finite V] (i : DoubledQuiver G) : (orientationPathAlgebraEquiv o k) (signlessPreprojectiveRelator k i) = signlessPreprojectiveRelator k ((unsymmetrifyMap G o).obj i)

Restoring an orientation carries each signless graph relator to the signless relator at the corresponding vertex of the symmetrified oriented quiver.

@[simp]

theorem TauCeti.DoubledQuiver.orientationPathAlgebraEquiv_symm_signlessPreprojectiveRelator {V : Type u} {G : SimpleGraph V} (o : Orientation G) (k : Type w) [CommSemiring k] [Finite V] (i : Quiver.Symmetrify (OrientedQuiver G o)) : (orientationPathAlgebraEquiv o k).symm (signlessPreprojectiveRelator k i) = signlessPreprojectiveRelator k ((symmetrifyMap G o).obj i)

The inverse path-algebra comparison also carries signless relators to signless relators.

Transporting the signless quotient

noncomputable def TauCeti.DoubledQuiver.orientationSignlessPreprojectiveAlgebraEquiv {V : Type u} {G : SimpleGraph V} (o : Orientation G) (k : Type w) [CommRing k] [Finite V] : signlessPreprojectiveAlgebra k (DoubledQuiver G) ≃ₐ[k] signlessPreprojectiveAlgebra k (Quiver.Symmetrify (OrientedQuiver G o))

Restoring an orientation identifies the signless algebra of the doubled graph with the signless algebra of the symmetrified oriented quiver.

@[simp]

theorem TauCeti.DoubledQuiver.orientationSignlessPreprojectiveAlgebraEquiv_signlessPreprojectiveMk {V : Type u} {G : SimpleGraph V} (o : Orientation G) (k : Type w) [CommRing k] [Finite V] (x : pathAlgebra k (DoubledQuiver G)) : (orientationSignlessPreprojectiveAlgebraEquiv o k) ((signlessPreprojectiveMk k (DoubledQuiver G)) x) = (signlessPreprojectiveMk k (Quiver.Symmetrify (OrientedQuiver G o))) ((orientationPathAlgebraEquiv o k) x)

The signless-quotient comparison is induced by the path-algebra comparison.

@[simp]

theorem TauCeti.DoubledQuiver.orientationSignlessPreprojectiveAlgebraEquiv_symm_signlessPreprojectiveMk {V : Type u} {G : SimpleGraph V} (o : Orientation G) (k : Type w) [CommRing k] [Finite V] (x : pathAlgebra k (Quiver.Symmetrify (OrientedQuiver G o))) : (orientationSignlessPreprojectiveAlgebraEquiv o k).symm ((signlessPreprojectiveMk k (Quiver.Symmetrify (OrientedQuiver G o))) x) = (signlessPreprojectiveMk k (DoubledQuiver G)) ((orientationPathAlgebraEquiv o k).symm x)

The inverse signless-quotient comparison is induced by the inverse path-algebra comparison.

theorem TauCeti.DoubledQuiver.preprojectiveMk_ofPath_eq_zero_of_signless {V : Type u} {G : SimpleGraph V} (o : Orientation G) (k : Type w) [CommRing k] [Finite V] {c : OrientedQuiver G o → Bool} (hc : ∀ ⦃i j : OrientedQuiver G o⦄ (a : i ⟶ j), c i ≠ c j) (x : Quiver.TotalPath (Quiver.Symmetrify (OrientedQuiver G o))) (hx : (signlessPreprojectiveMk k (DoubledQuiver G)) (PathAlgebra.ofPath ((symmetrifyMap G o).mapTotalPath x)) = 0) : (preprojectiveMk k (OrientedQuiver G o)) (PathAlgebra.ofPath x) = 0

Vanishing of a path in the signless algebra of a doubled graph transfers to the preprojective algebra of any orientation when the graph is bipartite.

def SimpleGraph.Coloring.orientedColor {V : Type u} {G : SimpleGraph V} (C : G.Coloring Bool) (o : TauCeti.DoubledQuiver.Orientation G) (i : TauCeti.DoubledQuiver.OrientedQuiver G o) : Bool

The colour of a vertex of an oriented quiver, transported from the graph.

@[simp]

theorem SimpleGraph.Coloring.orientedColor_vertex {V : Type u} {G : SimpleGraph V} (C : G.Coloring Bool) (o : TauCeti.DoubledQuiver.Orientation G) (i : V) : C.orientedColor o (TauCeti.DoubledQuiver.OrientedQuiver.vertex G o i) = C i

The colour on an oriented quiver is the original graph colouring.

theorem SimpleGraph.Coloring.orientedColor_ne {V : Type u} {G : SimpleGraph V} (C : G.Coloring Bool) (o : TauCeti.DoubledQuiver.Orientation G) {i j : TauCeti.DoubledQuiver.OrientedQuiver G o} (a : i ⟶ j) : C.orientedColor o i ≠ C.orientedColor o j

Every arrow of an orientation of a two-coloured graph has differently coloured endpoints.

theorem SimpleGraph.Coloring.orientedColor_sourceSink_target_eq_true {V : Type u} {G : SimpleGraph V} (C : G.Coloring Bool) {i j : TauCeti.DoubledQuiver.OrientedQuiver G C.sourceSink} (a : i ⟶ j) : C.orientedColor C.sourceSink j = true

Every arrow of the source--sink orientation ends at a vertex of colour true.

The preprojective comparison

noncomputable def SimpleGraph.Coloring.signlessPreprojectiveAlgebraEquiv {V : Type u} {G : SimpleGraph V} (C : G.Coloring Bool) (k : Type w) [CommRing k] [Finite V] (o : TauCeti.DoubledQuiver.Orientation G) : TauCeti.signlessPreprojectiveAlgebra k (TauCeti.DoubledQuiver G) ≃ₐ[k] TauCeti.preprojectiveAlgebra k (TauCeti.DoubledQuiver.OrientedQuiver G o)

The signless algebra of a two-coloured graph is isomorphic to the additive preprojective algebra of any of its orientations. The isomorphism identifies the doubled quiver with the symmetrification of the oriented graph and then rescales each arrow by the sign of the colour of its head.

@[simp]

theorem SimpleGraph.Coloring.signlessPreprojectiveAlgebraEquiv_signlessPreprojectiveMk {V : Type u} {G : SimpleGraph V} (C : G.Coloring Bool) (k : Type w) [CommRing k] [Finite V] (o : TauCeti.DoubledQuiver.Orientation G) (x : TauCeti.pathAlgebra k (TauCeti.DoubledQuiver G)) : (C.signlessPreprojectiveAlgebraEquiv k o) ((TauCeti.signlessPreprojectiveMk k (TauCeti.DoubledQuiver G)) x) = (TauCeti.preprojectiveMk k (TauCeti.DoubledQuiver.OrientedQuiver G o)) ((TauCeti.PathAlgebra.rescale (TauCeti.doubledLabelling k fun (x j : TauCeti.DoubledQuiver.OrientedQuiver G o) (x_1 : x ⟶ j) => if C.orientedColor o j = true then 1 else -1)) ((TauCeti.DoubledQuiver.orientationPathAlgebraEquiv o k) x))

The bipartite comparison for an arbitrary orientation sends a doubled-path-algebra class through the orientation identification and the head-colour sign rescaling.

theorem SimpleGraph.Coloring.signlessPreprojectiveAlgebraEquiv_vertexIdempotent {V : Type u} {G : SimpleGraph V} (C : G.Coloring Bool) (k : Type w) [CommRing k] [Finite V] (o : TauCeti.DoubledQuiver.Orientation G) (i : V) : (C.signlessPreprojectiveAlgebraEquiv k o) ((TauCeti.signlessPreprojectiveMk k (TauCeti.DoubledQuiver G)) (TauCeti.PathAlgebra.vertexIdempotent k (TauCeti.DoubledQuiver.vertex G i))) = (TauCeti.preprojectiveMk k (TauCeti.DoubledQuiver.OrientedQuiver G o)) (TauCeti.PathAlgebra.vertexIdempotent k (Quiver.Symmetrify.of.obj (TauCeti.DoubledQuiver.OrientedQuiver.vertex G o i)))

The bipartite comparison preserves the vertex idempotents under the identification of graph vertices with vertices of the symmetrified orientation.

theorem SimpleGraph.Coloring.signlessPreprojectiveAlgebraEquiv_mem_preprojectiveGrade {V : Type u} {G : SimpleGraph V} (C : G.Coloring Bool) (k : Type w) [CommRing k] [Finite V] (o : TauCeti.DoubledQuiver.Orientation G) {n : ℕ} {x : TauCeti.signlessPreprojectiveAlgebra k (TauCeti.DoubledQuiver G)} (hx : x ∈ TauCeti.signlessPreprojectiveGrade k (TauCeti.DoubledQuiver G) n) : (C.signlessPreprojectiveAlgebraEquiv k o) x ∈ TauCeti.preprojectiveGrade k (TauCeti.DoubledQuiver.OrientedQuiver G o) n

The bipartite comparison preserves every path-length graded piece: restoring an orientation and rescaling arrows both preserve degree.

@[simp]

theorem SimpleGraph.Coloring.signlessPreprojectiveAlgebraEquiv_symm_preprojectiveMk {V : Type u} {G : SimpleGraph V} (C : G.Coloring Bool) (k : Type w) [CommRing k] [Finite V] (o : TauCeti.DoubledQuiver.Orientation G) (x : TauCeti.pathAlgebra k (Quiver.Symmetrify (TauCeti.DoubledQuiver.OrientedQuiver G o))) : (C.signlessPreprojectiveAlgebraEquiv k o).symm ((TauCeti.preprojectiveMk k (TauCeti.DoubledQuiver.OrientedQuiver G o)) x) = (TauCeti.signlessPreprojectiveMk k (TauCeti.DoubledQuiver G)) ((TauCeti.DoubledQuiver.orientationPathAlgebraEquiv o k).symm ((TauCeti.PathAlgebra.rescale (TauCeti.doubledLabelling k fun (x j : TauCeti.DoubledQuiver.OrientedQuiver G o) (x_1 : x ⟶ j) => if C.orientedColor o j = true then 1 else -1)) x))

The inverse bipartite comparison for an arbitrary orientation rescales by the head-colour sign and applies the inverse orientation path-algebra identification.

noncomputable def SimpleGraph.Coloring.sourceSinkSignlessPreprojectiveAlgebraEquiv {V : Type u} {G : SimpleGraph V} (C : G.Coloring Bool) (k : Type w) [CommRing k] [Finite V] : TauCeti.signlessPreprojectiveAlgebra k (TauCeti.DoubledQuiver G) ≃ₐ[k] TauCeti.preprojectiveAlgebra k (TauCeti.DoubledQuiver.OrientedQuiver G C.sourceSink)

The signless algebra of a bipartite graph is the additive preprojective algebra of its source--sink orientation. The isomorphism first identifies the doubled quiver with the symmetrification of the oriented graph; no further arrow rescaling is needed.

@[simp]

theorem SimpleGraph.Coloring.sourceSinkSignlessPreprojectiveAlgebraEquiv_signlessPreprojectiveMk {V : Type u} {G : SimpleGraph V} (C : G.Coloring Bool) (k : Type w) [CommRing k] [Finite V] (x : TauCeti.pathAlgebra k (TauCeti.DoubledQuiver G)) : (C.sourceSinkSignlessPreprojectiveAlgebraEquiv k) ((TauCeti.signlessPreprojectiveMk k (TauCeti.DoubledQuiver G)) x) = (TauCeti.preprojectiveMk k (TauCeti.DoubledQuiver.OrientedQuiver G C.sourceSink)) ((TauCeti.DoubledQuiver.orientationPathAlgebraEquiv C.sourceSink k) x)

The bipartite comparison sends the class of a doubled-path-algebra element to its image under the source--sink identification, followed by the standard preprojective quotient map.

@[simp]

theorem SimpleGraph.Coloring.sourceSinkSignlessPreprojectiveAlgebraEquiv_symm_preprojectiveMk {V : Type u} {G : SimpleGraph V} (C : G.Coloring Bool) (k : Type w) [CommRing k] [Finite V] (x : TauCeti.pathAlgebra k (Quiver.Symmetrify (TauCeti.DoubledQuiver.OrientedQuiver G C.sourceSink))) : (C.sourceSinkSignlessPreprojectiveAlgebraEquiv k).symm ((TauCeti.preprojectiveMk k (TauCeti.DoubledQuiver.OrientedQuiver G C.sourceSink)) x) = (TauCeti.signlessPreprojectiveMk k (TauCeti.DoubledQuiver G)) ((TauCeti.DoubledQuiver.orientationPathAlgebraEquiv C.sourceSink k).symm x)

The inverse bipartite comparison sends a preprojective representative through the inverse source--sink path-algebra identification.

noncomputable def SimpleGraph.IsBipartite.coloringBool {V : Type u} {G : SimpleGraph V} (hG : G.IsBipartite) : G.Coloring Bool

A two-colouring of a bipartite graph, valued in Bool.

noncomputable def SimpleGraph.IsBipartite.signlessPreprojectiveAlgebraEquiv {V : Type u} {G : SimpleGraph V} (hG : G.IsBipartite) (k : Type w) [CommRing k] [Finite V] (o : TauCeti.DoubledQuiver.Orientation G) : TauCeti.signlessPreprojectiveAlgebra k (TauCeti.DoubledQuiver G) ≃ₐ[k] TauCeti.preprojectiveAlgebra k (TauCeti.DoubledQuiver.OrientedQuiver G o)

The signless preprojective algebra of a bipartite graph is isomorphic to the additive preprojective algebra of any of its orientations.

@[simp]

theorem SimpleGraph.IsBipartite.signlessPreprojectiveAlgebraEquiv_signlessPreprojectiveMk {V : Type u} {G : SimpleGraph V} (hG : G.IsBipartite) (k : Type w) [CommRing k] [Finite V] (o : TauCeti.DoubledQuiver.Orientation G) (x : TauCeti.pathAlgebra k (TauCeti.DoubledQuiver G)) : (hG.signlessPreprojectiveAlgebraEquiv k o) ((TauCeti.signlessPreprojectiveMk k (TauCeti.DoubledQuiver G)) x) = (TauCeti.preprojectiveMk k (TauCeti.DoubledQuiver.OrientedQuiver G o)) ((TauCeti.PathAlgebra.rescale (TauCeti.doubledLabelling k fun (x j : TauCeti.DoubledQuiver.OrientedQuiver G o) (x_1 : x ⟶ j) => if hG.coloringBool.orientedColor o j = true then 1 else -1)) ((TauCeti.DoubledQuiver.orientationPathAlgebraEquiv o k) x))

The bipartite comparison sends a doubled-path-algebra class through the orientation identification and the chosen two-colouring's head-colour sign rescaling.

@[simp]

theorem SimpleGraph.IsBipartite.signlessPreprojectiveAlgebraEquiv_symm_preprojectiveMk {V : Type u} {G : SimpleGraph V} (hG : G.IsBipartite) (k : Type w) [CommRing k] [Finite V] (o : TauCeti.DoubledQuiver.Orientation G) (x : TauCeti.pathAlgebra k (Quiver.Symmetrify (TauCeti.DoubledQuiver.OrientedQuiver G o))) : (hG.signlessPreprojectiveAlgebraEquiv k o).symm ((TauCeti.preprojectiveMk k (TauCeti.DoubledQuiver.OrientedQuiver G o)) x) = (TauCeti.signlessPreprojectiveMk k (TauCeti.DoubledQuiver G)) ((TauCeti.DoubledQuiver.orientationPathAlgebraEquiv o k).symm ((TauCeti.PathAlgebra.rescale (TauCeti.doubledLabelling k fun (x j : TauCeti.DoubledQuiver.OrientedQuiver G o) (x_1 : x ⟶ j) => if hG.coloringBool.orientedColor o j = true then 1 else -1)) x))

The inverse bipartite comparison rescales by the chosen two-colouring's head-colour sign and applies the inverse orientation path-algebra identification.

The non-bipartite obstruction

theorem TauCeti.DoubledQuiver.Orientation.not_exists_forall_vertexCorner_eq_smul_of_not_isBipartite {V : Type u} {G : SimpleGraph V} (o : Orientation G) (k : Type w) [CommRing k] [Finite V] (hG : ¬G.IsBipartite) {ε : ⦃i j : OrientedQuiver G o⦄ → (i ⟶ j) → k} (hε : ∀ ⦃i j : OrientedQuiver G o⦄ (a : i ⟶ j), IsUnit (ε a)) (h2 : 2 ≠ 0) : ¬∃ (c : OrientedQuiver G o → k), ∀ (v : OrientedQuiver G o), doubledVertexIdempotent k v * gaugedPreprojectiveRelator k ε * doubledVertexIdempotent k v = c v • signlessPreprojectiveRelator k (Quiver.Symmetrify.of.obj v)

A non-bipartite graph admits no cornerwise signless comparison. For any orientation of a finite non-bipartite simple graph, when 2 ≠ 0, no unit gauge makes every corner of the gauged preprojective relator a scalar multiple of the corresponding signless relator.