Functoriality of basic graph constructors

The bridge and wedge constructors respect graph isomorphisms of their factors, including the distinguished attachment vertices. The wedge proof uses its presentation interface so that the dependent subtype of unmarked right vertices never has to be relabelled directly.

def Utilities.CFGraphIso.bridgeGraphCongr {G : CFGraph} {G' : CFGraph} {H : CFGraph} {H' : CFGraph} (φ : CFGraphIso G G') (ψ : CFGraphIso H H') (a : G.V) (b : H.V) : CFGraphIso (bridgeGraph G H a b) (bridgeGraph G' H' (φ.vertexEquiv a) (ψ.vertexEquiv b))

Relabel both factors of a separating bridge.

Equations

• φ.bridgeGraphCongr ψ a b = { vertexEquiv := φ.vertexEquiv.sumCongr ψ.vertexEquiv, map_num_edges := ⋯ }

@[simp]

theorem Utilities.CFGraphIso.bridgeGraphCongr_apply_left {G : CFGraph} {G' : CFGraph} {H : CFGraph} {H' : CFGraph} (φ : CFGraphIso G G') (ψ : CFGraphIso H H') (a : G.V) (b : H.V) (x : G.V) : (φ.bridgeGraphCongr ψ a b).vertexEquiv (Sum.inl x) = Sum.inl (φ.vertexEquiv x)

@[simp]

theorem Utilities.CFGraphIso.bridgeGraphCongr_apply_right {G : CFGraph} {G' : CFGraph} {H : CFGraph} {H' : CFGraph} (φ : CFGraphIso G G') (ψ : CFGraphIso H H') (a : G.V) (b y : H.V) : (φ.bridgeGraphCongr ψ a b).vertexEquiv (Sum.inr y) = Sum.inr (ψ.vertexEquiv y)

noncomputable def Utilities.CFGraphIso.vertexWedgeCongrPresentation {G : CFGraph} {G' : CFGraph} {H : CFGraph} {H' : CFGraph} (φ : CFGraphIso G G') (ψ : CFGraphIso H H') (a : G.V) (b : H.V) : VertexWedgePresentation (vertexWedge G' H' (φ.vertexEquiv a) (ψ.vertexEquiv b)) G H a b

A presentation of the relabelled wedge by the original two factors.

Equations

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

noncomputable def Utilities.CFGraphIso.vertexWedgeCongr {G : CFGraph} {G' : CFGraph} {H : CFGraph} {H' : CFGraph} (φ : CFGraphIso G G') (ψ : CFGraphIso H H') (a : G.V) (b : H.V) : CFGraphIso (vertexWedge G H a b) (vertexWedge G' H' (φ.vertexEquiv a) (ψ.vertexEquiv b))

Relabel both factors of a vertex wedge.

Equations

• φ.vertexWedgeCongr ψ a b = (φ.vertexWedgeCongrPresentation ψ a b).graphIso

@[simp]

theorem Utilities.CFGraphIso.vertexWedgeCongr_apply_left {G : CFGraph} {G' : CFGraph} {H : CFGraph} {H' : CFGraph} (φ : CFGraphIso G G') (ψ : CFGraphIso H H') (a : G.V) (b : H.V) (x : G.V) : (φ.vertexWedgeCongr ψ a b).vertexEquiv (Sum.inl x) = Sum.inl (φ.vertexEquiv x)

@[simp]

theorem Utilities.CFGraphIso.vertexWedgeCongr_apply_right {G : CFGraph} {G' : CFGraph} {H : CFGraph} {H' : CFGraph} (φ : CFGraphIso G G') (ψ : CFGraphIso H H') (a : G.V) (b y : H.V) : (φ.vertexWedgeCongr ψ a b).vertexEquiv (wedgeRightVertex G H a b y) = wedgeRightVertex G' H' (φ.vertexEquiv a) (ψ.vertexEquiv b) (ψ.vertexEquiv y)