Extending edge data by zero along a copy

Let f be a copy of a graph H in a graph G, that is an injective graph homomorphism, not necessarily induced. A family β x y of values on the ordered pairs of vertices of H extends by zero to G: the extended family takes the value β x y on (f x, f y) for every edge x ∼ y of H, and zero on every other pair, including the pairs of G-adjacent vertices of the copy which are not edges of H.

When the values lie in a semiring, the local sums ∑_{w ∼ v} β w v * β v w over the neighbours of a vertex are preserved: at a vertex f x of the copy the extended sum is the sum of H at x, and away from the copy it is zero. These are the local relations of the signless preprojective algebra, so a representation of the signless preprojective algebra of H by such a family extends by zero to one of G.

Main definitions

• SimpleGraph.Copy.extendByZero: the extension by zero of a family on the vertex pairs of H along a copy of H in G.

Main results

• SimpleGraph.Copy.extendByZero_apply_apply: along the copy, the extension is the original family on edges of H and zero elsewhere.
• SimpleGraph.Copy.sum_extendByZero_mul_extendByZero: the local sums ∑_{w ∼ v} β w v * β v w vanish for the extension when they vanish for the original family.

def SimpleGraph.Copy.extendByZero {V : Type u_1} {W : Type u_2} {M : Type u_3} {G : SimpleGraph V} {H : SimpleGraph W} [AddCommMonoid M] [Fintype W] [DecidableEq V] [DecidableRel H.Adj] (f : H.Copy G) (β : W → W → M) : V → V → M

The extension by zero of a family β on the vertex pairs of H along a copy f of H in G: the pair (f x, f y) of an edge x ∼ y of H carries β x y, and every other pair carries zero.

theorem SimpleGraph.Copy.extendByZero_apply_apply {V : Type u_1} {W : Type u_2} {M : Type u_3} {G : SimpleGraph V} {H : SimpleGraph W} [AddCommMonoid M] [Fintype W] [DecidableEq V] [DecidableRel H.Adj] (f : H.Copy G) (β : W → W → M) (x y : W) : f.extendByZero β (f x) (f y) = if H.Adj x y then β x y else 0

Along the copy, the extension is the original family on edges of H, and zero elsewhere.

@[simp]

theorem SimpleGraph.Copy.extendByZero_apply_apply_of_adj {V : Type u_1} {W : Type u_2} {M : Type u_3} {G : SimpleGraph V} {H : SimpleGraph W} [AddCommMonoid M] [Fintype W] [DecidableEq V] [DecidableRel H.Adj] (f : H.Copy G) (β : W → W → M) {x y : W} (h : H.Adj x y) : f.extendByZero β (f x) (f y) = β x y

Along an edge of H, the extension is the original family.

theorem SimpleGraph.Copy.extendByZero_apply_apply_of_not_adj {V : Type u_1} {W : Type u_2} {M : Type u_3} {G : SimpleGraph V} {H : SimpleGraph W} [AddCommMonoid M] [Fintype W] [DecidableEq V] [DecidableRel H.Adj] (f : H.Copy G) (β : W → W → M) {x y : W} (h : ¬H.Adj x y) : f.extendByZero β (f x) (f y) = 0

Along a pair of vertices of the copy which is not an edge of H, the extension vanishes.

theorem SimpleGraph.Copy.extendByZero_eq_zero_of_notMem_range_left {V : Type u_1} {W : Type u_2} {M : Type u_3} {G : SimpleGraph V} {H : SimpleGraph W} [AddCommMonoid M] [Fintype W] [DecidableEq V] [DecidableRel H.Adj] (f : H.Copy G) (β : W → W → M) {v : V} (hv : v ∉ Set.range ⇑f) (w : V) : f.extendByZero β v w = 0

Away from the image of the copy, the extension vanishes.

theorem SimpleGraph.Copy.extendByZero_eq_zero_of_notMem_range_right {V : Type u_1} {W : Type u_2} {M : Type u_3} {G : SimpleGraph V} {H : SimpleGraph W} [AddCommMonoid M] [Fintype W] [DecidableEq V] [DecidableRel H.Adj] (f : H.Copy G) (β : W → W → M) (v : V) {w : V} (hw : w ∉ Set.range ⇑f) : f.extendByZero β v w = 0

Away from the image of the copy, the extension vanishes.

theorem SimpleGraph.Copy.sum_extendByZero_mul_extendByZero {V : Type u_1} {W : Type u_2} {M : Type u_3} {G : SimpleGraph V} {H : SimpleGraph W} [NonUnitalNonAssocSemiring M] [Fintype W] [DecidableEq V] [DecidableRel H.Adj] (f : H.Copy G) (β : W → W → M) [Fintype V] [DecidableRel G.Adj] (hβ : ∀ (x : W), ∑ y ∈ H.neighborFinset x, β y x * β x y = 0) (v : V) : ∑ w ∈ G.neighborFinset v, f.extendByZero β w v * f.extendByZero β v w = 0

Local relations extend by zero along a copy: if the sums ∑_{y ∼ x} β y x * β x y over the neighbours in H vanish at every vertex of H, then so do the corresponding sums of the extension by zero at every vertex of G.