Presentations of a vertex wedge

VertexWedgePresentation records the data needed to recognize an ambient graph as a wedge of two graphs at distinguished vertices. It is deliberately stated using edge multiplicities, so it can be used without choosing an orientation of the raw edge multisets.

structure Utilities.VertexWedgePresentation (K : CFGraph) (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) : Type (max (max u v) w)

A presentation of K as the wedge of G and H, identifying x with y.

• leftMap : G.V → K.V

  The injective, edge-multiplicity-preserving placement of the left factor into the presented wedge.

• rightMap : H.V → K.V

  The injective placement of the right factor, identifying only its marked vertex with the left factor's mark.

• left_injective : Function.Injective self.leftMap
• right_injective : Function.Injective self.rightMap
• marked_eq : self.leftMap x = self.rightMap y
• only_overlap (a : G.V) (b : H.V) : self.leftMap a = self.rightMap b → a = x ∧ b = y
• vertex_cover (z : K.V) : (∃ (a : G.V), self.leftMap a = z) ∨ ∃ (b : H.V), self.rightMap b = z
• num_edges_left (a b : G.V) : numEdges K (self.leftMap a) (self.leftMap b) = numEdges G a b
• num_edges_right (a b : H.V) : numEdges K (self.rightMap a) (self.rightMap b) = numEdges H a b
• num_edges_cross (a : G.V) (b : H.V) : b ≠ y → numEdges K (self.leftMap a) (self.rightMap b) = if a = x then numEdges H y b else 0

def Utilities.VertexWedgePresentation.canonical (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) : VertexWedgePresentation (vertexWedge G H x y) G H x y

The concrete vertex wedge carries its tautological presentation. Besides being useful in compositions, this witnesses that the presentation fields do not impose any unintended restrictions at the common vertex.

Equations

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

def Utilities.VertexWedgePresentation.map {K : CFGraph} {G : CFGraph} {H : CFGraph} {x : G.V} {y : H.V} (P : VertexWedgePresentation K G H x y) : (vertexWedge G H x y).V → K.V

The map from the concrete wedge vertex type into a presented ambient graph.

Equations

• P.map = Sum.elim P.leftMap fun (b : { b : H.V // b ≠ y }) => P.rightMap ↑b

@[simp]

theorem Utilities.VertexWedgePresentation.map_left {K : CFGraph} {G : CFGraph} {H : CFGraph} {x : G.V} {y : H.V} (P : VertexWedgePresentation K G H x y) (a : G.V) : P.map (Sum.inl a) = P.leftMap a

@[simp]

theorem Utilities.VertexWedgePresentation.map_right {K : CFGraph} {G : CFGraph} {H : CFGraph} {x : G.V} {y : H.V} (P : VertexWedgePresentation K G H x y) (b : { b : H.V // b ≠ y }) : P.map (Sum.inr b) = P.rightMap ↑b

theorem Utilities.VertexWedgePresentation.map_injective {K : CFGraph} {G : CFGraph} {H : CFGraph} {x : G.V} {y : H.V} (P : VertexWedgePresentation K G H x y) : Function.Injective P.map

theorem Utilities.VertexWedgePresentation.map_surjective {K : CFGraph} {G : CFGraph} {H : CFGraph} {x : G.V} {y : H.V} (P : VertexWedgePresentation K G H x y) : Function.Surjective P.map

noncomputable def Utilities.VertexWedgePresentation.vertexEquiv {K : CFGraph} {G : CFGraph} {H : CFGraph} {x : G.V} {y : H.V} (P : VertexWedgePresentation K G H x y) : (vertexWedge G H x y).V ≃ K.V

The vertex equivalence induced by a wedge presentation.

Equations

• P.vertexEquiv = Equiv.ofBijective P.map ⋯

@[simp]

theorem Utilities.VertexWedgePresentation.vertexEquiv_left {K : CFGraph} {G : CFGraph} {H : CFGraph} {x : G.V} {y : H.V} (P : VertexWedgePresentation K G H x y) (a : G.V) : P.vertexEquiv (Sum.inl a) = P.leftMap a

@[simp]

theorem Utilities.VertexWedgePresentation.vertexEquiv_right {K : CFGraph} {G : CFGraph} {H : CFGraph} {x : G.V} {y : H.V} (P : VertexWedgePresentation K G H x y) (b : { b : H.V // b ≠ y }) : P.vertexEquiv (Sum.inr b) = P.rightMap ↑b

@[simp]

theorem Utilities.VertexWedgePresentation.vertexEquiv_wedgeRightVertex {K : CFGraph} {G : CFGraph} {H : CFGraph} {x : G.V} {y : H.V} (P : VertexWedgePresentation K G H x y) (b : H.V) : P.vertexEquiv (wedgeRightVertex G H x y b) = P.rightMap b

The whole right-factor vertex map, including the identified vertex, is carried to the advertised ambient map.

noncomputable def Utilities.VertexWedgePresentation.graphIso {K : CFGraph} {G : CFGraph} {H : CFGraph} {x : G.V} {y : H.V} (P : VertexWedgePresentation K G H x y) : CFGraphIso (vertexWedge G H x y) K

A wedge presentation determines an isomorphism from the concrete wedge to the ambient graph.

Equations

• P.graphIso = { vertexEquiv := P.vertexEquiv, map_num_edges := ⋯ }

@[simp]

theorem Utilities.VertexWedgePresentation.graphIso_apply_left {K : CFGraph} {G : CFGraph} {H : CFGraph} {x : G.V} {y : H.V} (P : VertexWedgePresentation K G H x y) (a : G.V) : P.graphIso.vertexEquiv (Sum.inl a) = P.leftMap a

@[simp]

theorem Utilities.VertexWedgePresentation.graphIso_apply_right {K : CFGraph} {G : CFGraph} {H : CFGraph} {x : G.V} {y : H.V} (P : VertexWedgePresentation K G H x y) (b : { b : H.V // b ≠ y }) : P.graphIso.vertexEquiv (Sum.inr b) = P.rightMap ↑b

@[simp]

theorem Utilities.VertexWedgePresentation.graphIso_apply_wedgeRightVertex {K : CFGraph} {G : CFGraph} {H : CFGraph} {x : G.V} {y : H.V} (P : VertexWedgePresentation K G H x y) (b : H.V) : P.graphIso.vertexEquiv (wedgeRightVertex G H x y b) = P.rightMap b

theorem Utilities.VertexWedgePresentation.genus_eq {K : CFGraph} {G : CFGraph} {H : CFGraph} {x : G.V} {y : H.V} (P : VertexWedgePresentation K G H x y) : K.genus = G.genus + H.genus

The presented graph has the genus expected of the two factors.

theorem Utilities.VertexWedgePresentation.graph_connected_iff {K : CFGraph} {G : CFGraph} {H : CFGraph} {x : G.V} {y : H.V} (P : VertexWedgePresentation K G H x y) : graphConnected K ↔ graphConnected (vertexWedge G H x y)

Connectivity of the presented graph is equivalent to connectivity of its concrete wedge.

theorem Utilities.VertexWedgePresentation.graph_connected_of_factors {K : CFGraph} {G : CFGraph} {H : CFGraph} {x : G.V} {y : H.V} (P : VertexWedgePresentation K G H x y) (hG : graphConnected G) (hH : graphConnected H) : graphConnected K

Connected factors give a connected presented ambient graph.

theorem Utilities.VertexWedgePresentation.BNExists_iff {K : CFGraph} {G : CFGraph} {H : CFGraph} {x : G.V} {y : H.V} (P : VertexWedgePresentation K G H x y) (r d : ℤ) : BNExists K r d ↔ BNExists (vertexWedge G H x y) r d

Brill--Noether existence on a presented graph is exactly existence on its concrete wedge model, at every rank and degree.