Associativity of vertex wedges

The concrete vertexWedge constructor retains every vertex of the left factor and every vertex of the right factor except its attachment vertex. Consequently, both bracketings of a three-factor wedge have the same three classes of vertices. This file records the resulting graph isomorphism.

def Bananas.vertexWedgeAssocVertexEquiv (G : CFGraph) (H : CFGraph) (K : CFGraph) (x : G.V) (y z : H.V) (t : K.V) : (Utilities.vertexWedge (Utilities.vertexWedge G H x y) K (Utilities.wedgeRightVertex G H x y z) t).V ≃ (Utilities.vertexWedge G (Utilities.vertexWedge H K z t) x (Sum.inl y)).V

Rebracket the concrete vertex types underlying a three-factor wedge.

Equations

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

@[simp]

theorem Bananas.vertexWedgeAssocVertexEquiv_apply_first (G : CFGraph) (H : CFGraph) (K : CFGraph) (x : G.V) (y z : H.V) (t : K.V) (a : G.V) : (vertexWedgeAssocVertexEquiv G H K x y z t) (Sum.inl (Sum.inl a)) = Sum.inl a

def Bananas.vertexWedgeAssocMiddleVertex (H : CFGraph) (K : CFGraph) (y z : H.V) (t : K.V) (b : { b : H.V // b ≠ y }) : { q : (Utilities.vertexWedge H K z t).V // q ≠ Sum.inl y }

The unglued middle-factor vertex viewed in the right-associated outer wedge's unmarked right subtype.

Equations

• Bananas.vertexWedgeAssocMiddleVertex H K y z t b = ⟨Sum.inl ↑b, ⋯⟩

def Bananas.vertexWedgeAssocLastVertex (H : CFGraph) (K : CFGraph) (y z : H.V) (t : K.V) (c : { c : K.V // c ≠ t }) : { q : (Utilities.vertexWedge H K z t).V // q ≠ Sum.inl y }

The unglued last-factor vertex viewed in the right-associated outer wedge's unmarked right subtype.

Equations

• Bananas.vertexWedgeAssocLastVertex H K y z t c = ⟨Sum.inr ⟨↑c, ⋯⟩, ⋯⟩

@[simp]

theorem Bananas.vertexWedgeAssocMiddleVertex_val (H : CFGraph) (K : CFGraph) (y z : H.V) (t : K.V) (b : { b : H.V // b ≠ y }) : ↑(vertexWedgeAssocMiddleVertex H K y z t b) = Sum.inl ↑b

@[simp]

theorem Bananas.vertexWedgeAssocLastVertex_val (H : CFGraph) (K : CFGraph) (y z : H.V) (t : K.V) (c : { c : K.V // c ≠ t }) : ↑(vertexWedgeAssocLastVertex H K y z t c) = Sum.inr c

@[simp]

theorem Bananas.vertexWedgeAssocVertexEquiv_apply_middle (G : CFGraph) (H : CFGraph) (K : CFGraph) (x : G.V) (y z : H.V) (t : K.V) (b : { b : H.V // b ≠ y }) : (vertexWedgeAssocVertexEquiv G H K x y z t) (Sum.inl (Sum.inr b)) = Sum.inr (vertexWedgeAssocMiddleVertex H K y z t b)

@[simp]

theorem Bananas.vertexWedgeAssocVertexEquiv_apply_last (G : CFGraph) (H : CFGraph) (K : CFGraph) (x : G.V) (y z : H.V) (t : K.V) (c : { c : K.V // c ≠ t }) : (vertexWedgeAssocVertexEquiv G H K x y z t) (Sum.inr c) = Sum.inr (vertexWedgeAssocLastVertex H K y z t c)

@[simp]

theorem Bananas.num_edges_vertexWedge_right_left (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) (b : { b : H.V // b ≠ y }) (a : G.V) : numEdges (Utilities.vertexWedge G H x y) (Sum.inr b) (Sum.inl a) = if a = x then numEdges H y ↑b else 0

The symmetric orientation of num_edges_vertexWedge_left_right.

@[simp]

theorem Bananas.wedgeLeft_eq_wedgeRightVertex_iff (G : CFGraph) (H : CFGraph) (x : G.V) (y b : H.V) (a : G.V) : Sum.inl a = Utilities.wedgeRightVertex G H x y b ↔ b = y ∧ a = x

@[simp]

theorem Bananas.wedgeUnmarkedRight_eq_wedgeRightVertex_iff (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) (q : { q : H.V // q ≠ y }) (b : H.V) : Sum.inr q = Utilities.wedgeRightVertex G H x y b ↔ ↑q = b

def Bananas.vertexWedgeAssoc (G : CFGraph) (H : CFGraph) (K : CFGraph) (x : G.V) (y z : H.V) (t : K.V) : Utilities.CFGraphIso (Utilities.vertexWedge (Utilities.vertexWedge G H x y) K (Utilities.wedgeRightVertex G H x y z) t) (Utilities.vertexWedge G (Utilities.vertexWedge H K z t) x (Sum.inl y))

Vertex-wedge associativity as an isomorphism of chip-firing graphs.

The middle graph is glued to G at y and to K at z; no hypothesis that these two vertices are distinct is needed.

Equations

• Bananas.vertexWedgeAssoc G H K x y z t = { vertexEquiv := Bananas.vertexWedgeAssocVertexEquiv G H K x y z t, map_num_edges := ⋯ }

theorem Bananas.brillNoetherGeneral_iff_graphIso {G : CFGraph} {H : CFGraph} (equivalence : Utilities.CFGraphIso G H) : BrillNoetherGeneral H ↔ BrillNoetherGeneral G

Brill--Noether generality is invariant under graph isomorphism.

theorem Bananas.brillNoetherGeneral_vertexWedge_assoc_iff (G : CFGraph) (H : CFGraph) (K : CFGraph) (x : G.V) (y z : H.V) (t : K.V) : BrillNoetherGeneral (Utilities.vertexWedge G (Utilities.vertexWedge H K z t) x (Sum.inl y)) ↔ BrillNoetherGeneral (Utilities.vertexWedge (Utilities.vertexWedge G H x y) K (Utilities.wedgeRightVertex G H x y z) t)

Brill--Noether generality does not depend on the bracketing of a three-factor vertex wedge.