Unit-distance graph embeddings

An embedding of a graph into some metric space is unit-distance if the distance between any two adjacent vertices is 1. The space in question is usually the Euclidean plane, but can also be higher-dimensional Euclidean space or the sphere (cf. [FKS20]). We do not require nonadjacent vertices to not be distance 1 apart as [HI14] does.

Main definitions

• G.UnitDistEmbedding E is a unit-distance embedding of G into E.
• UnitDistEmbedding.copy, UnitDistEmbedding.embed, UnitDistEmbedding.iso: transfer a unit-distance embedding down a Copy, graph embedding or graph isomorphism respectively.

structure SimpleGraph.UnitDistEmbedding {V : Type u_1} (G : SimpleGraph V) (E : Type u_3) [MetricSpace E] : Type (max u_1 u_3)

A unit-distance embedding of a graph into a metric space is a vertex embedding such that adjacent vertices are at distance 1 from each other.

• p : V ↪ E

  The embedding itself (position of vertices)

• unit_dist {u v : V} (ha : G.Adj u v) : dist (self.p u) (self.p v) = 1

  The distance between any two adjacent vertices is 1.

def SimpleGraph.UnitDistEmbedding.bot {V : Type u_1} {E : Type u_3} [MetricSpace E] (p : V ↪ E) : ⊥.UnitDistEmbedding E

An injection into the metric space provides a unit-distance embedding of the empty graph.

Equations

• SimpleGraph.UnitDistEmbedding.bot p = { p := p, unit_dist := ⋯ }

@[simp]

theorem SimpleGraph.UnitDistEmbedding.bot_p {V : Type u_1} {E : Type u_3} [MetricSpace E] (p : V ↪ E) : (bot p).p = p

def SimpleGraph.UnitDistEmbedding.subsingleton {V : Type u_1} (G : SimpleGraph V) {E : Type u_3} [MetricSpace E] [Subsingleton V] (x : E) : G.UnitDistEmbedding E

Any graph on a subsingleton vertex type has a unit-distance embedding, provided the metric space is nonempty.

Equations

• SimpleGraph.UnitDistEmbedding.subsingleton G x = { p := { toFun := fun (x_1 : V) => x, inj' := ⋯ }, unit_dist := ⋯ }

@[simp]

theorem SimpleGraph.UnitDistEmbedding.subsingleton_p_apply {V : Type u_1} (G : SimpleGraph V) {E : Type u_3} [MetricSpace E] [Subsingleton V] (x : E) (x✝ : V) : (subsingleton G x).p x✝ = x

def SimpleGraph.UnitDistEmbedding.copy {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {H : SimpleGraph W} {E : Type u_3} [MetricSpace E] (U : G.UnitDistEmbedding E) (f : H.Copy G) : H.UnitDistEmbedding E

Derive a unit-distance embedding of H from a unit-distance embedding of G containing H.

Equations

• U.copy f = { p := f.toEmbedding.trans U.p, unit_dist := ⋯ }

@[simp]

theorem SimpleGraph.UnitDistEmbedding.copy_p_apply {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {H : SimpleGraph W} {E : Type u_3} [MetricSpace E] (U : G.UnitDistEmbedding E) (f : H.Copy G) (a✝ : W) : (U.copy f).p a✝ = U.p (f.toEmbedding a✝)

def SimpleGraph.UnitDistEmbedding.embed {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {H : SimpleGraph W} {E : Type u_3} [MetricSpace E] (U : G.UnitDistEmbedding E) (f : H ↪g G) : H.UnitDistEmbedding E

U.copy specialised to graph embeddings.

Equations

• U.embed f = U.copy f.toCopy

@[simp]

theorem SimpleGraph.UnitDistEmbedding.embed_p_apply {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {H : SimpleGraph W} {E : Type u_3} [MetricSpace E] (U : G.UnitDistEmbedding E) (f : H ↪g G) (a✝ : W) : (U.embed f).p a✝ = U.p (f.toCopy.toEmbedding a✝)

def SimpleGraph.UnitDistEmbedding.iso {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {H : SimpleGraph W} {E : Type u_3} [MetricSpace E] (U : G.UnitDistEmbedding E) (e : G ≃g H) : H.UnitDistEmbedding E

Transfer a unit-distance embedding across a graph isomorphism.

Equations

• U.iso e = U.copy e.symm.toCopy

@[simp]

theorem SimpleGraph.UnitDistEmbedding.iso_p_apply {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {H : SimpleGraph W} {E : Type u_3} [MetricSpace E] (U : G.UnitDistEmbedding E) (e : G ≃g H) (a✝ : W) : (U.iso e).p a✝ = U.p (e.symm.toCopy.toEmbedding a✝)