Creation sequences for finite threshold graphs

A creation sequence starts with the empty graph and adds isolated or universal vertices. A representation includes an isomorphism to the actual graph. Existence is proved by deletion and induction, not by a recognition algorithm.

def SimpleGraph.Iso.addIsolated {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {H : SimpleGraph W} (f : G ≃g H) : G.addIsolated ≃g H.addIsolated

Relabel the old vertices of an isolated creation step.

Equations

• f.addIsolated = SimpleGraph.Iso.refl.sumCongr f

def SimpleGraph.Iso.addUniversal {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {H : SimpleGraph W} (f : G ≃g H) : G.addUniversal ≃g H.addUniversal

Relabel the old vertices of a universal creation step.

Equations

• f.addUniversal = f.complement.addIsolated.complement

noncomputable def SimpleGraph.vertexDeletionEquiv {V : Type u_1} (v : V) : Unit ⊕ { x : V // x ≠ v } ≃ V

Reinsert a deleted vertex, with the left summand representing that vertex.

Equations

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

noncomputable def SimpleGraph.isolatedDeletionIso {V : Type u_1} {G : SimpleGraph V} (v : V) (h : ∀ (u : V), ¬G.Adj v u) : (induce {x : V | x ≠ v} G).addIsolated ≃g G

Reinserting a deleted isolated vertex restores the graph.

Equations

• SimpleGraph.isolatedDeletionIso v h = { toEquiv := SimpleGraph.vertexDeletionEquiv v, map_rel_iff' := ⋯ }

noncomputable def SimpleGraph.universalDeletionIso {V : Type u_1} {G : SimpleGraph V} (v : V) (h : ∀ (u : V), u ≠ v → G.Adj v u) : (induce {x : V | x ≠ v} G).addUniversal ≃g G

Reinserting a deleted universal vertex restores the graph.

Equations

• SimpleGraph.universalDeletionIso v h = ⋯.mp (⋯.mp (SimpleGraph.isolatedDeletionIso v ⋯).complement)

inductive SimpleGraph.ThresholdSequence : Type

A finite sequence of isolated and universal vertex additions.

• empty : ThresholdSequence

  Start with the empty graph.

• isolated (previous : ThresholdSequence) : ThresholdSequence

  Add an isolated vertex to the previous graph.

• universal (previous : ThresholdSequence) : ThresholdSequence

  Add a universal vertex to the previous graph.

def SimpleGraph.ThresholdSequence.Vertex : ThresholdSequence → Type

The vertices created by a sequence.

Equations

• SimpleGraph.ThresholdSequence.empty.Vertex = PEmpty.{1}
• s.isolated.Vertex = (Unit ⊕ s.Vertex)
• s.universal.Vertex = (Unit ⊕ s.Vertex)

@[instance_reducible]

noncomputable instance SimpleGraph.ThresholdSequence.vertexFintype (s : ThresholdSequence) : Fintype s.Vertex

A creation sequence has finitely many created vertices.

Equations

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

def SimpleGraph.ThresholdSequence.graph (s : ThresholdSequence) : SimpleGraph s.Vertex

The graph created by a sequence.

Equations

• SimpleGraph.ThresholdSequence.empty.graph = ⊥
• s.isolated.graph = s.graph.addIsolated
• s.universal.graph = s.graph.addUniversal

def SimpleGraph.ThresholdSequence.partition (s : ThresholdSequence) : s.graph.ThresholdPartition

Every sequence carries an explicit threshold partition.

Equations

• One or more equations did not get rendered due to their size.
• s.isolated.partition = s.partition.addIsolated
• s.universal.partition = s.partition.addUniversal

def SimpleGraph.ThresholdSequence.complement : ThresholdSequence → ThresholdSequence

Interchange isolated and universal steps.

Equations

• SimpleGraph.ThresholdSequence.empty.complement = SimpleGraph.ThresholdSequence.empty
• s.isolated.complement = s.complement.universal
• s.universal.complement = s.complement.isolated

@[simp]

theorem SimpleGraph.ThresholdSequence.complement_complement (s : ThresholdSequence) : s.complement.complement = s

Flipping creation steps twice restores the sequence.

noncomputable def SimpleGraph.ThresholdSequence.complementIso (s : ThresholdSequence) : s.complement.graph ≃g s.graphᶜ

Flipping creation steps represents the complementary graph.

Equations

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

structure SimpleGraph.ThresholdCreationRepresentation {V : Type u_1} (G : SimpleGraph V) : Type u_1

A creation sequence with an isomorphism to the represented graph.

• sequence : ThresholdSequence

  The supplied creation sequence.

• iso : self.sequence.graph ≃g G

  Its created vertices correspond exactly to the graph vertices.

def SimpleGraph.ThresholdCreationRepresentation.partition {V : Type u_1} {G : SimpleGraph V} (R : G.ThresholdCreationRepresentation) : G.ThresholdPartition

A creation representation supplies an explicit threshold partition.

Equations

• R.partition = R.sequence.partition.mapIso R.iso

theorem SimpleGraph.ThresholdCreationRepresentation.isThreshold {V : Type u_1} {G : SimpleGraph V} (R : G.ThresholdCreationRepresentation) : G.IsThreshold

A creation representation certifies threshold membership.

def SimpleGraph.ThresholdCreationRepresentation.mapIso {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {H : SimpleGraph W} (R : G.ThresholdCreationRepresentation) (f : G ≃g H) : H.ThresholdCreationRepresentation

Relabel a creation representation without changing its sequence.

Equations

• R.mapIso f = { sequence := R.sequence, iso := RelIso.trans R.iso f }

def SimpleGraph.ThresholdCreationRepresentation.addIsolated {V : Type u_1} {G : SimpleGraph V} (R : G.ThresholdCreationRepresentation) : G.addIsolated.ThresholdCreationRepresentation

Append an isolated step to the supplied representation.

Equations

• R.addIsolated = { sequence := R.sequence.isolated, iso := R.iso.addIsolated }

def SimpleGraph.ThresholdCreationRepresentation.addUniversal {V : Type u_1} {G : SimpleGraph V} (R : G.ThresholdCreationRepresentation) : G.addUniversal.ThresholdCreationRepresentation

Append a universal step to the supplied representation.

Equations

• R.addUniversal = { sequence := R.sequence.universal, iso := R.iso.addUniversal }

noncomputable def SimpleGraph.ThresholdCreationRepresentation.compl {V : Type u_1} {G : SimpleGraph V} (R : G.ThresholdCreationRepresentation) : Gᶜ.ThresholdCreationRepresentation

Complement a representation by interchanging its creation steps.

Equations

• R.compl = { sequence := R.sequence.complement, iso := RelIso.trans R.sequence.complementIso R.iso.complement }

def SimpleGraph.ThresholdCreationRepresentation.ofIsEmpty {V : Type u_1} [IsEmpty V] (G : SimpleGraph V) : G.ThresholdCreationRepresentation

The empty graph has an empty creation sequence.

Equations

• SimpleGraph.ThresholdCreationRepresentation.ofIsEmpty G = { sequence := SimpleGraph.ThresholdSequence.empty, iso := id { toEquiv := Equiv.equivOfIsEmpty PEmpty.{1} V, map_rel_iff' := ⋯ } }

theorem SimpleGraph.IsThreshold.nonempty_creationRepresentation {V : Type u_1} {G : SimpleGraph V} [Finite V] (h : G.IsThreshold) : Nonempty G.ThresholdCreationRepresentation

Every finite threshold graph admits a creation sequence.

theorem SimpleGraph.isThreshold_iff_nonempty_creationRepresentation {V : Type u_1} {G : SimpleGraph V} [Finite V] : G.IsThreshold ↔ Nonempty G.ThresholdCreationRepresentation

Creation sequences characterize finite threshold graphs.