Doubled quivers of simple graphs

The doubled quiver of a simple graph has the graph's vertices and one arrow in each direction over every edge. Since adjacency in a simple graph is a proposition, this quiver is thin: it has no loops or parallel arrows. Its canonical arrow reversal comes from symmetry of adjacency.

This file relates the quiver API to Mathlib's graph API. Total arrows are identified with graph darts, stars and costars are identified with neighbor sets, and their cardinalities recover the adjacency matrix, vertex degrees, and twice the number of edges. A graph homomorphism acts on doubled quivers by a reversal-preserving prefunctor, and a graph isomorphism gives mutually inverse prefunctors.

Main definitions

• TauCeti.DoubledQuiver: the doubled quiver attached to a simple graph.
• TauCeti.DoubledQuiver.totalArrowEquivDart: its arrows are the graph's darts.
• TauCeti.DoubledQuiver.map: the prefunctor induced by a graph homomorphism.

Main results

• TauCeti.DoubledQuiver.card_hom_eq_adjMatrix: arrow counts are adjacency-matrix entries.
• TauCeti.DoubledQuiver.card_totalArrow_eq_twice_card_edges: every edge gives two arrows.
• TauCeti.DoubledQuiver.map_toHom_comp_symm_toHom and TauCeti.DoubledQuiver.map_symm_toHom_comp_toHom: graph isomorphisms induce inverse prefunctors.
• TauCeti.DoubledQuiver.map_obj_bijective: a graph isomorphism relabels the doubled-quiver vertices bijectively.

References

This is the doubled-graph construction in Layer 0 of TauCetiRoadmap/ZigzagPreprojective/README.md; its interface follows the target-signature prototype in TauCetiRoadmap/ZigzagPreprojective/Suggested.lean. See Huerfano--Khovanov, A category for the adjoint representation, Section 3.

def TauCeti.DoubledQuiver {V : Type u} (_G : SimpleGraph V) : Type u

The doubled quiver of a simple graph. Its vertices are the graph's vertices, and there is one arrow i ⟶ j for every proof that i and j are adjacent.

Equations

• TauCeti.DoubledQuiver _G = V

def TauCeti.DoubledQuiver.vertex {V : Type u} (G : SimpleGraph V) (v : V) : DoubledQuiver G

Include a graph vertex into the vertex type of its doubled quiver.

Equations

• TauCeti.DoubledQuiver.vertex G v = v

def TauCeti.DoubledQuiver.vertexEquiv {V : Type u} (G : SimpleGraph V) : V ≃ DoubledQuiver G

The graph vertices and the doubled-quiver vertices are canonically equivalent.

Equations

• TauCeti.DoubledQuiver.vertexEquiv G = { toFun := TauCeti.DoubledQuiver.vertex G, invFun := fun (v : TauCeti.DoubledQuiver G) => v, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem TauCeti.DoubledQuiver.vertexEquiv_apply {V : Type u} (G : SimpleGraph V) (v : V) : (vertexEquiv G) v = vertex G v

@[simp]

theorem TauCeti.DoubledQuiver.vertexEquiv_symm_apply {V : Type u} (G : SimpleGraph V) (v : DoubledQuiver G) : vertex G ((vertexEquiv G).symm v) = v

@[simp]

theorem TauCeti.DoubledQuiver.vertexEquiv_symm_vertex {V : Type u} (G : SimpleGraph V) (v : V) : (vertexEquiv G).symm (vertex G v) = v

theorem TauCeti.DoubledQuiver.exists_eq_vertex {V : Type u} (G : SimpleGraph V) (a : DoubledQuiver G) : ∃ (v : V), a = vertex G v

Every vertex of the doubled quiver comes from a vertex of the graph.

theorem TauCeti.DoubledQuiver.vertex_injective {V : Type u} (G : SimpleGraph V) : Function.Injective (vertex G)

The vertex inclusion of a doubled quiver is injective.

@[simp]

theorem TauCeti.DoubledQuiver.vertex_inj {V : Type u} (G : SimpleGraph V) {u v : V} : vertex G u = vertex G v ↔ u = v

Two graph vertices have the same image in the doubled quiver exactly when they are equal.

@[instance_reducible]

instance TauCeti.DoubledQuiver.instQuiver {V : Type u} (G : SimpleGraph V) : Quiver (DoubledQuiver G)

Equations

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

instance TauCeti.DoubledQuiver.instIsThin {V : Type u} (G : SimpleGraph V) : Quiver.IsThin (DoubledQuiver G)

instance TauCeti.DoubledQuiver.instFinite {V : Type u} (G : SimpleGraph V) [Finite V] : Finite (DoubledQuiver G)

@[instance_reducible]

instance TauCeti.DoubledQuiver.instFintype {V : Type u} (G : SimpleGraph V) [Fintype V] : Fintype (DoubledQuiver G)

Equations

• TauCeti.DoubledQuiver.instFintype G = Fintype.ofEquiv V (TauCeti.DoubledQuiver.vertexEquiv G)

instance TauCeti.DoubledQuiver.instFiniteHom {V : Type u} (G : SimpleGraph V) (i j : DoubledQuiver G) : Finite (i ⟶ j)

@[instance_reducible]

instance TauCeti.DoubledQuiver.instFintypeHomOfDecidableRelAdj {V : Type u} (G : SimpleGraph V) [DecidableRel G.Adj] (i j : DoubledQuiver G) : Fintype (i ⟶ j)

Equations

• TauCeti.DoubledQuiver.instFintypeHomOfDecidableRelAdj G i j = id inferInstance

@[instance_reducible]

instance TauCeti.DoubledQuiver.instHasReverse {V : Type u} (G : SimpleGraph V) : Quiver.HasReverse (DoubledQuiver G)

Equations

• TauCeti.DoubledQuiver.instHasReverse G = { reverse' := fun {a b : TauCeti.DoubledQuiver G} (e : a ⟶ b) => { down := ⋯ } }

@[instance_reducible]

instance TauCeti.DoubledQuiver.instHasInvolutiveReverse {V : Type u} (G : SimpleGraph V) : Quiver.HasInvolutiveReverse (DoubledQuiver G)

Equations

• TauCeti.DoubledQuiver.instHasInvolutiveReverse G = { toHasReverse := inferInstance, inv' := ⋯ }

def TauCeti.DoubledQuiver.arrow {V : Type u} (G : SimpleGraph V) {i j : V} (h : G.Adj i j) : vertex G i ⟶ vertex G j

The arrow of the doubled quiver corresponding to an adjacency.

Equations

• TauCeti.DoubledQuiver.arrow G h = { down := ⋯ }

theorem TauCeti.DoubledQuiver.arrow_down {V : Type u} (G : SimpleGraph V) {i j : V} (h : G.Adj i j) : ⋯ = ⋯

@[simp]

theorem TauCeti.DoubledQuiver.reverse_arrow {V : Type u} (G : SimpleGraph V) {i j : V} (h : G.Adj i j) : Quiver.reverse (arrow G h) = arrow G ⋯

Reversing the arrow induced by an adjacency gives the arrow induced by symmetric adjacency.

@[simp]

theorem TauCeti.DoubledQuiver.nonempty_hom_iff {V : Type u} (G : SimpleGraph V) {i j : V} : Nonempty (vertex G i ⟶ vertex G j) ↔ G.Adj i j

There is an arrow from i to j exactly when the vertices are adjacent.

@[simp]

theorem TauCeti.DoubledQuiver.isEmpty_hom_iff {V : Type u} (G : SimpleGraph V) {i j : V} : IsEmpty (vertex G i ⟶ vertex G j) ↔ ¬G.Adj i j

The arrow type from i to j is empty exactly when the vertices are not adjacent.

@[reducible, inline]

abbrev TauCeti.DoubledQuiver.TotalArrow {V : Type u} (G : SimpleGraph V) : Type u

All arrows in the doubled quiver, with their source and target.

Equations

• TauCeti.DoubledQuiver.TotalArrow G = ((i : TauCeti.DoubledQuiver G) × (j : TauCeti.DoubledQuiver G) × (i ⟶ j))

def TauCeti.DoubledQuiver.totalArrowEquivDart {V : Type u} (G : SimpleGraph V) : TotalArrow G ≃ G.Dart

The total arrows of the doubled quiver are the oriented edges, or darts, of the graph.

Equations

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

@[simp]

theorem TauCeti.DoubledQuiver.totalArrowEquivDart_apply {V : Type u} (G : SimpleGraph V) (i j : DoubledQuiver G) (e : i ⟶ j) : (totalArrowEquivDart G) ⟨i, ⟨j, e⟩⟩ = { fst := (vertexEquiv G).symm i, snd := (vertexEquiv G).symm j, adj := ⋯ }

@[simp]

theorem TauCeti.DoubledQuiver.totalArrowEquivDart_symm_apply {V : Type u} (G : SimpleGraph V) (d : G.Dart) : (totalArrowEquivDart G).symm d = ⟨vertex G d.toProd.1, ⟨vertex G d.toProd.2, arrow G ⋯⟩⟩

def TauCeti.DoubledQuiver.reverseTotalArrow {V : Type u} (G : SimpleGraph V) (e : TotalArrow G) : TotalArrow G

Reverse a total arrow, exchanging its source and target.

Equations

• TauCeti.DoubledQuiver.reverseTotalArrow G e = ⟨e.snd.fst, ⟨e.fst, Quiver.reverse e.snd.snd⟩⟩

@[simp]

theorem TauCeti.DoubledQuiver.totalArrowEquivDart_reverse {V : Type u} (G : SimpleGraph V) (e : TotalArrow G) : (totalArrowEquivDart G) (reverseTotalArrow G e) = ((totalArrowEquivDart G) e).symm

@[simp]

theorem TauCeti.DoubledQuiver.reverseTotalArrow_reverseTotalArrow {V : Type u} (G : SimpleGraph V) (e : TotalArrow G) : reverseTotalArrow G (reverseTotalArrow G e) = e

def TauCeti.DoubledQuiver.starEquivNeighborSet {V : Type u} (G : SimpleGraph V) (v : V) : Quiver.Star (vertex G v) ≃ ↑(G.neighborSet v)

The arrows leaving a vertex are its neighbors in the graph.

Equations

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

@[instance_reducible]

noncomputable instance TauCeti.DoubledQuiver.instFintypeStarVertex {V : Type u} (G : SimpleGraph V) (v : V) [Fintype ↑(G.neighborSet v)] : Fintype (Quiver.Star (vertex G v))

The star at a doubled-quiver vertex is finite whenever its neighbor set is finite.

Equations

• TauCeti.DoubledQuiver.instFintypeStarVertex G v = Fintype.ofEquiv (↑(G.neighborSet v)) (TauCeti.DoubledQuiver.starEquivNeighborSet G v).symm

@[instance_reducible]

noncomputable instance TauCeti.DoubledQuiver.instFintypeStar {V : Type u} (G : SimpleGraph V) [(v : V) → Fintype ↑(G.neighborSet v)] (x : DoubledQuiver G) : Fintype (Quiver.Star x)

If every graph neighbor set is finite, then every star of its doubled quiver is finite.

Equations

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

@[simp]

theorem TauCeti.DoubledQuiver.starEquivNeighborSet_apply {V : Type u} (G : SimpleGraph V) (v : V) (e : Quiver.Star (vertex G v)) : (starEquivNeighborSet G v) e = ⟨(vertexEquiv G).symm e.fst, ⋯⟩

@[simp]

theorem TauCeti.DoubledQuiver.starEquivNeighborSet_symm_apply {V : Type u} (G : SimpleGraph V) (v : V) (w : ↑(G.neighborSet v)) : (starEquivNeighborSet G v).symm w = ⟨vertex G ↑w, arrow G ⋯⟩

def TauCeti.DoubledQuiver.costarEquivNeighborSet {V : Type u} (G : SimpleGraph V) (v : V) : Quiver.Costar (vertex G v) ≃ ↑(G.neighborSet v)

The arrows entering a vertex are also its neighbors in the graph.

Equations

• TauCeti.DoubledQuiver.costarEquivNeighborSet G v = (Quiver.starEquivCostar (TauCeti.DoubledQuiver.vertex G v)).symm.trans (TauCeti.DoubledQuiver.starEquivNeighborSet G v)

@[simp]

theorem TauCeti.DoubledQuiver.costarEquivNeighborSet_apply {V : Type u} (G : SimpleGraph V) (v : V) (e : Quiver.Costar (vertex G v)) : (costarEquivNeighborSet G v) e = ⟨(vertexEquiv G).symm e.fst, ⋯⟩

@[simp]

theorem TauCeti.DoubledQuiver.costarEquivNeighborSet_symm_apply {V : Type u} (G : SimpleGraph V) (v : V) (w : ↑(G.neighborSet v)) : (costarEquivNeighborSet G v).symm w = ⟨vertex G ↑w, arrow G ⋯⟩

@[simp]

theorem TauCeti.DoubledQuiver.card_hom_eq_adjMatrix {V : Type u} (G : SimpleGraph V) [DecidableRel G.Adj] (i j : V) : Fintype.card (vertex G i ⟶ vertex G j) = SimpleGraph.adjMatrix ℕ G i j

The number of doubled-quiver arrows from i to j is the corresponding adjacency-matrix entry.

theorem TauCeti.DoubledQuiver.card_star_eq_degree {V : Type u} (G : SimpleGraph V) (v : V) [Fintype ↑(G.neighborSet v)] : Nat.card (Quiver.Star (vertex G v)) = G.degree v

The number of doubled-quiver arrows leaving a vertex is its degree in the graph.

theorem TauCeti.DoubledQuiver.card_costar_eq_degree {V : Type u} (G : SimpleGraph V) (v : V) [Fintype ↑(G.neighborSet v)] : Nat.card (Quiver.Costar (vertex G v)) = G.degree v

The number of doubled-quiver arrows entering a vertex is its degree in the graph.

theorem TauCeti.DoubledQuiver.card_totalArrow_eq_twice_card_edges {V : Type u} (G : SimpleGraph V) [Fintype V] [DecidableRel G.Adj] : Fintype.card (TotalArrow G) = 2 * G.edgeFinset.card

The total number of doubled-quiver arrows is twice the number of graph edges.

def TauCeti.DoubledQuiver.map {V : Type u} {G : SimpleGraph V} {W : Type v} {H : SimpleGraph W} (f : G →g H) : DoubledQuiver G ⥤q DoubledQuiver H

A graph homomorphism induces a prefunctor of doubled quivers.

Equations

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

@[simp]

theorem TauCeti.DoubledQuiver.map_obj {V : Type u} {G : SimpleGraph V} {W : Type v} {H : SimpleGraph W} (f : G →g H) (i : V) : (map f).obj (vertex G i) = vertex H (f i)

@[simp]

theorem TauCeti.DoubledQuiver.map_arrow {V : Type u} {G : SimpleGraph V} {W : Type v} {H : SimpleGraph W} (f : G →g H) {i j : V} (h : G.Adj i j) : (map f).map (arrow G h) = Quiver.homOfEq (arrow H ⋯) ⋯ ⋯

instance TauCeti.DoubledQuiver.mapMapReverse {V : Type u} {G : SimpleGraph V} {W : Type v} {H : SimpleGraph W} (f : G →g H) : (map f).MapReverse

The doubled-quiver prefunctor induced by a graph homomorphism commutes with arrow reversal.

@[simp]

theorem TauCeti.DoubledQuiver.map_id {V : Type u} {G : SimpleGraph V} : map SimpleGraph.Hom.id = 𝟭q (DoubledQuiver G)

Mapping the identity graph homomorphism gives the identity doubled-quiver prefunctor.

theorem TauCeti.DoubledQuiver.map_comp {V : Type u} {G : SimpleGraph V} {W : Type v} {X : Type u_1} {H : SimpleGraph W} {K : SimpleGraph X} (f : G →g H) (g : H →g K) : map (g.comp f) = map f ⋙q map g

The doubled-quiver map preserves composition of graph homomorphisms.

@[simp]

theorem TauCeti.DoubledQuiver.map_refl {V : Type u} {G : SimpleGraph V} : map SimpleGraph.Iso.refl.toHom = 𝟭q (DoubledQuiver G)

Mapping the identity graph isomorphism gives the identity doubled-quiver prefunctor.

theorem TauCeti.DoubledQuiver.map_trans {V : Type u} {G : SimpleGraph V} {W : Type v} {X : Type u_1} {H : SimpleGraph W} {K : SimpleGraph X} (e : G ≃g H) (f : H ≃g K) : map (SimpleGraph.Iso.toHom (RelIso.trans e f)) = map e.toHom ⋙q map f.toHom

Mapping a composite graph isomorphism composes the doubled-quiver prefunctors.

@[simp]

theorem TauCeti.DoubledQuiver.map_toHom_comp_symm_toHom {V : Type u} {G : SimpleGraph V} {W : Type v} {H : SimpleGraph W} (f : G ≃g H) : map f.toHom ⋙q map f.symm.toHom = 𝟭q (DoubledQuiver G)

Relabelling a graph and then undoing the relabelling is the identity doubled-quiver map.

@[simp]

theorem TauCeti.DoubledQuiver.map_symm_toHom_comp_toHom {V : Type u} {G : SimpleGraph V} {W : Type v} {H : SimpleGraph W} (f : G ≃g H) : map f.symm.toHom ⋙q map f.toHom = 𝟭q (DoubledQuiver H)

Undoing a graph relabelling and then applying it is the identity doubled-quiver map.

theorem TauCeti.DoubledQuiver.map_obj_bijective {V : Type u} {G : SimpleGraph V} {W : Type v} {H : SimpleGraph W} (e : G ≃g H) : Function.Bijective (map e.toHom).obj

A graph isomorphism relabels the vertices of the doubled quiver bijectively.