Symmetrified quivers

This file supplies general infrastructure for Mathlib's Quiver.Symmetrify construction.

Main results

• TauCeti.symmetrify_of_obj: the doubling inclusion is the identity on vertices.

References

This file supplies a prerequisite for Layer 4 of TauCetiRoadmap/ZigzagPreprojective/README.md.

instance TauCeti.instFiniteSymmetrify (Q : Type u) [Finite Q] : Finite (Quiver.Symmetrify Q)

Typeclass search does not unfold the Symmetrify type synonym to reuse Finite Q.

@[instance_reducible]

instance TauCeti.instDecidableEqSymmetrify (Q : Type u) [DecidableEq Q] : DecidableEq (Quiver.Symmetrify Q)

Typeclass search does not unfold the Symmetrify type synonym to reuse DecidableEq Q.

Equations

• TauCeti.instDecidableEqSymmetrify Q = TauCeti.instDecidableEqSymmetrify._aux_1 Q

@[instance_reducible]

instance TauCeti.instFintypeSymmetrify (Q : Type u) [Fintype Q] : Fintype (Quiver.Symmetrify Q)

Typeclass search does not unfold the Symmetrify type synonym to reuse Fintype Q.

Equations

• TauCeti.instFintypeSymmetrify Q = TauCeti.instFintypeSymmetrify._aux_1 Q

@[instance_reducible]

instance TauCeti.instFintypeSymmetrifyHom (Q : Type u) [Quiver Q] [(i j : Q) → Fintype (i ⟶ j)] (x y : Quiver.Symmetrify Q) : Fintype (x ⟶ y)

The arrows of the doubled quiver between two vertices are the arrows of Q in either direction, so there are finitely many whenever Q has finitely many between each pair.

Equations

• TauCeti.instFintypeSymmetrifyHom Q x y = { elems := Finset.univ.disjSum Finset.univ, complete := ⋯ }

theorem TauCeti.symmetrify_of_obj {Q : Type u} [Quiver Q] (x : Q) : Quiver.Symmetrify.of.obj x = x

The inclusion Quiver.Symmetrify.of of a quiver in its doubled quiver is the identity on vertices. Deliberately not a simp lemma: the two vertex types are definitionally equal, so rewriting Quiver.Symmetrify.of away erases the only record of which of the two quiver structures a vertex was meant to carry.

theorem TauCeti.symmetrify_of_obj_bijective {Q : Type u} [Quiver Q] : Function.Bijective Quiver.Symmetrify.of.obj

The inclusion Quiver.Symmetrify.of of a quiver in its doubled quiver is the identity on vertices, hence bijective on them.