The local source unfold

This file formalizes the local graph move used in the last case of the Stallings proof of Grushko's theorem. Fix an oriented edge e₀ leaving a vertex a. The source is split into an old copy and a new copy. All original arrows labelled in the colour of e₀ remain attached to the old copy, the other coloured arrows are attached to the new copy, and a second copy of e₀ is attached to the new copy.

The construction is intentionally local. In particular, it does not yet choose a new marking or perform the subsequent monochromatic-vertex contraction. The main certified fact here is that the old copy is monochromatic, exactly the invariant needed by that contraction.

Split vertices and duplicated arrows

@[reducible, inline]

abbrev MarshallHall.GeneralGrushko.UnfoldVertex {V : Type u} (a : V) : Type u

A copy of a is added to the original vertex set. false denotes the old copy and true the new copy.

Equations

• MarshallHall.GeneralGrushko.UnfoldVertex a = ({ x : V // x ≠ a } ⊕ Bool)

@[instance_reducible]

noncomputable instance MarshallHall.GeneralGrushko.unfoldVertexFintype {V : Type u} [Fintype V] (a : V) : Fintype (UnfoldVertex a)

Equations

• MarshallHall.GeneralGrushko.unfoldVertexFintype a = id inferInstance

def MarshallHall.GeneralGrushko.unfoldOld {V : Type u} (a : V) : UnfoldVertex a

The original copy of the vertex split by unfolding.

Equations

• MarshallHall.GeneralGrushko.unfoldOld a = Sum.inr false

def MarshallHall.GeneralGrushko.unfoldNew {V : Type u} (a : V) : UnfoldVertex a

The new copy of the vertex created by unfolding.

Equations

• MarshallHall.GeneralGrushko.unfoldNew a = Sum.inr true

theorem MarshallHall.GeneralGrushko.unfoldOld_ne_new {V : Type u} (a : V) : unfoldOld a ≠ unfoldNew a

theorem MarshallHall.GeneralGrushko.unfoldNew_ne_old {V : Type u} (a : V) : unfoldNew a ≠ unfoldOld a

def MarshallHall.GeneralGrushko.unfoldEdgeColor {G H : Type v} [Group G] [Group H] {V : Type u} [Quiver V] [Quiver.HasInvolutiveReverse V] (L : BinaryLabelling) (e : AllArrow) : Bool

The factor containing an edge's label.

Equations

• MarshallHall.GeneralGrushko.unfoldEdgeColor L e = MarshallHall.GeneralGrushko.binarySumIndex (MarshallHall.GeneralGrushko.allArrowLabel L e)

noncomputable def MarshallHall.GeneralGrushko.unfoldVertexAt {G H : Type v} [Group G] [Group H] {V : Type u} [Quiver V] [Quiver.HasInvolutiveReverse V] (L : BinaryLabelling) (a : V) (e₀ : AllArrow) (x : V) (c : Bool) : UnfoldVertex a

Chooses the appropriate copy of the split vertex according to the incident factor.

Equations

• MarshallHall.GeneralGrushko.unfoldVertexAt L a e₀ x c = if h : x = a then Sum.inr (if c = MarshallHall.GeneralGrushko.unfoldEdgeColor L e₀ then false else true) else Sum.inl ⟨x, h⟩

theorem MarshallHall.GeneralGrushko.unfoldVertexAt_eq_old_iff {G H : Type v} [Group G] [Group H] {V : Type u} [Quiver V] [Quiver.HasInvolutiveReverse V] (L : BinaryLabelling) (a : V) (e₀ : AllArrow) (x : V) (c : Bool) : unfoldVertexAt L a e₀ x c = unfoldOld a ↔ x = a ∧ c = unfoldEdgeColor L e₀

theorem MarshallHall.GeneralGrushko.unfoldVertexAt_eq_new_iff {G H : Type v} [Group G] [Group H] {V : Type u} [Quiver V] [Quiver.HasInvolutiveReverse V] (L : BinaryLabelling) (a : V) (e₀ : AllArrow) (x : V) (c : Bool) : unfoldVertexAt L a e₀ x c = unfoldNew a ↔ x = a ∧ c ≠ unfoldEdgeColor L e₀

theorem MarshallHall.GeneralGrushko.unfoldVertexAt_of_ne {G H : Type v} [Group G] [Group H] {V : Type u} [Quiver V] [Quiver.HasInvolutiveReverse V] {a : V} {e₀ : AllArrow} (L : BinaryLabelling) (x : V) (c : Bool) (hx : x ≠ a) : unfoldVertexAt L a e₀ x c = Sum.inl ⟨x, hx⟩

theorem MarshallHall.GeneralGrushko.unfoldEdgeColor_reverse {G H : Type v} [Group G] [Group H] {V : Type u} [Quiver V] [Quiver.HasInvolutiveReverse V] (L : BinaryLabelling) (e : AllArrow) : unfoldEdgeColor L (allArrowReverse e) = unfoldEdgeColor L e

The unfolded edge type and its quiver

@[reducible, inline]

abbrev MarshallHall.GeneralGrushko.UnfoldEdge {V : Type u} [Quiver V] : Type (max u_1 u)

The old oriented edges together with the two orientations of a duplicated edge. The Bool component is the orientation of the duplicate.

Equations

• MarshallHall.GeneralGrushko.UnfoldEdge = (MarshallHall.GeneralGrushko.AllArrow ⊕ Bool)

@[instance_reducible]

noncomputable instance MarshallHall.GeneralGrushko.unfoldEdgeFintype {V : Type u} [Fintype V] [Quiver V] [(a b : V) → Fintype (a ⟶ b)] : Fintype UnfoldEdge

Equations

• MarshallHall.GeneralGrushko.unfoldEdgeFintype = id inferInstance

def MarshallHall.GeneralGrushko.unfoldEdgeReverse {V : Type u} [Quiver V] [Quiver.HasInvolutiveReverse V] : UnfoldEdge → UnfoldEdge

Reverses an original or duplicated edge in the unfolded graph.

Equations

• MarshallHall.GeneralGrushko.unfoldEdgeReverse (Sum.inl e) = Sum.inl (MarshallHall.GeneralGrushko.allArrowReverse e)
• MarshallHall.GeneralGrushko.unfoldEdgeReverse (Sum.inr false) = Sum.inr true
• MarshallHall.GeneralGrushko.unfoldEdgeReverse (Sum.inr true) = Sum.inr false

@[simp]

theorem MarshallHall.GeneralGrushko.unfoldEdgeReverse_reverse {V : Type u} [Quiver V] [Quiver.HasInvolutiveReverse V] (e : UnfoldEdge) : unfoldEdgeReverse (unfoldEdgeReverse e) = e

noncomputable def MarshallHall.GeneralGrushko.unfoldEdgeSource {G H : Type v} [Group G] [Group H] {V : Type u} [Quiver V] [Quiver.HasInvolutiveReverse V] (L : BinaryLabelling) (e₀ : AllArrow) : UnfoldEdge → UnfoldVertex (allArrowSource e₀)

The source of an edge after the vertex has been split by factor.

Equations

• One or more equations did not get rendered due to their size.
• MarshallHall.GeneralGrushko.unfoldEdgeSource L e₀ (Sum.inr false) = MarshallHall.GeneralGrushko.unfoldNew (MarshallHall.GeneralGrushko.allArrowSource e₀)

noncomputable def MarshallHall.GeneralGrushko.unfoldEdgeTarget {G H : Type v} [Group G] [Group H] {V : Type u} [Quiver V] [Quiver.HasInvolutiveReverse V] (L : BinaryLabelling) (e₀ : AllArrow) : UnfoldEdge → UnfoldVertex (allArrowSource e₀)

The target of an edge after the vertex has been split by factor.

Equations

• One or more equations did not get rendered due to their size.
• MarshallHall.GeneralGrushko.unfoldEdgeTarget L e₀ (Sum.inr true) = MarshallHall.GeneralGrushko.unfoldNew (MarshallHall.GeneralGrushko.allArrowSource e₀)

theorem MarshallHall.GeneralGrushko.unfoldEdgeSource_reverse {G H : Type v} [Group G] [Group H] {V : Type u} [Quiver V] [Quiver.HasInvolutiveReverse V] (L : BinaryLabelling) (e₀ : AllArrow) (e : UnfoldEdge) : unfoldEdgeSource L e₀ (unfoldEdgeReverse e) = unfoldEdgeTarget L e₀ e

theorem MarshallHall.GeneralGrushko.unfoldEdgeTarget_reverse {G H : Type v} [Group G] [Group H] {V : Type u} [Quiver V] [Quiver.HasInvolutiveReverse V] (L : BinaryLabelling) (e₀ : AllArrow) (e : UnfoldEdge) : unfoldEdgeTarget L e₀ (unfoldEdgeReverse e) = unfoldEdgeSource L e₀ e

@[reducible]

def MarshallHall.GeneralGrushko.unfoldQuiver {G H : Type v} [Group G] [Group H] {V : Type u} [Quiver V] [Quiver.HasInvolutiveReverse V] (L : BinaryLabelling) (e₀ : AllArrow) : Quiver (UnfoldVertex (allArrowSource e₀))

The quiver obtained by splitting a vertex and duplicating the selected edge.

Equations

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

@[instance_reducible]

noncomputable def MarshallHall.GeneralGrushko.unfoldQuiverHomFintype {G H : Type v} [Group G] [Group H] {V : Type u} [Fintype V] [Quiver V] [Quiver.HasInvolutiveReverse V] [(a b : V) → Fintype (a ⟶ b)] (L : BinaryLabelling) (e₀ : AllArrow) (x y : UnfoldVertex (allArrowSource e₀)) : Fintype (x ⟶ y)

A finite enumeration of arrows in the unfolded quiver.

Equations

• MarshallHall.GeneralGrushko.unfoldQuiverHomFintype L e₀ x y = id inferInstance

@[instance_reducible]

noncomputable instance MarshallHall.GeneralGrushko.unfoldAllArrowFintype {G H : Type v} [Group G] [Group H] {V : Type u} [Fintype V] [Quiver V] [Quiver.HasInvolutiveReverse V] [(a b : V) → Fintype (a ⟶ b)] (L : BinaryLabelling) (e₀ : AllArrow) : Fintype AllArrow

Equations

• MarshallHall.GeneralGrushko.unfoldAllArrowFintype L e₀ = MarshallHall.GeneralGrushko.allArrowFintype

def MarshallHall.GeneralGrushko.unfoldReverseArrow {G H : Type v} [Group G] [Group H] {V : Type u} [Quiver V] [Quiver.HasInvolutiveReverse V] (L : BinaryLabelling) (e₀ : AllArrow) {x y : UnfoldVertex (allArrowSource e₀)} (e : x ⟶ y) : y ⟶ x

Reverses an arrow of the unfolded quiver.

Equations

• MarshallHall.GeneralGrushko.unfoldReverseArrow L e₀ e = ⟨MarshallHall.GeneralGrushko.unfoldEdgeReverse ↑e, ⋯⟩

@[instance_reducible]

def MarshallHall.GeneralGrushko.unfoldHasReverse {G H : Type v} [Group G] [Group H] {V : Type u} [Quiver V] [Quiver.HasInvolutiveReverse V] (L : BinaryLabelling) (e₀ : AllArrow) : Quiver.HasInvolutiveReverse (UnfoldVertex (allArrowSource e₀))

The involutive reversal on the unfolded quiver.

Equations

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

def MarshallHall.GeneralGrushko.unfoldEdgeLabel {G H : Type v} [Group G] [Group H] {V : Type u} [Quiver V] [Quiver.HasInvolutiveReverse V] (L : BinaryLabelling) (e₀ : AllArrow) : UnfoldEdge → G ⊕ H

The label of an unfolded edge, using the selected edge's label for its duplicate.

Equations

• MarshallHall.GeneralGrushko.unfoldEdgeLabel L e₀ (Sum.inl e) = MarshallHall.GeneralGrushko.allArrowLabel L e
• MarshallHall.GeneralGrushko.unfoldEdgeLabel L e₀ (Sum.inr false) = MarshallHall.GeneralGrushko.allArrowLabel L e₀
• MarshallHall.GeneralGrushko.unfoldEdgeLabel L e₀ (Sum.inr true) = MarshallHall.GeneralGrushko.factorWordInv (MarshallHall.GeneralGrushko.allArrowLabel L e₀)

theorem MarshallHall.GeneralGrushko.unfoldEdgeLabel_reverse {G H : Type v} [Group G] [Group H] {V : Type u} [Quiver V] [Quiver.HasInvolutiveReverse V] (L : BinaryLabelling) (e₀ : AllArrow) (e : UnfoldEdge) : unfoldEdgeLabel L e₀ (unfoldEdgeReverse e) = factorWordInv (unfoldEdgeLabel L e₀ e)

def MarshallHall.GeneralGrushko.unfoldLabelling {G H : Type v} [Group G] [Group H] {V : Type u} [Quiver V] [Quiver.HasInvolutiveReverse V] (L : BinaryLabelling) (e₀ : AllArrow) : BinaryLabelling

The factor labelling on the unfolded graph.

Equations

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

The old copy is monochromatic

def MarshallHall.GeneralGrushko.unfoldOldIncident {G H : Type v} [Group G] [Group H] {V : Type u} [Quiver V] [Quiver.HasInvolutiveReverse V] (L : BinaryLabelling) (e₀ : AllArrow) (e : AllArrow) : Prop

An unfolded arrow is incident to the original copy of the split vertex.

Equations

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

theorem MarshallHall.GeneralGrushko.unfold_old_incident_color {G H : Type v} [Group G] [Group H] {V : Type u} [Quiver V] [Quiver.HasInvolutiveReverse V] (L : BinaryLabelling) (e₀ : AllArrow) (e : AllArrow) (h : unfoldOldIncident L e₀ e) : binarySumIndex (unfoldEdgeLabel L e₀ ↑e.snd.snd) = unfoldEdgeColor L e₀

def MarshallHall.GeneralGrushko.unfoldOriginalEdge {G H : Type v} [Group G] [Group H] {V : Type u} [Quiver V] [Quiver.HasInvolutiveReverse V] (L : BinaryLabelling) (e₀ : AllArrow) {x y : V} (e : x ⟶ y) : unfoldVertexAt L (allArrowSource e₀) e₀ x (unfoldEdgeColor L (allArrowOf e)) ⟶ unfoldVertexAt L (allArrowSource e₀) e₀ y (unfoldEdgeColor L (allArrowOf e))

The unfolded arrow corresponding to an original edge.

Equations

• MarshallHall.GeneralGrushko.unfoldOriginalEdge L e₀ e = ⟨Sum.inl (MarshallHall.GeneralGrushko.allArrowOf e), ⋯⟩

theorem MarshallHall.GeneralGrushko.unfoldOriginalEdge_label {G H : Type v} [Group G] [Group H] {V : Type u} [Quiver V] [Quiver.HasInvolutiveReverse V] (L : BinaryLabelling) (e₀ : AllArrow) {x y : V} (e : x ⟶ y) : unfoldEdgeLabel L e₀ (Sum.inl (allArrowOf e)) = L.label e

def MarshallHall.GeneralGrushko.unfoldOriginalEdgeAtColor {G H : Type v} [Group G] [Group H] {V : Type u} [Quiver V] [Quiver.HasInvolutiveReverse V] (L : BinaryLabelling) (e₀ : AllArrow) {x y : V} (e : x ⟶ y) (color : Bool) (hc : unfoldEdgeColor L (allArrowOf e) = color) : unfoldVertexAt L (allArrowSource e₀) e₀ x color ⟶ unfoldVertexAt L (allArrowSource e₀) e₀ y color

The unfolded original edge with its factor made explicit in the endpoints.

Equations

• MarshallHall.GeneralGrushko.unfoldOriginalEdgeAtColor L e₀ e color hc = ⟨Sum.inl (MarshallHall.GeneralGrushko.allArrowOf e), ⋯⟩

theorem MarshallHall.GeneralGrushko.unfoldOriginalEdgeAtColor_label {G H : Type v} [Group G] [Group H] {V : Type u} [Quiver V] [Quiver.HasInvolutiveReverse V] (L : BinaryLabelling) (e₀ : AllArrow) {x y : V} (e : x ⟶ y) (color : Bool) (hc : unfoldEdgeColor L (allArrowOf e) = color) : unfoldEdgeLabel L e₀ ↑(unfoldOriginalEdgeAtColor L e₀ e color hc) = L.label e

@[irreducible]

def MarshallHall.GeneralGrushko.unfoldMonochromaticPath {G H : Type v} [Group G] [Group H] {V : Type u} [Quiver V] [Quiver.HasInvolutiveReverse V] (L : BinaryLabelling) (e₀ : AllArrow) (color : Bool) {x y : V} (p : Quiver.Path x y) : L.IsMonochromatic p color → Quiver.Path (unfoldVertexAt L (allArrowSource e₀) e₀ x color) (unfoldVertexAt L (allArrowSource e₀) e₀ y color)

Lifts a monochromatic path to the corresponding factor side of the unfolded graph.

Equations

• One or more equations did not get rendered due to their size.
• MarshallHall.GeneralGrushko.unfoldMonochromaticPath L e₀ color Quiver.Path.nil x_4 = Quiver.Path.nil

theorem MarshallHall.GeneralGrushko.unfoldMonochromaticPath_read {G H : Type v} [Group G] [Group H] {V : Type u} [Quiver V] [Quiver.HasInvolutiveReverse V] (L : BinaryLabelling) (e₀ : AllArrow) (color : Bool) {x y : V} (p : Quiver.Path x y) (hp : L.IsMonochromatic p color) : (unfoldLabelling L e₀).pathRead (unfoldMonochromaticPath L e₀ color p hp) = L.pathRead p

Cardinal bookkeeping

theorem MarshallHall.GeneralGrushko.unfoldEdge_card {V : Type u} [Fintype V] [Quiver V] [(a b : V) → Fintype (a ⟶ b)] : Fintype.card UnfoldEdge = Fintype.card AllArrow + 2

noncomputable def MarshallHall.GeneralGrushko.unfoldAllArrowEquivEdge {G H : Type v} [Group G] [Group H] {V : Type u} [Quiver V] [Quiver.HasInvolutiveReverse V] (L : BinaryLabelling) (e₀ : AllArrow) : AllArrow ≃ UnfoldEdge

Identifies packaged arrows in the unfolded quiver with its explicit edge type.

Equations

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

theorem MarshallHall.GeneralGrushko.unfoldAllArrow_card {G H : Type v} [Group G] [Group H] {V : Type u} [Fintype V] [Quiver V] [Quiver.HasInvolutiveReverse V] [(a b : V) → Fintype (a ⟶ b)] (L : BinaryLabelling) (e₀ : AllArrow) : Fintype.card AllArrow = Fintype.card AllArrow + 2

theorem MarshallHall.GeneralGrushko.unfoldVertex_card {V : Type u} [Fintype V] (a : V) : Fintype.card (UnfoldVertex a) = Fintype.card V + 1

theorem MarshallHall.GeneralGrushko.unfold_euler_bound {G H : Type v} [Group G] [Group H] {V : Type u} [Fintype V] [Quiver V] [Quiver.HasInvolutiveReverse V] [(a b : V) → Fintype (a ⟶ b)] {n : ℕ} (L : BinaryLabelling) (e₀ : AllArrow) (hEuler : Fintype.card AllArrow ≤ 2 * (n + Fintype.card V - 1)) : Fintype.card AllArrow ≤ 2 * (n + Fintype.card (UnfoldVertex (allArrowSource e₀)) - 1)

theorem MarshallHall.GeneralGrushko.unfold_allArrow_reverse_ne {G H : Type v} [Group G] [Group H] {V : Type u} [Quiver V] [Quiver.HasInvolutiveReverse V] (L : BinaryLabelling) (e₀ : AllArrow) (hfree : ReverseFree) (e : AllArrow) : allArrowReverse e ≠ e

The zero-labelled switch paths

def MarshallHall.GeneralGrushko.unfoldBaseEdge {G H : Type v} [Group G] [Group H] {V : Type u} [Quiver V] [Quiver.HasInvolutiveReverse V] (L : BinaryLabelling) (e₀ : AllArrow) : unfoldOld (allArrowSource e₀) ⟶ unfoldVertexAt L (allArrowSource e₀) e₀ (allArrowTarget e₀) (unfoldEdgeColor L e₀)

The selected original edge starting at the original copy of the split vertex.

Equations

• MarshallHall.GeneralGrushko.unfoldBaseEdge L e₀ = ⟨Sum.inl e₀, ⋯⟩

def MarshallHall.GeneralGrushko.unfoldBaseReverseEdge {G H : Type v} [Group G] [Group H] {V : Type u} [Quiver V] [Quiver.HasInvolutiveReverse V] (L : BinaryLabelling) (e₀ : AllArrow) : unfoldVertexAt L (allArrowSource e₀) e₀ (allArrowTarget e₀) (unfoldEdgeColor L e₀) ⟶ unfoldOld (allArrowSource e₀)

The reverse of the selected original edge in the unfolded graph.

Equations

• MarshallHall.GeneralGrushko.unfoldBaseReverseEdge L e₀ = ⟨Sum.inl (MarshallHall.GeneralGrushko.allArrowReverse e₀), ⋯⟩

def MarshallHall.GeneralGrushko.unfoldDuplicateForward {G H : Type v} [Group G] [Group H] {V : Type u} [Quiver V] [Quiver.HasInvolutiveReverse V] (L : BinaryLabelling) (e₀ : AllArrow) : unfoldNew (allArrowSource e₀) ⟶ unfoldVertexAt L (allArrowSource e₀) e₀ (allArrowTarget e₀) (unfoldEdgeColor L e₀)

The duplicate of the selected edge starting at the new vertex.

Equations

• MarshallHall.GeneralGrushko.unfoldDuplicateForward L e₀ = ⟨Sum.inr false, ⋯⟩

def MarshallHall.GeneralGrushko.unfoldDuplicateBackward {G H : Type v} [Group G] [Group H] {V : Type u} [Quiver V] [Quiver.HasInvolutiveReverse V] (L : BinaryLabelling) (e₀ : AllArrow) : unfoldVertexAt L (allArrowSource e₀) e₀ (allArrowTarget e₀) (unfoldEdgeColor L e₀) ⟶ unfoldNew (allArrowSource e₀)

The reverse orientation of the duplicated selected edge.

Equations

• MarshallHall.GeneralGrushko.unfoldDuplicateBackward L e₀ = ⟨Sum.inr true, ⋯⟩

noncomputable def MarshallHall.GeneralGrushko.unfoldSwitchOldNew {G H : Type v} [Group G] [Group H] {V : Type u} [Quiver V] [Quiver.HasInvolutiveReverse V] (L : BinaryLabelling) (e₀ : AllArrow) : Quiver.Path (unfoldOld (allArrowSource e₀)) (unfoldNew (allArrowSource e₀))

The path from the original split vertex to its new copy through the selected edge pair.

Equations

• MarshallHall.GeneralGrushko.unfoldSwitchOldNew L e₀ = (MarshallHall.GeneralGrushko.unfoldBaseEdge L e₀).toPath.comp (MarshallHall.GeneralGrushko.unfoldDuplicateBackward L e₀).toPath

noncomputable def MarshallHall.GeneralGrushko.unfoldSwitchNewOld {G H : Type v} [Group G] [Group H] {V : Type u} [Quiver V] [Quiver.HasInvolutiveReverse V] (L : BinaryLabelling) (e₀ : AllArrow) : Quiver.Path (unfoldNew (allArrowSource e₀)) (unfoldOld (allArrowSource e₀))

The reverse switching path from the new split vertex to its original copy.

Equations

• MarshallHall.GeneralGrushko.unfoldSwitchNewOld L e₀ = (MarshallHall.GeneralGrushko.unfoldDuplicateForward L e₀).toPath.comp (MarshallHall.GeneralGrushko.unfoldBaseReverseEdge L e₀).toPath

theorem MarshallHall.GeneralGrushko.unfoldSwitchOldNew_read {G H : Type v} [Group G] [Group H] {V : Type u} [Quiver V] [Quiver.HasInvolutiveReverse V] (L : BinaryLabelling) (e₀ : AllArrow) : (unfoldLabelling L e₀).pathRead (unfoldSwitchOldNew L e₀) = 1

theorem MarshallHall.GeneralGrushko.unfoldSwitchNewOld_read {G H : Type v} [Group G] [Group H] {V : Type u} [Quiver V] [Quiver.HasInvolutiveReverse V] (L : BinaryLabelling) (e₀ : AllArrow) : (unfoldLabelling L e₀).pathRead (unfoldSwitchNewOld L e₀) = 1

Canonical endpoints and path lifting

noncomputable def MarshallHall.GeneralGrushko.unfoldCanonical {V : Type u} (a x : V) : UnfoldVertex a

The canonical lift of an original vertex, choosing the original copy at the split vertex.

Equations

• MarshallHall.GeneralGrushko.unfoldCanonical a x = if h : x = a then MarshallHall.GeneralGrushko.unfoldOld a else Sum.inl ⟨x, h⟩

theorem MarshallHall.GeneralGrushko.unfoldCanonical_eq_old {V : Type u} (a : V) : unfoldCanonical a a = unfoldOld a

theorem MarshallHall.GeneralGrushko.unfoldCanonical_eq_vertexAt_of_ne {G H : Type v} [Group G] [Group H] {V : Type u} [Quiver V] [Quiver.HasInvolutiveReverse V] (L : BinaryLabelling) (e₀ : AllArrow) {x : V} (hx : x ≠ allArrowSource e₀) (color : Bool) : unfoldCanonical (allArrowSource e₀) x = unfoldVertexAt L (allArrowSource e₀) e₀ x color

theorem MarshallHall.GeneralGrushko.unfoldVertexAt_eq_new_of_ne_color {G H : Type v} [Group G] [Group H] {V : Type u} [Quiver V] [Quiver.HasInvolutiveReverse V] (L : BinaryLabelling) (e₀ : AllArrow) (color : Bool) (hc : color ≠ unfoldEdgeColor L e₀) : unfoldVertexAt L (allArrowSource e₀) e₀ (allArrowSource e₀) color = unfoldNew (allArrowSource e₀)

noncomputable def MarshallHall.GeneralGrushko.unfoldPrePath {G H : Type v} [Group G] [Group H] {V : Type u} [Quiver V] [Quiver.HasInvolutiveReverse V] (L : BinaryLabelling) (e₀ : AllArrow) {x y : V} (e : x ⟶ y) : Quiver.Path (unfoldCanonical (allArrowSource e₀) x) (unfoldVertexAt L (allArrowSource e₀) e₀ x (unfoldEdgeColor L (allArrowOf e)))

The switching path before an unfolded edge, from its canonical source to its factor side.

Equations

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

noncomputable def MarshallHall.GeneralGrushko.unfoldPostPath {G H : Type v} [Group G] [Group H] {V : Type u} [Quiver V] [Quiver.HasInvolutiveReverse V] (L : BinaryLabelling) (e₀ : AllArrow) {x y : V} (e : x ⟶ y) : Quiver.Path (unfoldVertexAt L (allArrowSource e₀) e₀ y (unfoldEdgeColor L (allArrowOf e))) (unfoldCanonical (allArrowSource e₀) y)

The switching path after an unfolded edge, from its factor side to its canonical target.

Equations

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

noncomputable def MarshallHall.GeneralGrushko.unfoldLiftEdge {G H : Type v} [Group G] [Group H] {V : Type u} [Quiver V] [Quiver.HasInvolutiveReverse V] (L : BinaryLabelling) (e₀ : AllArrow) {x y : V} (e : x ⟶ y) : Quiver.Path (unfoldCanonical (allArrowSource e₀) x) (unfoldCanonical (allArrowSource e₀) y)

Lifts an original edge as a path between canonical lifted endpoints.

Equations

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

theorem MarshallHall.GeneralGrushko.unfoldPrePath_read {G H : Type v} [Group G] [Group H] {V : Type u} [Quiver V] [Quiver.HasInvolutiveReverse V] (L : BinaryLabelling) (e₀ : AllArrow) {x y : V} (e : x ⟶ y) : (unfoldLabelling L e₀).pathRead (unfoldPrePath L e₀ e) = 1

theorem MarshallHall.GeneralGrushko.unfoldPostPath_read {G H : Type v} [Group G] [Group H] {V : Type u} [Quiver V] [Quiver.HasInvolutiveReverse V] (L : BinaryLabelling) (e₀ : AllArrow) {x y : V} (e : x ⟶ y) : (unfoldLabelling L e₀).pathRead (unfoldPostPath L e₀ e) = 1

theorem MarshallHall.GeneralGrushko.unfoldLiftEdge_read {G H : Type v} [Group G] [Group H] {V : Type u} [Quiver V] [Quiver.HasInvolutiveReverse V] (L : BinaryLabelling) (e₀ : AllArrow) {x y : V} (e : x ⟶ y) : (unfoldLabelling L e₀).pathRead (unfoldLiftEdge L e₀ e) = L.pathRead e.toPath

@[irreducible]

def MarshallHall.GeneralGrushko.unfoldLiftPath {G H : Type v} [Group G] [Group H] {V : Type u} [Quiver V] [Quiver.HasInvolutiveReverse V] (L : BinaryLabelling) (e₀ : AllArrow) {x y : V} : Quiver.Path x y → Quiver.Path (unfoldCanonical (allArrowSource e₀) x) (unfoldCanonical (allArrowSource e₀) y)

Lifts an ordinary path to a path between canonical vertices of the unfolded graph.

Equations

• MarshallHall.GeneralGrushko.unfoldLiftPath L e₀ Quiver.Path.nil = Quiver.Path.nil
• MarshallHall.GeneralGrushko.unfoldLiftPath L e₀ (p.cons e) = (MarshallHall.GeneralGrushko.unfoldLiftPath L e₀ p).comp (MarshallHall.GeneralGrushko.unfoldLiftEdge L e₀ e)

theorem MarshallHall.GeneralGrushko.unfoldLiftPath_read {G H : Type v} [Group G] [Group H] {V : Type u} [Quiver V] [Quiver.HasInvolutiveReverse V] (L : BinaryLabelling) (e₀ : AllArrow) {x y : V} (p : Quiver.Path x y) : (unfoldLabelling L e₀).pathRead (unfoldLiftPath L e₀ p) = L.pathRead p

noncomputable def MarshallHall.GeneralGrushko.unfoldSymmLiftArrow {G H : Type v} [Group G] [Group H] {V : Type u} [Quiver V] [Quiver.HasInvolutiveReverse V] (L : BinaryLabelling) (e₀ : AllArrow) {x y : Quiver.Symmetrify V} (e : x ⟶ y) : Quiver.Path (unfoldCanonical (allArrowSource e₀) (have this := x; this)) (unfoldCanonical (allArrowSource e₀) (have this := y; this))

Lifts a symmetrized arrow to a path in the unfolded graph.

Equations

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

@[irreducible]

def MarshallHall.GeneralGrushko.unfoldSymmLiftPath {G H : Type v} [Group G] [Group H] {V : Type u} [Quiver V] [Quiver.HasInvolutiveReverse V] (L : BinaryLabelling) (e₀ : AllArrow) {x y : Quiver.Symmetrify V} : Quiver.Path x y → Quiver.Path (unfoldCanonical (allArrowSource e₀) (have this := x; this)) (unfoldCanonical (allArrowSource e₀) (have this := y; this))

Lifts a symmetrized path to a path in the unfolded graph.

Equations

• MarshallHall.GeneralGrushko.unfoldSymmLiftPath L e₀ Quiver.Path.nil = Quiver.Path.nil
• MarshallHall.GeneralGrushko.unfoldSymmLiftPath L e₀ (p.cons e) = (MarshallHall.GeneralGrushko.unfoldSymmLiftPath L e₀ p).comp (MarshallHall.GeneralGrushko.unfoldSymmLiftArrow L e₀ e)

theorem MarshallHall.GeneralGrushko.unfoldSymmLiftArrow_read {G H : Type v} [Group G] [Group H] {V : Type u} [Quiver V] [Quiver.HasInvolutiveReverse V] (L : BinaryLabelling) (e₀ : AllArrow) {x y : Quiver.Symmetrify V} (e : x ⟶ y) : (unfoldLabelling L e₀).pathRead (unfoldSymmLiftArrow L e₀ e) = separatedMap (L.symmLabel e)

theorem MarshallHall.GeneralGrushko.unfoldSymmLiftPath_read {G H : Type v} [Group G] [Group H] {V : Type u} [Quiver V] [Quiver.HasInvolutiveReverse V] (L : BinaryLabelling) (e₀ : AllArrow) {x y : Quiver.Symmetrify V} (p : Quiver.Path x y) : (unfoldLabelling L e₀).pathRead (unfoldSymmLiftPath L e₀ p) = L.symmPathRead p

@[irreducible]

def MarshallHall.GeneralGrushko.unfoldSymmMonochromaticPath {G H : Type v} [Group G] [Group H] {V : Type u} [Quiver V] [Quiver.HasInvolutiveReverse V] (L : BinaryLabelling) (e₀ : AllArrow) (color : Bool) {x y : Quiver.Symmetrify V} (p : Quiver.Path x y) : L.symmIsMonochromatic p color → Quiver.Path (unfoldVertexAt L (allArrowSource e₀) e₀ (have this := x; this) color) (unfoldVertexAt L (allArrowSource e₀) e₀ (have this := y; this) color)

Lifts a monochromatic symmetrized path to its factor side in the unfolded graph.

Equations

• One or more equations did not get rendered due to their size.
• MarshallHall.GeneralGrushko.unfoldSymmMonochromaticPath L e₀ color Quiver.Path.nil x_4 = Quiver.Path.nil

theorem MarshallHall.GeneralGrushko.unfoldSymmMonochromaticPath_read {G H : Type v} [Group G] [Group H] {V : Type u} [Quiver V] [Quiver.HasInvolutiveReverse V] (L : BinaryLabelling) (e₀ : AllArrow) (color : Bool) {x y : Quiver.Symmetrify V} (p : Quiver.Path x y) (hp : L.symmIsMonochromatic p color) : (unfoldLabelling L e₀).pathRead (unfoldSymmMonochromaticPath L e₀ color p hp) = L.symmPathRead p

The duplicated edge and its complementary tail

noncomputable def MarshallHall.GeneralGrushko.unfoldDuplicatePath {G H : Type v} [Group G] [Group H] {V : Type u} [Quiver V] [Quiver.HasInvolutiveReverse V] (L : BinaryLabelling) (e₀ : AllArrow) {b : Quiver.Symmetrify V} (q : Quiver.Path (have this := allArrowTarget e₀; this) b) (hq : L.symmIsMonochromatic q (unfoldEdgeColor L e₀)) : Quiver.Path (unfoldNew (allArrowSource e₀)) (unfoldVertexAt L (allArrowSource e₀) e₀ (have this := b; this) (unfoldEdgeColor L e₀))

The path beginning with the duplicated edge and following the lifted monochromatic continuation.

Equations

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

theorem MarshallHall.GeneralGrushko.unfoldDuplicatePath_read {G H : Type v} [Group G] [Group H] {V : Type u} [Quiver V] [Quiver.HasInvolutiveReverse V] (L : BinaryLabelling) (e₀ : AllArrow) {b : Quiver.Symmetrify V} (q : Quiver.Path (have this := allArrowTarget e₀; this) b) (hq : L.symmIsMonochromatic q (unfoldEdgeColor L e₀)) : (unfoldLabelling L e₀).pathRead (unfoldDuplicatePath L e₀ q hq) = separatedMap (allArrowLabel L e₀) * L.symmPathRead q

def MarshallHall.GeneralGrushko.unfoldPathEdges {G H : Type v} [Group G] [Group H] {V : Type u} [Quiver V] [Quiver.HasInvolutiveReverse V] (L : BinaryLabelling) (e₀ : AllArrow) {x y : UnfoldVertex (allArrowSource e₀)} : Quiver.Path x y → List UnfoldEdge

The list of explicit unfolded edges traversed by a path.

Equations

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

theorem MarshallHall.GeneralGrushko.unfoldPathEdges_comp {G H : Type v} [Group G] [Group H] {V : Type u} [Quiver V] [Quiver.HasInvolutiveReverse V] (L : BinaryLabelling) (e₀ : AllArrow) {x y : UnfoldVertex (allArrowSource e₀)} (p : Quiver.Path x y) {z : UnfoldVertex (allArrowSource e₀)} (q : Quiver.Path y z) : unfoldPathEdges L e₀ (p.comp q) = unfoldPathEdges L e₀ p ++ unfoldPathEdges L e₀ q

theorem MarshallHall.GeneralGrushko.unfoldPathEdges_reverse {G H : Type v} [Group G] [Group H] {V : Type u} [Quiver V] [Quiver.HasInvolutiveReverse V] (L : BinaryLabelling) (e₀ : AllArrow) {x y : UnfoldVertex (allArrowSource e₀)} (p : Quiver.Path x y) : unfoldPathEdges L e₀ p.reverse = List.map unfoldEdgeReverse (unfoldPathEdges L e₀ p).reverse

theorem MarshallHall.GeneralGrushko.unfoldMonochromaticPath_edges_original {G H : Type v} [Group G] [Group H] {V : Type u} [Quiver V] [Quiver.HasInvolutiveReverse V] (L : BinaryLabelling) (e₀ : AllArrow) (color : Bool) {x y : V} (p : Quiver.Path x y) (hp : L.IsMonochromatic p color) (z : UnfoldEdge) : z ∈ unfoldPathEdges L e₀ (unfoldMonochromaticPath L e₀ color p hp) → ∃ (f : AllArrow), z = Sum.inl f

theorem MarshallHall.GeneralGrushko.unfoldSymmMonochromaticPath_edges_original {G H : Type v} [Group G] [Group H] {V : Type u} [Quiver V] [Quiver.HasInvolutiveReverse V] (L : BinaryLabelling) (e₀ : AllArrow) (color : Bool) {x y : Quiver.Symmetrify V} (p : Quiver.Path x y) (hp : L.symmIsMonochromatic p color) (z : UnfoldEdge) : z ∈ unfoldPathEdges L e₀ (unfoldSymmMonochromaticPath L e₀ color p hp) → ∃ (f : AllArrow), z = Sum.inl f

theorem MarshallHall.GeneralGrushko.unfoldPath_avoid_duplicate {G H : Type v} [Group G] [Group H] {V : Type u} [Quiver V] [Quiver.HasInvolutiveReverse V] (L : BinaryLabelling) (e₀ : AllArrow) {x y : UnfoldVertex (allArrowSource e₀)} (r : Quiver.Path x y) (hr : ∀ z ∈ unfoldPathEdges L e₀ r, ∃ (f : AllArrow), z = Sum.inl f) : foldSymmPathAvoid (allArrowOf (unfoldDuplicateForward L e₀)) (Quiver.Symmetrify.of.mapPath r)

noncomputable def MarshallHall.GeneralGrushko.unfoldDuplicateFoldPath {G H : Type v} [Group G] [Group H] {V : Type u} [Quiver V] [Quiver.HasInvolutiveReverse V] (L : BinaryLabelling) (e₀ : AllArrow) {b : Quiver.Symmetrify V} (q : Quiver.Path (have this := allArrowTarget e₀; this) b) (hq : L.symmIsMonochromatic q (unfoldEdgeColor L e₀)) : Quiver.Path (unfoldNew (allArrowSource e₀)) (unfoldVertexAt L (allArrowSource e₀) e₀ (have this := b; this) (unfoldEdgeColor L e₀))

The duplicate-edge detour packaged as a path for the subsequent fold.

Equations

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

theorem MarshallHall.GeneralGrushko.unfoldDuplicateFoldPath_read {G H : Type v} [Group G] [Group H] {V : Type u} [Quiver V] [Quiver.HasInvolutiveReverse V] (L : BinaryLabelling) (e₀ : AllArrow) {b : Quiver.Symmetrify V} (q : Quiver.Path (have this := allArrowTarget e₀; this) b) (hq : L.symmIsMonochromatic q (unfoldEdgeColor L e₀)) : (unfoldLabelling L e₀).symmPathRead (unfoldDuplicateFoldPath L e₀ q hq) = separatedMap (allArrowLabel L e₀) * L.symmPathRead q

theorem MarshallHall.GeneralGrushko.unfold_duplicate_safe_tail {G H : Type v} [Group G] [Group H] {V : Type u} [Quiver V] [Quiver.HasInvolutiveReverse V] (L : BinaryLabelling) (e₀ : AllArrow) {b : Quiver.Symmetrify V} (q : Quiver.Path (have this := allArrowTarget e₀; this) b) (hq : L.symmIsMonochromatic q (unfoldEdgeColor L e₀)) (hread : L.symmPathRead q = (separatedMap (allArrowLabel L e₀))⁻¹) : foldSymmPathAvoid (allArrowOf (unfoldDuplicateForward L e₀)) (Quiver.Symmetrify.of.mapPath (unfoldSymmMonochromaticPath L e₀ (unfoldEdgeColor L e₀) q hq)) ∧ (unfoldLabelling L e₀).symmPathRead (unfoldDuplicateFoldPath L e₀ q hq) = 1

theorem MarshallHall.GeneralGrushko.unfoldDuplicateFoldPath_target_eq_old {G H : Type v} [Group G] [Group H] {V : Type u} [Quiver V] [Quiver.HasInvolutiveReverse V] (L : BinaryLabelling) (e₀ : AllArrow) : unfoldVertexAt L (allArrowSource e₀) e₀ (have this := allArrowSource e₀; this) (unfoldEdgeColor L e₀) = unfoldOld (allArrowSource e₀)

noncomputable def MarshallHall.GeneralGrushko.unfoldedMarkedGraph {G H : Type v} [Group G] [Group H] {V : Type u} [Quiver V] [Quiver.HasInvolutiveReverse V] {n : ℕ} (M : MarkedBinaryGraph n) (e₀ : AllArrow) (ha : allArrowSource e₀ = M.base) : MarkedBinaryGraph n

The unfolded marked graph based at the original copy of its split base vertex.

Equations

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

theorem MarshallHall.GeneralGrushko.unfoldedMarkedGraph_read {G H : Type v} [Group G] [Group H] {V : Type u} [Quiver V] [Quiver.HasInvolutiveReverse V] {n : ℕ} (M : MarkedBinaryGraph n) (e₀ : AllArrow) (ha : allArrowSource e₀ = M.base) (i : Fin n) : (unfoldedMarkedGraph M e₀ ha).read i = M.read i

theorem MarshallHall.GeneralGrushko.unfoldedMarkedGraph_isGenerating {G H : Type v} [Group G] [Group H] {V : Type u} [Quiver V] [Quiver.HasInvolutiveReverse V] {n : ℕ} (M : MarkedBinaryGraph n) (e₀ : AllArrow) (ha : allArrowSource e₀ = M.base) (hgen : M.IsGenerating) : (unfoldedMarkedGraph M e₀ ha).IsGenerating

theorem MarshallHall.GeneralGrushko.unfoldedMarkedGraph_weaklyConnected {G H : Type v} [Group G] [Group H] {V : Type u} [Quiver V] [Quiver.HasInvolutiveReverse V] {n : ℕ} (M : MarkedBinaryGraph n) (e₀ : AllArrow) (ha : allArrowSource e₀ = M.base) (hconn : M.WeaklyConnected) : (unfoldedMarkedGraph M e₀ ha).WeaklyConnected

Rerooting the unfolded marking at the new source

noncomputable def MarshallHall.GeneralGrushko.unfoldedMarkedGraphNew {G H : Type v} [Group G] [Group H] {V : Type u} [Quiver V] [Quiver.HasInvolutiveReverse V] {n : ℕ} (M : MarkedBinaryGraph n) (e₀ : AllArrow) (ha : allArrowSource e₀ = M.base) : MarkedBinaryGraph n

The unfolded marked graph rerooted at the new copy of its split base vertex.

Equations

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

theorem MarshallHall.GeneralGrushko.unfoldedMarkedGraphNew_read {G H : Type v} [Group G] [Group H] {V : Type u} [Quiver V] [Quiver.HasInvolutiveReverse V] {n : ℕ} (M : MarkedBinaryGraph n) (e₀ : AllArrow) (ha : allArrowSource e₀ = M.base) (i : Fin n) : (unfoldedMarkedGraphNew M e₀ ha).read i = M.read i

theorem MarshallHall.GeneralGrushko.unfoldedMarkedGraphNew_isGenerating {G H : Type v} [Group G] [Group H] {V : Type u} [Quiver V] [Quiver.HasInvolutiveReverse V] {n : ℕ} (M : MarkedBinaryGraph n) (e₀ : AllArrow) (ha : allArrowSource e₀ = M.base) (hgen : M.IsGenerating) : (unfoldedMarkedGraphNew M e₀ ha).IsGenerating

theorem MarshallHall.GeneralGrushko.unfoldedMarkedGraphNew_weaklyConnected {G H : Type v} [Group G] [Group H] {V : Type u} [Quiver V] [Quiver.HasInvolutiveReverse V] {n : ℕ} (M : MarkedBinaryGraph n) (e₀ : AllArrow) (ha : allArrowSource e₀ = M.base) (hconn : M.WeaklyConnected) : (unfoldedMarkedGraphNew M e₀ ha).WeaklyConnected

theorem MarshallHall.GeneralGrushko.unfoldNew_ne_sourceAt_color {G H : Type v} [Group G] [Group H] {V : Type u} [Quiver V] [Quiver.HasInvolutiveReverse V] (L : BinaryLabelling) (e₀ : AllArrow) : unfoldNew (allArrowSource e₀) ≠ unfoldVertexAt L (allArrowSource e₀) e₀ (allArrowSource e₀) (unfoldEdgeColor L e₀)

theorem MarshallHall.GeneralGrushko.unfoldNew_ne_vertexAt_of_ne_source {G H : Type v} [Group G] [Group H] {V : Type u} [Quiver V] [Quiver.HasInvolutiveReverse V] (L : BinaryLabelling) (e₀ : AllArrow) {b : Quiver.Symmetrify V} (hb : (have this := b; this) ≠ allArrowSource e₀) : unfoldNew (allArrowSource e₀) ≠ unfoldVertexAt L (allArrowSource e₀) e₀ (have this := b; this) (unfoldEdgeColor L e₀)

The source-unfold branch supplies a safe fold

theorem MarshallHall.GeneralGrushko.exists_safe_fold_after_unfold {G H : Type v} [Group G] [Group H] {V : Type u} [Fintype V] [Quiver V] [Quiver.HasInvolutiveReverse V] {n : ℕ} (M : MarkedBinaryGraph n) (e₀ : AllArrow) (ha : allArrowSource e₀ = M.base) {b : Quiver.Symmetrify V} (q : Quiver.Path (have this := allArrowTarget e₀; this) b) (hb : (have this := b; this) ≠ allArrowSource e₀) (hq : M.labeling.symmIsMonochromatic q (unfoldEdgeColor M.labeling e₀)) (hread : M.labeling.symmPathRead q = (separatedMap (allArrowLabel M.labeling e₀))⁻¹) (hgen : M.IsGenerating) (hconn : M.WeaklyConnected) : ∃ (e₁ : AllArrow) (ha₁ : allArrowSource e₁ = unfoldNew (allArrowSource e₀)) (q₁ : Quiver.Path (Quiver.Symmetrify.of.obj (allArrowTarget e₁)) (Quiver.Symmetrify.of.obj (unfoldVertexAt M.labeling (allArrowSource e₀) e₀ (have this := b; this) (unfoldEdgeColor M.labeling e₀)))) (hq₁ : foldSymmPathAvoid e₁ q₁), (foldedMarkedGraphSymm (unfoldedMarkedGraphNew M e₀ ha) e₁ ha₁ q₁ hq₁).IsGenerating ∧ (foldedMarkedGraphSymm (unfoldedMarkedGraphNew M e₀ ha) e₁ ha₁ q₁ hq₁).WeaklyConnected ∧ Fintype.card (foldVertex (unfoldNew (allArrowSource e₀)) (unfoldVertexAt M.labeling (allArrowSource e₀) e₀ (have this := b; this) (unfoldEdgeColor M.labeling e₀))) < Fintype.card (UnfoldVertex (allArrowSource e₀))