Edge labelings

This module defines labelings of the edges of a graph.

Main definitions

• SimpleGraph.EdgeLabeling: An assignment of a label from a given type to each edge of the graph.

• SimpleGraph.EdgeLabeling.labelGraph: the graph consisting of all edges with a given label.

def SimpleGraph.EdgeLabeling {V : Type u_1} (G : SimpleGraph V) (K : Type u_5) : Type (max u_1 u_5)

An edge labeling of a simple graph G with labels in type K. Sometimes this is called an edge-colouring, but we reserve that terminology for labelings where incident edges cannot share a label.

Equations

• G.EdgeLabeling K = (↑G.edgeSet → K)

instance SimpleGraph.instFintypeEdgeLabelingOfDecidableEqOfElemSym2EdgeSet {V : Type u_1} {G : SimpleGraph V} {K : Type u_3} [DecidableEq V] [Fintype ↑G.edgeSet] [Fintype K] : Fintype (G.EdgeLabeling K)

Equations

• SimpleGraph.instFintypeEdgeLabelingOfDecidableEqOfElemSym2EdgeSet = Pi.instFintype

instance SimpleGraph.instFiniteEdgeLabelingOfElemSym2EdgeSet {V : Type u_1} {G : SimpleGraph V} {K : Type u_3} [Finite ↑G.edgeSet] [Finite K] : Finite (G.EdgeLabeling K)

instance SimpleGraph.instNonemptyEdgeLabeling {V : Type u_1} {G : SimpleGraph V} {K : Type u_3} [Nonempty K] : Nonempty (G.EdgeLabeling K)

instance SimpleGraph.instInhabitedEdgeLabeling {V : Type u_1} {G : SimpleGraph V} {K : Type u_3} [Inhabited K] : Inhabited (G.EdgeLabeling K)

Equations

• SimpleGraph.instInhabitedEdgeLabeling = Pi.instInhabited

instance SimpleGraph.instSubsingletonEdgeLabeling {V : Type u_1} {G : SimpleGraph V} {K : Type u_3} [Subsingleton K] : Subsingleton (G.EdgeLabeling K)

instance SimpleGraph.instNontrivialEdgeLabelingOfNonemptyElemSym2EdgeSet {V : Type u_1} {G : SimpleGraph V} {K : Type u_3} [Nonempty ↑G.edgeSet] [Nontrivial K] : Nontrivial (G.EdgeLabeling K)

instance SimpleGraph.instUniqueEdgeLabeling {V : Type u_1} {G : SimpleGraph V} {K : Type u_3} [Unique K] : Unique (G.EdgeLabeling K)

Equations

• SimpleGraph.instUniqueEdgeLabeling = Pi.unique

@[reducible, inline]

abbrev SimpleGraph.TopEdgeLabeling (V : Type u_5) (K : Type u_6) : Type (max u_5 u_6)

An edge labeling of the complete graph on V with labels in type K.

Equations

• SimpleGraph.TopEdgeLabeling V K = ⊤.EdgeLabeling K

theorem SimpleGraph.card_topEdgeLabeling {V : Type u_1} {K : Type u_3} [DecidableEq V] [Fintype V] [Fintype K] : Fintype.card (TopEdgeLabeling V K) = Fintype.card K ^ (Fintype.card V).choose 2

def SimpleGraph.EdgeLabeling.get {V : Type u_1} {G : SimpleGraph V} {K : Type u_3} (C : G.EdgeLabeling K) (x y : V) (h : G.Adj x y) : K

Convenience function to get the colour of the edge x ~ y in the colouring of the complete graph on V.

Equations

• C.get x y h = C ⟨s(x, y), h⟩

theorem SimpleGraph.EdgeLabeling.get_eq {V : Type u_1} {G : SimpleGraph V} {K : Type u_3} (C : G.EdgeLabeling K) (x y : V) (h : G.Adj x y) : C.get x y h = C ⟨s(x, y), h⟩

theorem SimpleGraph.EdgeLabeling.get_comm {V : Type u_1} {G : SimpleGraph V} {K : Type u_3} {C : G.EdgeLabeling K} (x y : V) (h : G.Adj y x) : C.get y x h = C.get x y ⋯

theorem SimpleGraph.EdgeLabeling.ext_get {V : Type u_1} {G : SimpleGraph V} {K : Type u_3} {C C' : G.EdgeLabeling K} (h : ∀ (x y : V) (h : G.Adj x y), C.get x y h = C'.get x y h) : C = C'

theorem SimpleGraph.EdgeLabeling.ext_get_iff {V : Type u_1} {G : SimpleGraph V} {K : Type u_3} {C C' : G.EdgeLabeling K} : C = C' ↔ ∀ (x y : V) (h : G.Adj x y), C.get x y h = C'.get x y h

def SimpleGraph.EdgeLabeling.compRight {V : Type u_1} {G : SimpleGraph V} {K : Type u_3} {K' : Type u_4} (C : G.EdgeLabeling K) (f : K → K') : G.EdgeLabeling K'

Compose an edge-labeling with a function on the colour set.

Equations

• C.compRight f = f ∘ C

def SimpleGraph.EdgeLabeling.pullback {V : Type u_1} {V' : Type u_2} {G : SimpleGraph V} {G' : SimpleGraph V'} {K : Type u_3} (C : G.EdgeLabeling K) (f : G' →g G) : G'.EdgeLabeling K

Compose an edge-labeling with a graph embedding.

Equations

• C.pullback f = C ∘ f.mapEdgeSet

@[simp]

theorem SimpleGraph.EdgeLabeling.pullback_apply {V : Type u_1} {V' : Type u_2} {G : SimpleGraph V} {G' : SimpleGraph V'} {K : Type u_3} {C : G.EdgeLabeling K} {f : G' →g G} (e : ↑G'.edgeSet) : C.pullback f e = C (f.mapEdgeSet e)

@[simp]

theorem SimpleGraph.EdgeLabeling.get_pullback {V : Type u_1} {V' : Type u_2} {G : SimpleGraph V} {G' : SimpleGraph V'} {K : Type u_3} {C : G.EdgeLabeling K} {f : G' ↪g G} (x y : V') (h : G'.Adj x y) : (C.pullback (RelEmbedding.toRelHom f)).get x y h = C.get (f x) (f y) ⋯

@[simp]

theorem SimpleGraph.EdgeLabeling.compRight_apply {V : Type u_1} {G : SimpleGraph V} {K : Type u_3} {K' : Type u_4} {C : G.EdgeLabeling K} (f : K → K') (e : ↑G.edgeSet) : C.compRight f e = f (C e)

@[simp]

theorem SimpleGraph.EdgeLabeling.compRight_get {V : Type u_1} {G : SimpleGraph V} {K : Type u_3} {K' : Type u_4} {C : G.EdgeLabeling K} (f : K → K') (x y : V) (h : G.Adj x y) : (C.compRight f).get x y h = f (C.get x y h)

def SimpleGraph.EdgeLabeling.mk {V : Type u_1} {G : SimpleGraph V} {K : Type u_3} (f : (x y : V) → G.Adj x y → K) (f_symm : ∀ (x y : V) (H : G.Adj x y), f y x ⋯ = f x y H) : G.EdgeLabeling K

Construct an edge labeling from a symmetric function on adjacent vertices.

Equations

• SimpleGraph.EdgeLabeling.mk f f_symm ⟨e, he⟩ = Sym2.hrec (motive := fun (x : Sym2 V) => x ∈ G.edgeSet → K) (fun (xy : V × V) => f xy.1 xy.2) ⋯ e he

theorem SimpleGraph.EdgeLabeling.get_mk {V : Type u_1} {G : SimpleGraph V} {K : Type u_3} (f : (x y : V) → G.Adj x y → K) (f_symm : ∀ (x y : V) (H : G.Adj x y), f y x ⋯ = f x y H) (x y : V) (h : G.Adj x y) : (mk f f_symm).get x y h = f x y h

def SimpleGraph.EdgeLabeling.labelGraph {V : Type u_1} {G : SimpleGraph V} {K : Type u_3} (C : G.EdgeLabeling K) (k : K) : SimpleGraph V

Given an edge labeling and a choice of label k, construct the graph corresponding to the edges labeled k.

Equations

• C.labelGraph k = SimpleGraph.fromEdgeSet {e : Sym2 V | ∃ (h : e ∈ G.edgeSet), C ⟨e, h⟩ = k}

theorem SimpleGraph.EdgeLabeling.labelGraph_adj {V : Type u_1} {G : SimpleGraph V} {K : Type u_3} {C : G.EdgeLabeling K} {k : K} (x y : V) : (C.labelGraph k).Adj x y ↔ ∃ (H : G.Adj x y), C ⟨s(x, y), H⟩ = k

instance SimpleGraph.EdgeLabeling.instDecidableRelAdjLabelGraphOfDecidableEq {V : Type u_1} {G : SimpleGraph V} {K : Type u_3} [DecidableRel G.Adj] [DecidableEq K] (k : K) {C : G.EdgeLabeling K} : DecidableRel (C.labelGraph k).Adj

Equations

• SimpleGraph.EdgeLabeling.instDecidableRelAdjLabelGraphOfDecidableEq k x✝¹ x✝ = decidable_of_iff' (∃ (H : G.Adj x✝¹ x✝), C ⟨s(x✝¹, x✝), H⟩ = k) ⋯

theorem SimpleGraph.EdgeLabeling.labelGraph_le {V : Type u_1} {G : SimpleGraph V} {K : Type u_3} (C : G.EdgeLabeling K) {k : K} : C.labelGraph k ≤ G

theorem SimpleGraph.EdgeLabeling.pairwise_disjoint_labelGraph {V : Type u_1} {G : SimpleGraph V} {K : Type u_3} {C : G.EdgeLabeling K} : Pairwise fun (k l : K) => Disjoint (C.labelGraph k) (C.labelGraph l)

theorem SimpleGraph.EdgeLabeling.pairwiseDisjoint_univ_labelGraph {V : Type u_1} {G : SimpleGraph V} {K : Type u_3} {C : G.EdgeLabeling K} : Set.univ.PairwiseDisjoint C.labelGraph

theorem SimpleGraph.EdgeLabeling.iSup_labelGraph {V : Type u_1} {G : SimpleGraph V} {K : Type u_3} (C : G.EdgeLabeling K) : ⨆ (k : K), C.labelGraph k = G

@[reducible, inline]

abbrev SimpleGraph.TopEdgeLabeling.pullback {V : Type u_1} {V' : Type u_2} {K : Type u_3} (C : TopEdgeLabeling V K) (f : V' ↪ V) : TopEdgeLabeling V' K

Compose an edge-labeling, by an injection into the vertex type. This must be an injection, else we don't know how to colour x ~ y in the case f x = f y.

Equations

• C.pullback f = SimpleGraph.EdgeLabeling.pullback C { toFun := ⇑f, map_rel' := ⋯ }

@[simp]

theorem SimpleGraph.TopEdgeLabeling.labelGraph_adj {V : Type u_1} {K : Type u_3} {C : TopEdgeLabeling V K} {k : K} (x y : V) : (EdgeLabeling.labelGraph C k).Adj x y ↔ ∃ (H : x ≠ y), EdgeLabeling.get C x y H = k

def SimpleGraph.toTopEdgeLabeling {V : Type u_1} (G : SimpleGraph V) [DecidableRel G.Adj] : TopEdgeLabeling V (Fin 2)

From a simple graph on V, construct the edge labeling on the complete graph of V given where edges are labeled 1 and non-edges are labeled 0.

Equations

• G.toTopEdgeLabeling = SimpleGraph.EdgeLabeling.mk (fun (x y : V) (x_1 : ⊤.Adj x y) => if G.Adj x y then 1 else 0) ⋯

@[simp]

theorem SimpleGraph.toTopEdgeLabeling_get {V : Type u_1} {G : SimpleGraph V} [DecidableRel G.Adj] {x y : V} (H : x ≠ y) : EdgeLabeling.get G.toTopEdgeLabeling x y H = if G.Adj x y then 1 else 0

@[simp]

theorem SimpleGraph.toTopEdgeLabeling_labelGraph {V : Type u_1} (G : SimpleGraph V) [DecidableRel G.Adj] : EdgeLabeling.labelGraph G.toTopEdgeLabeling 1 = G

@[simp]

theorem SimpleGraph.toTopEdgeLabeling_labelGraph_compl {V : Type u_1} (G : SimpleGraph V) [DecidableRel G.Adj] : EdgeLabeling.labelGraph G.toTopEdgeLabeling 0 = Gᶜ

theorem SimpleGraph.TopEdgeLabeling.labelGraph_toTopEdgeLabeling {V : Type u_1} [DecidableEq V] (C : TopEdgeLabeling V (Fin 2)) : (EdgeLabeling.labelGraph C 1).toTopEdgeLabeling = C