Copies of Simple Graphs

This file introduces the concept of one simple graph containing a copy of another.

Main definitions

• SimpleGraph.Copy A B is the type of copies of A in B, implemented as the subtype of injective homomorphisms.

• SimpleGraph.IsContained A B, A ⊑ B is the relation that B contains a copy of A, that is, the type of copies of A in B is nonempty. This is equivalent to the existence of an isomorphism from A to a subgraph of B.

  This is similar to SimpleGraph.IsSubgraph except that the simple graphs here need not have the same underlying vertex type.

• SimpleGraph.Free is the predicate that B is A-free, that is, B does not contain a copy of A. This is the negation of SimpleGraph.IsContained implemented for convenience.

Notation

The following notation is declared in locale SimpleGraph:

• G ⊑ H for SimpleGraph.IsContained G H.

@[reducible, inline]

abbrev SimpleGraph.Copy {α : Type u_2} {β : Type u_3} (A : SimpleGraph α) (B : SimpleGraph β) : Type (max 0 u_2 u_3)

The type of copies as a subtype of injective homomorphisms.

Equations

• A.Copy B = { f : A →g B // Function.Injective ⇑f }

@[reducible, inline]

abbrev SimpleGraph.Hom.toCopy {α : Type u_2} {β : Type u_3} {A : SimpleGraph α} {B : SimpleGraph β} (f : A →g B) (h : Function.Injective ⇑f) : A.Copy B

An injective homomorphism gives rise to a copy.

Equations

• f.toCopy h = ⟨f, h⟩

@[reducible, inline]

abbrev SimpleGraph.Embedding.toCopy {α : Type u_2} {β : Type u_3} {A : SimpleGraph α} {B : SimpleGraph β} (f : A ↪g B) : A.Copy B

An embedding gives rise to a copy.

Equations

• f.toCopy = f.toHom.toCopy ⋯

@[reducible, inline]

abbrev SimpleGraph.Iso.toCopy {α : Type u_2} {β : Type u_3} {A : SimpleGraph α} {B : SimpleGraph β} (f : A ≃g B) : A.Copy B

An isomorphism gives rise to a copy.

Equations

• f.toCopy = f.toEmbedding.toCopy

@[reducible, inline]

abbrev SimpleGraph.Copy.toHom {α : Type u_2} {β : Type u_3} {A : SimpleGraph α} {B : SimpleGraph β} : A.Copy B → A →g B

A copy gives rise to a homomorphism.

Equations

• SimpleGraph.Copy.toHom = Subtype.val

@[simp]

theorem SimpleGraph.Copy.coe_toHom {α : Type u_2} {β : Type u_3} {A : SimpleGraph α} {B : SimpleGraph β} (f : A.Copy B) : ⇑f.toHom = ⇑↑f

theorem SimpleGraph.Copy.injective {α : Type u_2} {β : Type u_3} {A : SimpleGraph α} {B : SimpleGraph β} (f : A.Copy B) : Function.Injective ⇑f.toHom

instance SimpleGraph.Copy.instFunLike {α : Type u_2} {β : Type u_3} {A : SimpleGraph α} {B : SimpleGraph β} : FunLike (A.Copy B) α β

Equations

• SimpleGraph.Copy.instFunLike = { coe := fun (f : A.Copy B) => ⇑f.toHom, coe_injective' := ⋯ }

@[simp]

theorem SimpleGraph.Copy.coe_toHom_apply {α : Type u_2} {β : Type u_3} {A : SimpleGraph α} {B : SimpleGraph β} (f : A.Copy B) (a : α) : f.toHom a = f a

def SimpleGraph.Copy.mapEdgeSet {α : Type u_2} {β : Type u_3} {A : SimpleGraph α} {B : SimpleGraph β} (f : A.Copy B) : ↑A.edgeSet ↪ ↑B.edgeSet

A copy induces an embedding of edge sets.

Equations

• f.mapEdgeSet = { toFun := f.toHom.mapEdgeSet, inj' := ⋯ }

def SimpleGraph.Copy.mapNeighborSet {α : Type u_2} {β : Type u_3} {A : SimpleGraph α} {B : SimpleGraph β} (f : A.Copy B) (a : α) : ↑(A.neighborSet a) ↪ ↑(B.neighborSet (f a))

A copy induces an embedding of neighbor sets.

Equations

• f.mapNeighborSet a = { toFun := fun (v : ↑(A.neighborSet a)) => ⟨f ↑v, ⋯⟩, inj' := ⋯ }

def SimpleGraph.Copy.toEmbedding {α : Type u_2} {β : Type u_3} {A : SimpleGraph α} {B : SimpleGraph β} (f : A.Copy B) : α ↪ β

A copy gives rise to an embedding of vertex types.

Equations

• f.toEmbedding = { toFun := ⇑f, inj' := ⋯ }

def SimpleGraph.Copy.id {V : Type u_1} (G : SimpleGraph V) : G.Copy G

The identity copy from a simple graph to itself.

Equations

• SimpleGraph.Copy.id G = ⟨SimpleGraph.Hom.id, ⋯⟩

@[simp]

theorem SimpleGraph.Copy.coe_id {V : Type u_1} {G : SimpleGraph V} : ⇑(id G) = _root_.id

def SimpleGraph.Copy.comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} {A : SimpleGraph α} {B : SimpleGraph β} {C : SimpleGraph γ} (g : B.Copy C) (f : A.Copy B) : A.Copy C

The composition of copies is a copy.

Equations

• g.comp f = ⟨g.toHom.comp f.toHom, ⋯⟩

@[simp]

theorem SimpleGraph.Copy.comp_apply {α : Type u_2} {β : Type u_3} {γ : Type u_4} {A : SimpleGraph α} {B : SimpleGraph β} {C : SimpleGraph γ} (g : B.Copy C) (f : A.Copy B) (a : α) : (g.comp f) a = g (f a)

def SimpleGraph.Copy.ofLE {V : Type u_1} (G₁ G₂ : SimpleGraph V) (h : G₁ ≤ G₂) : G₁.Copy G₂

The copy from a subgraph to the supergraph.

Equations

• SimpleGraph.Copy.ofLE G₁ G₂ h = ⟨SimpleGraph.Hom.ofLE h, ⋯⟩

@[simp]

theorem SimpleGraph.Copy.coe_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} {A : SimpleGraph α} {B : SimpleGraph β} {C : SimpleGraph γ} (g : B.Copy C) (f : A.Copy B) : ⇑(g.comp f) = ⇑g ∘ ⇑f

@[simp]

theorem SimpleGraph.Copy.coe_ofLE {V : Type u_1} {G₁ G₂ : SimpleGraph V} (h : G₁ ≤ G₂) : ⇑(ofLE G₁ G₂ h) = _root_.id

@[simp]

theorem SimpleGraph.Copy.ofLE_refl {V : Type u_1} {G : SimpleGraph V} : ofLE G G ⋯ = id G

@[simp]

theorem SimpleGraph.Copy.ofLE_comp {V : Type u_1} {G₁ G₂ G₃ : SimpleGraph V} (h₁₂ : G₁ ≤ G₂) (h₂₃ : G₂ ≤ G₃) : (ofLE G₂ G₃ h₂₃).comp (ofLE G₁ G₂ h₁₂) = ofLE G₁ G₃ ⋯

def SimpleGraph.Copy.induce {V : Type u_1} (G : SimpleGraph V) (s : Set V) : (SimpleGraph.induce s G).Copy G

The copy from an induced subgraph to the initial simple graph.

Equations

• SimpleGraph.Copy.induce G s = (SimpleGraph.Embedding.induce s).toCopy

def SimpleGraph.Copy.bot {α : Type u_2} {β : Type u_3} {B : SimpleGraph β} (f : α ↪ β) : ⊥.Copy B

The copy of ⊥ in any simple graph that can embed its vertices.

Equations

• SimpleGraph.Copy.bot f = ⟨{ toFun := ⇑f, map_rel' := ⋯ }, ⋯⟩

def SimpleGraph.Subgraph.coeCopy {V : Type u_1} {G : SimpleGraph V} (G' : G.Subgraph) : G'.coe.Copy G

A Subgraph G gives rise to a copy from the coercion to G.

Equations

• G'.coeCopy = G'.hom.toCopy ⋯

@[reducible, inline]

abbrev SimpleGraph.IsContained {α : Type u_2} {β : Type u_3} (A : SimpleGraph α) (B : SimpleGraph β) : Prop

The relation IsContained A B, A ⊑ B says that B contains a copy of A.

This is equivalent to the existence of an isomorphism from A to a subgraph of B.

Equations

• A.IsContained B = Nonempty (A.Copy B)

def SimpleGraph.«term_⊑_» : Lean.TrailingParserDescr

The relation IsContained A B, A ⊑ B says that B contains a copy of A.

This is equivalent to the existence of an isomorphism from A to a subgraph of B.

Equations

• SimpleGraph.«term_⊑_» = Lean.ParserDescr.trailingNode `SimpleGraph.«term_⊑_» 50 50 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊑ ") (Lean.ParserDescr.cat `term 51))

theorem SimpleGraph.IsContained.refl {V : Type u_1} (G : SimpleGraph V) : G.IsContained G

A simple graph contains itself.

theorem SimpleGraph.IsContained.rfl {V : Type u_1} {G : SimpleGraph V} : G.IsContained G

theorem SimpleGraph.IsContained.of_le {V : Type u_1} {G₁ G₂ : SimpleGraph V} (h : G₁ ≤ G₂) : G₁.IsContained G₂

A simple graph contains its subgraphs.

theorem SimpleGraph.IsContained.trans {α : Type u_2} {β : Type u_3} {γ : Type u_4} {A : SimpleGraph α} {B : SimpleGraph β} {C : SimpleGraph γ} : A.IsContained B → B.IsContained C → A.IsContained C

If A contains B and B contains C, then A contains C.

theorem SimpleGraph.IsContained.trans' {α : Type u_2} {β : Type u_3} {γ : Type u_4} {A : SimpleGraph α} {B : SimpleGraph β} {C : SimpleGraph γ} : B.IsContained C → A.IsContained B → A.IsContained C

If B contains C and A contains B, then A contains C.

theorem SimpleGraph.IsContained.mono_right {α : Type u_2} {β : Type u_3} {A : SimpleGraph α} {B B' : SimpleGraph β} (h_isub : A.IsContained B) (h_sub : B ≤ B') : A.IsContained B'

theorem SimpleGraph.IsContained.trans_le {α : Type u_2} {β : Type u_3} {A : SimpleGraph α} {B B' : SimpleGraph β} (h_isub : A.IsContained B) (h_sub : B ≤ B') : A.IsContained B'

Alias of SimpleGraph.IsContained.mono_right.

theorem SimpleGraph.IsContained.mono_left {α : Type u_2} {β : Type u_3} {A : SimpleGraph α} {B : SimpleGraph β} {A' : SimpleGraph α} (h_sub : A ≤ A') (h_isub : A'.IsContained B) : A.IsContained B

theorem SimpleGraph.IsContained.trans_le' {α : Type u_2} {β : Type u_3} {A : SimpleGraph α} {B : SimpleGraph β} {A' : SimpleGraph α} (h_sub : A ≤ A') (h_isub : A'.IsContained B) : A.IsContained B

Alias of SimpleGraph.IsContained.mono_left.

theorem SimpleGraph.isContained_congr {α : Type u_2} {β : Type u_3} {γ : Type u_4} {A : SimpleGraph α} {B : SimpleGraph β} {C : SimpleGraph γ} (e : A ≃g B) : A.IsContained C ↔ B.IsContained C

If A ≃g B, then A is contained in C if and only if B is contained in C.

theorem SimpleGraph.IsContained.of_isEmpty {α : Type u_2} {β : Type u_3} {A : SimpleGraph α} {B : SimpleGraph β} [IsEmpty α] : A.IsContained B

A simple graph having no vertices is contained in any simple graph.

theorem SimpleGraph.bot_isContained_iff_card_le {α : Type u_2} {β : Type u_3} {B : SimpleGraph β} [Fintype α] [Fintype β] : ⊥.IsContained B ↔ Fintype.card α ≤ Fintype.card β

⊥ is contained in any simple graph having sufficently many vertices.

theorem SimpleGraph.IsContained.bot {α : Type u_2} {β : Type u_3} {B : SimpleGraph β} [Fintype α] [Fintype β] : ⊥.IsContained B ↔ Fintype.card α ≤ Fintype.card β

Alias of SimpleGraph.bot_isContained_iff_card_le.

---

⊥ is contained in any simple graph having sufficently many vertices.

theorem SimpleGraph.Subgraph.coe_isContained {V : Type u_1} {G : SimpleGraph V} (G' : G.Subgraph) : G'.coe.IsContained G

A simple graph G contains all Subgraph G coercions.

noncomputable def SimpleGraph.Subgraph.Copy.map {α : Type u_2} {β : Type u_3} {A : SimpleGraph α} {B : SimpleGraph β} (f : A.Copy B) (A' : A.Subgraph) : A'.coe ≃g (Subgraph.map f.toHom A').coe

The isomorphism from Subgraph A to its map under a copy Copy A B.

Equations

• SimpleGraph.Subgraph.Copy.map f A' = { toEquiv := Equiv.Set.image (⇑f.toHom) A'.verts ⋯, map_rel_iff' := ⋯ }

theorem SimpleGraph.isContained_iff_exists_iso_subgraph {α : Type u_2} {β : Type u_3} {A : SimpleGraph α} {B : SimpleGraph β} : A.IsContained B ↔ ∃ (B' : B.Subgraph), Nonempty (A ≃g B'.coe)

B contains A if and only if B has a subgraph B' and B' is isomorphic to A.

theorem SimpleGraph.IsContained.of_exists_iso_subgraph {α : Type u_2} {β : Type u_3} {A : SimpleGraph α} {B : SimpleGraph β} : (∃ (B' : B.Subgraph), Nonempty (A ≃g B'.coe)) → A.IsContained B

Alias of the reverse direction of SimpleGraph.isContained_iff_exists_iso_subgraph.

---

B contains A if and only if B has a subgraph B' and B' is isomorphic to A.

theorem SimpleGraph.IsContained.exists_iso_subgraph {α : Type u_2} {β : Type u_3} {A : SimpleGraph α} {B : SimpleGraph β} : A.IsContained B → ∃ (B' : B.Subgraph), Nonempty (A ≃g B'.coe)

Alias of the forward direction of SimpleGraph.isContained_iff_exists_iso_subgraph.

---

B contains A if and only if B has a subgraph B' and B' is isomorphic to A.

@[reducible, inline]

abbrev SimpleGraph.Free {α : Type u_2} {β : Type u_3} (A : SimpleGraph α) (B : SimpleGraph β) : Prop

The proposition that a simple graph does not contain a copy of another simple graph.

Equations

• A.Free B = ¬A.IsContained B

theorem SimpleGraph.not_free {α : Type u_2} {β : Type u_3} {A : SimpleGraph α} {B : SimpleGraph β} : ¬A.Free B ↔ A.IsContained B

theorem SimpleGraph.free_congr {α : Type u_2} {β : Type u_3} {γ : Type u_4} {A : SimpleGraph α} {B : SimpleGraph β} {C : SimpleGraph γ} (e : A ≃g B) : A.Free C ↔ B.Free C

If A ≃g B, then C is A-free if and only if C is B-free.

theorem SimpleGraph.free_bot {α : Type u_2} {β : Type u_3} {A : SimpleGraph α} (h : A ≠ ⊥) : A.Free ⊥