Reorienting a quiver

A Bool-valued labelling σ of the arrows of a quiver Q specifies a change of orientation: this file builds the quiver TauCeti.Reorient Q σ, whose arrows are those of Q with the ones labelled true turned around.

The two doubled quivers Quiver.Symmetrify (Reorient Q σ) and Quiver.Symmetrify Q carry exactly the same arrows, distributed differently between an arrow and its formal reverse. That is the content of TauCeti.reorientSymmetrify and TauCeti.reorientSymmetrifyInv, mutually inverse prefunctors which are the identity on vertices and commute with reversal. They are the identification along which a construction on doubled quivers -- the additive preprojective algebra -- is compared across a change of orientation.

Main definitions

• TauCeti.Reorient: the quiver Q with the arrows labelled true by σ turned around.
• TauCeti.reorientHomEquiv: the identification of a hom set of Reorient Q σ with the two subtypes of hom sets of Q it is built from, together with TauCeti.reorientHom_induction_on the general elimination interface for a reoriented arrow.
• TauCeti.reorientSymmetrify and TauCeti.reorientSymmetrifyInv: the two prefunctors between the doubled quivers.

Main results

• TauCeti.reorientSymmetrify_comp_reorientSymmetrifyInv and TauCeti.reorientSymmetrifyInv_comp_reorientSymmetrify: the two prefunctors are inverse, so the two doubled quivers are isomorphic.
• TauCeti.reorientSymmetrify_map_reverse: the comparison commutes with arrow reversal.

Implementation notes

Reorient Q σ is a semireducible type synonym for Q, following Quiver.Symmetrify: were it reducible, instance search would unfold it and replace the reoriented quiver structure by that of Q. Its arrows i ⟶ j are the disjoint union of the arrows i ⟶ j of Q which σ leaves alone and the arrows j ⟶ i of Q which σ turns around, so a hom set of the doubled quiver Symmetrify (Reorient Q σ) splits into four pieces. Sorting an arrow of Symmetrify Q into those four pieces is what TauCeti.reorientSymmetrifyInv does, and it is why that prefunctor, unlike its inverse, is defined by a case distinction on the value of σ.

Turning around a single arrow is the special case where σ is supported on one arrow; allowing an arbitrary σ performs an arbitrary composite of such flips in one step.

References

This file supplies the doubled-quiver identification which the orientation-independence clause of Layer 4 of TauCetiRoadmap/ZigzagPreprojective/README.md needs; see Crawley-Boevey, Quiver algebras, weighted projective lines, and the Deligne--Simpson problem, Section 1.

def TauCeti.Reorient (Q : Type u) [Quiver Q] (_σ : ⦃i j : Q⦄ → (i ⟶ j) → Bool) : Type u

The quiver obtained from Q by turning around exactly the arrows on which the labelling σ takes the value true: an arrow i ⟶ j of Reorient Q σ is either an arrow i ⟶ j of Q which σ leaves alone, or an arrow j ⟶ i of Q which σ turns around.

Equations

• TauCeti.Reorient Q _σ = Q

@[instance_reducible]

instance TauCeti.reorientQuiver {Q : Type u} [Quiver Q] (σ : ⦃i j : Q⦄ → (i ⟶ j) → Bool) : Quiver (Reorient Q σ)

Equations

• TauCeti.reorientQuiver σ = { Hom := fun (i j : Q) => { a : i ⟶ j // ¬σ a = true } ⊕ { a : j ⟶ i // σ a = true } }

instance TauCeti.instFiniteReorient {Q : Type u} [Quiver Q] (σ : ⦃i j : Q⦄ → (i ⟶ j) → Bool) [Finite Q] : Finite (Reorient Q σ)

@[instance_reducible]

instance TauCeti.instFintypeReorient {Q : Type u} [Quiver Q] (σ : ⦃i j : Q⦄ → (i ⟶ j) → Bool) [Fintype Q] : Fintype (Reorient Q σ)

Equations

• TauCeti.instFintypeReorient σ = TauCeti.instFintypeReorient._aux_1 σ

@[instance_reducible]

def TauCeti.reorientHomFintype {Q : Type u} [Quiver Q] (σ : ⦃i j : Q⦄ → (i ⟶ j) → Bool) [(i j : Q) → Fintype (i ⟶ j)] (i j : Q) : Fintype (i ⟶ j)

A hom set of a reorientation is a disjoint union of two subtypes of hom sets of Q, hence finite. The vertices are taken in Q; TauCeti.instFintypeReorientHom is the instance form, whose vertices are taken in Reorient Q σ so that instance search can use it.

Equations

• TauCeti.reorientHomFintype σ i j = { elems := Finset.univ.disjSum Finset.univ, complete := ⋯ }

@[instance_reducible]

instance TauCeti.instFintypeReorientHom {Q : Type u} [Quiver Q] (σ : ⦃i j : Q⦄ → (i ⟶ j) → Bool) [(i j : Q) → Fintype (i ⟶ j)] (i j : Reorient Q σ) : Fintype (i ⟶ j)

Equations

• TauCeti.instFintypeReorientHom σ i j = TauCeti.reorientHomFintype σ i j

Vertices and arrows

@[reducible, inline]

abbrev TauCeti.reorientVertex {Q : Type u} [Quiver Q] (σ : ⦃i j : Q⦄ → (i ⟶ j) → Bool) (v : Q) : Reorient Q σ

The vertex of Reorient Q σ underlying a vertex of Q. The two vertex types are definitionally equal, so this is the identity; naming it keeps the two quiver structures apart.

Equations

• TauCeti.reorientVertex σ v = v

def TauCeti.reorientKeep {Q : Type u} [Quiver Q] (σ : ⦃i j : Q⦄ → (i ⟶ j) → Bool) {i j : Q} (a : i ⟶ j) (h : ¬σ a = true) : reorientVertex σ i ⟶ reorientVertex σ j

The arrow of Reorient Q σ carried by an arrow of Q which σ leaves alone.

Equations

• TauCeti.reorientKeep σ a h = Sum.inl ⟨a, h⟩

def TauCeti.reorientFlip {Q : Type u} [Quiver Q] (σ : ⦃i j : Q⦄ → (i ⟶ j) → Bool) {i j : Q} (a : j ⟶ i) (h : σ a = true) : reorientVertex σ i ⟶ reorientVertex σ j

The arrow of Reorient Q σ carried by an arrow of Q which σ turns around: it runs from the head of the original arrow to its tail.

Equations

• TauCeti.reorientFlip σ a h = Sum.inr ⟨a, h⟩

def TauCeti.reorientHomEquiv {Q : Type u} [Quiver Q] (σ : ⦃i j : Q⦄ → (i ⟶ j) → Bool) (i j : Q) : (reorientVertex σ i ⟶ reorientVertex σ j) ≃ { a : i ⟶ j // ¬σ a = true } ⊕ { a : j ⟶ i // σ a = true }

Every arrow of a reorientation is one of the two kinds: the arrows i ⟶ j of Reorient Q σ are the arrows i ⟶ j of Q which σ leaves alone together with the arrows j ⟶ i of Q which σ turns around. This equivalence is the general elimination interface for a reoriented hom set, so no consumer needs to unfold TauCeti.reorientQuiver; TauCeti.reorientHom_induction_on is its tactic form.

Equations

• TauCeti.reorientHomEquiv σ i j = Equiv.refl (TauCeti.reorientVertex σ i ⟶ TauCeti.reorientVertex σ j)

@[simp]

theorem TauCeti.reorientHomEquiv_reorientKeep {Q : Type u} [Quiver Q] (σ : ⦃i j : Q⦄ → (i ⟶ j) → Bool) {i j : Q} (a : i ⟶ j) (h : ¬σ a = true) : (reorientHomEquiv σ i j) (reorientKeep σ a h) = Sum.inl ⟨a, h⟩

The elimination equivalence sends an arrow σ leaves alone to the left summand.

@[simp]

theorem TauCeti.reorientHomEquiv_reorientFlip {Q : Type u} [Quiver Q] (σ : ⦃i j : Q⦄ → (i ⟶ j) → Bool) {i j : Q} (a : j ⟶ i) (h : σ a = true) : (reorientHomEquiv σ i j) (reorientFlip σ a h) = Sum.inr ⟨a, h⟩

The elimination equivalence sends an arrow σ turns around to the right summand.

@[simp]

theorem TauCeti.reorientHomEquiv_symm_inl {Q : Type u} [Quiver Q] (σ : ⦃i j : Q⦄ → (i ⟶ j) → Bool) {i j : Q} (x : { a : i ⟶ j // ¬σ a = true }) : (reorientHomEquiv σ i j).symm (Sum.inl x) = reorientKeep σ ↑x ⋯

The left summand of the elimination equivalence is an arrow σ leaves alone.

@[simp]

theorem TauCeti.reorientHomEquiv_symm_inr {Q : Type u} [Quiver Q] (σ : ⦃i j : Q⦄ → (i ⟶ j) → Bool) {i j : Q} (y : { a : j ⟶ i // σ a = true }) : (reorientHomEquiv σ i j).symm (Sum.inr y) = reorientFlip σ ↑y ⋯

The right summand of the elimination equivalence is an arrow σ turns around.

theorem TauCeti.reorientHom_induction_on {Q : Type u} [Quiver Q] (σ : ⦃i j : Q⦄ → (i ⟶ j) → Bool) {i j : Q} {motive : (reorientVertex σ i ⟶ reorientVertex σ j) → Prop} (b : reorientVertex σ i ⟶ reorientVertex σ j) (keep : ∀ (a : i ⟶ j) (h : ¬σ a = true), motive (reorientKeep σ a h)) (flip : ∀ (a : j ⟶ i) (h : σ a = true), motive (reorientFlip σ a h)) : motive b

Case analysis on an arrow of a reorientation: it is either an arrow of Q which σ leaves alone or an arrow of Q which σ turns around. This is the tactic form of TauCeti.reorientHomEquiv.

theorem TauCeti.sum_reorientVertex {Q : Type u} [Quiver Q] (σ : ⦃i j : Q⦄ → (i ⟶ j) → Bool) {M : Type u_1} [AddCommMonoid M] [Fintype Q] (f : Reorient Q σ → M) : ∑ v : Reorient Q σ, f v = ∑ v : Q, f (reorientVertex σ v)

A sum over the vertices of a reorientation is a sum over the vertices of Q.

theorem TauCeti.sum_reorientHom {Q : Type u} [Quiver Q] (σ : ⦃i j : Q⦄ → (i ⟶ j) → Bool) {M : Type u_1} [AddCommMonoid M] [(i j : Q) → Fintype (i ⟶ j)] (i j : Q) (f : (reorientVertex σ i ⟶ reorientVertex σ j) → M) : ∑ α : reorientVertex σ i ⟶ reorientVertex σ j, f α = ∑ x : { a : i ⟶ j // ¬σ a = true }, f (reorientKeep σ ↑x ⋯) + ∑ y : { a : j ⟶ i // σ a = true }, f (reorientFlip σ ↑y ⋯)

A sum over a hom set of a reorientation splits into the arrows σ leaves alone and the arrows σ turns around.

The doubled quivers of two orientations agree

def TauCeti.reorientSymmetrify {Q : Type u} [Quiver Q] (σ : ⦃i j : Q⦄ → (i ⟶ j) → Bool) : Quiver.Symmetrify (Reorient Q σ) ⥤q Quiver.Symmetrify Q

The comparison prefunctor from the doubled reoriented quiver to the doubled quiver. It is the identity on vertices; on arrows it forgets which of the four pieces of a hom set of Symmetrify (Reorient Q σ) an arrow came from and remembers only whether it runs forwards or backwards in Q. The body is exposed because the dependent source and target types of its public arrow-map equations contain the object map.

Equations

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

def TauCeti.reorientSymmetrifyInv {Q : Type u} [Quiver Q] (σ : ⦃i j : Q⦄ → (i ⟶ j) → Bool) : Quiver.Symmetrify Q ⥤q Quiver.Symmetrify (Reorient Q σ)

The inverse comparison: an arrow of the doubled quiver is sorted into one of the four pieces of a hom set of Symmetrify (Reorient Q σ) according to whether it runs forwards or backwards in Q and whether σ turns it around. As for TauCeti.reorientSymmetrify, exposure is needed for the dependent endpoint types of its public arrow-map equations.

Equations

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

@[simp]

theorem TauCeti.reorientSymmetrify_obj {Q : Type u} [Quiver Q] (σ : ⦃i j : Q⦄ → (i ⟶ j) → Bool) (i : Quiver.Symmetrify (Reorient Q σ)) : (reorientSymmetrify σ).obj i = i

The comparison of doubled quivers is the identity on vertices.

@[simp]

theorem TauCeti.reorientSymmetrifyInv_obj {Q : Type u} [Quiver Q] (σ : ⦃i j : Q⦄ → (i ⟶ j) → Bool) (i : Quiver.Symmetrify Q) : (reorientSymmetrifyInv σ).obj i = i

The inverse comparison of doubled quivers is the identity on vertices.

theorem TauCeti.reorientSymmetrifyInv_map_of_keep {Q : Type u} [Quiver Q] (σ : ⦃i j : Q⦄ → (i ⟶ j) → Bool) {i j : Q} (a : i ⟶ j) (h : ¬σ a = true) : (reorientSymmetrifyInv σ).map (Quiver.Symmetrify.of.map a) = Quiver.Symmetrify.of.map (reorientKeep σ a h)

The inverse comparison sends an arrow which σ leaves alone to the corresponding arrow of the reoriented quiver. Deliberately not a simp lemma: Quiver.Symmetrify.of_map rewrites Symmetrify.of.map a to Sum.inl a on the left-hand side, and simpNF rejects it.

theorem TauCeti.reorientSymmetrifyInv_map_reverse_of_keep {Q : Type u} [Quiver Q] (σ : ⦃i j : Q⦄ → (i ⟶ j) → Bool) {i j : Q} (a : i ⟶ j) (h : ¬σ a = true) : (reorientSymmetrifyInv σ).map (Quiver.reverse (Quiver.Symmetrify.of.map a)) = Quiver.reverse (Quiver.Symmetrify.of.map (reorientKeep σ a h))

The inverse comparison sends the formal reverse of an arrow which σ leaves alone to the formal reverse of the corresponding reoriented arrow. Deliberately not a simp lemma: simplifying formal reversal first would make this a non-normal-form rule.

theorem TauCeti.reorientSymmetrifyInv_map_of_flip {Q : Type u} [Quiver Q] (σ : ⦃i j : Q⦄ → (i ⟶ j) → Bool) {i j : Q} (a : i ⟶ j) (h : σ a = true) : (reorientSymmetrifyInv σ).map (Quiver.Symmetrify.of.map a) = Quiver.reverse (Quiver.Symmetrify.of.map (reorientFlip σ a h))

The inverse comparison sends an arrow which σ turns around to the formal reverse of the corresponding reoriented arrow. Deliberately not a simp lemma, for the reason recorded on TauCeti.reorientSymmetrifyInv_map_of_keep.

theorem TauCeti.reorientSymmetrifyInv_map_reverse_of_flip {Q : Type u} [Quiver Q] (σ : ⦃i j : Q⦄ → (i ⟶ j) → Bool) {i j : Q} (a : i ⟶ j) (h : σ a = true) : (reorientSymmetrifyInv σ).map (Quiver.reverse (Quiver.Symmetrify.of.map a)) = Quiver.Symmetrify.of.map (reorientFlip σ a h)

The inverse comparison sends the formal reverse of an arrow which σ turns around to the corresponding reoriented arrow. Deliberately not a simp lemma, for the reason recorded on TauCeti.reorientSymmetrifyInv_map_reverse_of_keep.

theorem TauCeti.reorientSymmetrify_map_of_keep {Q : Type u} [Quiver Q] (σ : ⦃i j : Q⦄ → (i ⟶ j) → Bool) {i j : Q} (a : i ⟶ j) (h : ¬σ a = true) : (reorientSymmetrify σ).map (Quiver.Symmetrify.of.map (reorientKeep σ a h)) = Quiver.Symmetrify.of.map a

An arrow of Q which σ leaves alone stays an arrow of the doubled quiver. Deliberately not a simp lemma: Quiver.Symmetrify.of_map rewrites Symmetrify.of.map ... to Sum.inl ... on the left-hand side, and simpNF rejects it.

theorem TauCeti.reorientSymmetrify_map_reverse_of_keep {Q : Type u} [Quiver Q] (σ : ⦃i j : Q⦄ → (i ⟶ j) → Bool) {i j : Q} (a : i ⟶ j) (h : ¬σ a = true) : (reorientSymmetrify σ).map (Quiver.reverse (Quiver.Symmetrify.of.map (reorientKeep σ a h))) = Quiver.reverse (Quiver.Symmetrify.of.map a)

The formal reverse of an arrow which σ leaves alone stays a formal reverse. Deliberately not a simp lemma: Quiver.symmetrify_reverse rewrites Quiver.reverse to Sum.swap on the left-hand side, and simpNF rejects the pair.

theorem TauCeti.reorientSymmetrify_map_of_flip {Q : Type u} [Quiver Q] (σ : ⦃i j : Q⦄ → (i ⟶ j) → Bool) {i j : Q} (a : j ⟶ i) (h : σ a = true) : (reorientSymmetrify σ).map (Quiver.Symmetrify.of.map (reorientFlip σ a h)) = Quiver.reverse (Quiver.Symmetrify.of.map a)

An arrow of Q which σ turns around becomes the formal reverse of itself. Deliberately not a simp lemma, for the reason recorded on TauCeti.reorientSymmetrify_map_of_keep.

theorem TauCeti.reorientSymmetrify_map_reverse_of_flip {Q : Type u} [Quiver Q] (σ : ⦃i j : Q⦄ → (i ⟶ j) → Bool) {i j : Q} (a : j ⟶ i) (h : σ a = true) : (reorientSymmetrify σ).map (Quiver.reverse (Quiver.Symmetrify.of.map (reorientFlip σ a h))) = Quiver.Symmetrify.of.map a

The formal reverse of a turned-around arrow is the arrow itself. Deliberately not a simp lemma, for the reason recorded on TauCeti.reorientSymmetrify_map_reverse_of_keep.

theorem TauCeti.reorientSymmetrify_comp_reorientSymmetrifyInv {Q : Type u} [Quiver Q] (σ : ⦃i j : Q⦄ → (i ⟶ j) → Bool) : reorientSymmetrify σ ⋙q reorientSymmetrifyInv σ = 𝟭q (Quiver.Symmetrify (Reorient Q σ))

The two comparisons are inverse, starting from the reoriented quiver.

theorem TauCeti.reorientSymmetrifyInv_comp_reorientSymmetrify {Q : Type u} [Quiver Q] (σ : ⦃i j : Q⦄ → (i ⟶ j) → Bool) : reorientSymmetrifyInv σ ⋙q reorientSymmetrify σ = 𝟭q (Quiver.Symmetrify Q)

The two comparisons are inverse, starting from the original quiver.

theorem TauCeti.reorientSymmetrify_map_reverse {Q : Type u} [Quiver Q] (σ : ⦃i j : Q⦄ → (i ⟶ j) → Bool) {i j : Quiver.Symmetrify (Reorient Q σ)} (b : i ⟶ j) : (reorientSymmetrify σ).map (Quiver.reverse b) = Quiver.reverse ((reorientSymmetrify σ).map b)

The comparison of doubled quivers commutes with arrow reversal, so it identifies the two doubled quivers as quivers with an involutive reverse.