Ends

This file contains a definition of the ends of a simple graph, as sections of the inverse system assigning, to each finite set of vertices, the connected components of its complement.

@[reducible]

def SimpleGraph.ComponentCompl {V : Type u} (G : SimpleGraph V) (K : Set V) : Type u

The components outside a given set of vertices K

Equations

• SimpleGraph.ComponentCompl G K = SimpleGraph.ConnectedComponent (SimpleGraph.induce Kᶜ G)

@[reducible]

def SimpleGraph.componentComplMk {V : Type u} {K : Set V} (G : SimpleGraph V) {v : V} (vK : v ∉ K) : SimpleGraph.ComponentCompl G K

The connected component of v in G.induce Kᶜ.

Equations

• SimpleGraph.componentComplMk G vK = SimpleGraph.connectedComponentMk (SimpleGraph.induce Kᶜ G) { val := v, property := vK }

def SimpleGraph.ComponentCompl.supp {V : Type u} {G : SimpleGraph V} {K : Set V} (C : SimpleGraph.ComponentCompl G K) : Set V

The set of vertices of G making up the connected component C

Equations

• SimpleGraph.ComponentCompl.supp C = {v : V | ∃ (h : v ∉ K), SimpleGraph.componentComplMk G h = C}

theorem SimpleGraph.ComponentCompl.supp_injective {V : Type u} {G : SimpleGraph V} {K : Set V} : Function.Injective SimpleGraph.ComponentCompl.supp

theorem SimpleGraph.ComponentCompl.supp_inj {V : Type u} {G : SimpleGraph V} {K : Set V} {C : SimpleGraph.ComponentCompl G K} {D : SimpleGraph.ComponentCompl G K} : SimpleGraph.ComponentCompl.supp C = SimpleGraph.ComponentCompl.supp D ↔ C = D

instance SimpleGraph.ComponentCompl.setLike {V : Type u} {G : SimpleGraph V} {K : Set V} : SetLike (SimpleGraph.ComponentCompl G K) V

Equations

• SimpleGraph.ComponentCompl.setLike = { coe := SimpleGraph.ComponentCompl.supp, coe_injective' := ⋯ }

@[simp]

theorem SimpleGraph.ComponentCompl.mem_supp_iff {V : Type u} {G : SimpleGraph V} {K : Set V} {v : V} {C : SimpleGraph.ComponentCompl G K} : v ∈ C ↔ ∃ (vK : v ∉ K), SimpleGraph.componentComplMk G vK = C

theorem SimpleGraph.componentComplMk_mem {V : Type u} {K : Set V} (G : SimpleGraph V) {v : V} (vK : v ∉ K) : v ∈ SimpleGraph.componentComplMk G vK

theorem SimpleGraph.componentComplMk_eq_of_adj {V : Type u} {K : Set V} (G : SimpleGraph V) {v : V} {w : V} (vK : v ∉ K) (wK : w ∉ K) (a : G.Adj v w) : SimpleGraph.componentComplMk G vK = SimpleGraph.componentComplMk G wK

instance SimpleGraph.componentCompl_nonempty_of_infinite {V : Type u} (G : SimpleGraph V) [Infinite V] (K : Finset V) : Nonempty (SimpleGraph.ComponentCompl G ↑K)

In an infinite graph, the set of components out of a finite set is nonempty.

Equations

• ⋯ = ⋯

def SimpleGraph.ComponentCompl.lift {V : Type u} {G : SimpleGraph V} {K : Set V} {β : Sort u_1} (f : ⦃v : V⦄ → v ∉ K → β) (h : ∀ ⦃v w : V⦄ (hv : v ∉ K) (hw : w ∉ K), G.Adj v w → f hv = f hw) : SimpleGraph.ComponentCompl G K → β

A ComponentCompl specialization of Quot.lift, where soundness has to be proved only for adjacent vertices.

Equations

• SimpleGraph.ComponentCompl.lift f h = SimpleGraph.ConnectedComponent.lift (fun (vv : ↑Kᶜ) => f ⋯) ⋯

theorem SimpleGraph.ComponentCompl.ind {V : Type u} {G : SimpleGraph V} {K : Set V} {β : SimpleGraph.ComponentCompl G K → Prop} (f : ∀ ⦃v : V⦄ (hv : v ∉ K), β (SimpleGraph.componentComplMk G hv)) (C : SimpleGraph.ComponentCompl G K) : β C

@[reducible]

def SimpleGraph.ComponentCompl.coeGraph {V : Type u} {G : SimpleGraph V} {K : Set V} (C : SimpleGraph.ComponentCompl G K) : SimpleGraph ↥C

The induced graph on the vertices C.

Equations

• SimpleGraph.ComponentCompl.coeGraph C = SimpleGraph.induce (↑C) G

theorem SimpleGraph.ComponentCompl.coe_inj {V : Type u} {G : SimpleGraph V} {K : Set V} {C : SimpleGraph.ComponentCompl G K} {D : SimpleGraph.ComponentCompl G K} : ↑C = ↑D ↔ C = D

@[simp]

theorem SimpleGraph.ComponentCompl.nonempty {V : Type u} {G : SimpleGraph V} {K : Set V} (C : SimpleGraph.ComponentCompl G K) : Set.Nonempty ↑C

theorem SimpleGraph.ComponentCompl.exists_eq_mk {V : Type u} {G : SimpleGraph V} {K : Set V} (C : SimpleGraph.ComponentCompl G K) : ∃ (v : V) (h : v ∉ K), SimpleGraph.componentComplMk G h = C

theorem SimpleGraph.ComponentCompl.disjoint_right {V : Type u} {G : SimpleGraph V} {K : Set V} (C : SimpleGraph.ComponentCompl G K) : Disjoint K ↑C

theorem SimpleGraph.ComponentCompl.not_mem_of_mem {V : Type u} {G : SimpleGraph V} {K : Set V} {C : SimpleGraph.ComponentCompl G K} {c : V} (cC : c ∈ C) : c ∉ K

theorem SimpleGraph.ComponentCompl.pairwise_disjoint {V : Type u} {G : SimpleGraph V} {K : Set V} : Pairwise fun (C D : SimpleGraph.ComponentCompl G K) => Disjoint ↑C ↑D

theorem SimpleGraph.ComponentCompl.mem_of_adj {V : Type u} {G : SimpleGraph V} {K : Set V} {C : SimpleGraph.ComponentCompl G K} (c : V) (d : V) : c ∈ C → d ∉ K → G.Adj c d → d ∈ C

Any vertex adjacent to a vertex of C and not lying in K must lie in C.

theorem SimpleGraph.ComponentCompl.exists_adj_boundary_pair {V : Type u} {G : SimpleGraph V} {K : Set V} (Gc : SimpleGraph.Preconnected G) (hK : Set.Nonempty K) (C : SimpleGraph.ComponentCompl G K) : ∃ (ck : V × V), ck.1 ∈ C ∧ ck.2 ∈ K ∧ G.Adj ck.1 ck.2

Assuming G is preconnected and K not empty, given any connected component C outside of K, there exists a vertex k ∈ K adjacent to a vertex v ∈ C.

@[reducible]

def SimpleGraph.ComponentCompl.hom {V : Type u} {G : SimpleGraph V} {K : Set V} {L : Set V} (h : K ⊆ L) (C : SimpleGraph.ComponentCompl G L) : SimpleGraph.ComponentCompl G K

If K ⊆ L, the components outside of L are all contained in a single component outside of K.

Equations

• SimpleGraph.ComponentCompl.hom h C = SimpleGraph.ConnectedComponent.map (SimpleGraph.induceHom SimpleGraph.Hom.id ⋯) C

theorem SimpleGraph.ComponentCompl.subset_hom {V : Type u} {G : SimpleGraph V} {K : Set V} {L : Set V} (C : SimpleGraph.ComponentCompl G L) (h : K ⊆ L) : ↑C ⊆ ↑(SimpleGraph.ComponentCompl.hom h C)

theorem SimpleGraph.componentComplMk_mem_hom {V : Type u} {K : Set V} {L : Set V} (G : SimpleGraph V) {v : V} (vK : v ∉ K) (h : L ⊆ K) : v ∈ SimpleGraph.ComponentCompl.hom h (SimpleGraph.componentComplMk G vK)

theorem SimpleGraph.ComponentCompl.hom_eq_iff_le {V : Type u} {G : SimpleGraph V} {K : Set V} {L : Set V} (C : SimpleGraph.ComponentCompl G L) (h : K ⊆ L) (D : SimpleGraph.ComponentCompl G K) : SimpleGraph.ComponentCompl.hom h C = D ↔ ↑C ⊆ ↑D

theorem SimpleGraph.ComponentCompl.hom_eq_iff_not_disjoint {V : Type u} {G : SimpleGraph V} {K : Set V} {L : Set V} (C : SimpleGraph.ComponentCompl G L) (h : K ⊆ L) (D : SimpleGraph.ComponentCompl G K) : SimpleGraph.ComponentCompl.hom h C = D ↔ ¬Disjoint ↑C ↑D

theorem SimpleGraph.ComponentCompl.hom_refl {V : Type u} {G : SimpleGraph V} {L : Set V} (C : SimpleGraph.ComponentCompl G L) : SimpleGraph.ComponentCompl.hom ⋯ C = C

theorem SimpleGraph.ComponentCompl.hom_trans {V : Type u} {G : SimpleGraph V} {K : Set V} {L : Set V} {M : Set V} (C : SimpleGraph.ComponentCompl G L) (h : K ⊆ L) (h' : M ⊆ K) : SimpleGraph.ComponentCompl.hom ⋯ C = SimpleGraph.ComponentCompl.hom h' (SimpleGraph.ComponentCompl.hom h C)

theorem SimpleGraph.ComponentCompl.hom_mk {V : Type u} {G : SimpleGraph V} {K : Set V} {L : Set V} {v : V} (vnL : v ∉ L) (h : K ⊆ L) : SimpleGraph.ComponentCompl.hom h (SimpleGraph.componentComplMk G vnL) = SimpleGraph.componentComplMk G ⋯

theorem SimpleGraph.ComponentCompl.hom_infinite {V : Type u} {G : SimpleGraph V} {K : Set V} {L : Set V} (C : SimpleGraph.ComponentCompl G L) (h : K ⊆ L) (Cinf : Set.Infinite ↑C) : Set.Infinite ↑(SimpleGraph.ComponentCompl.hom h C)

theorem SimpleGraph.ComponentCompl.infinite_iff_in_all_ranges {V : Type u} {G : SimpleGraph V} {K : Finset V} (C : SimpleGraph.ComponentCompl G ↑K) : Set.Infinite (SimpleGraph.ComponentCompl.supp C) ↔ ∀ (L : Finset V) (h : K ⊆ L), ∃ (D : SimpleGraph.ComponentCompl G ↑L), SimpleGraph.ComponentCompl.hom h D = C

instance SimpleGraph.componentCompl_finite {V : Type u} {G : SimpleGraph V} [SimpleGraph.LocallyFinite G] [Gpc : Fact (SimpleGraph.Preconnected G)] (K : Finset V) : Finite (SimpleGraph.ComponentCompl G ↑K)

Equations

• ⋯ = ⋯

@[simp]

theorem SimpleGraph.componentComplFunctor_obj {V : Type u} (G : SimpleGraph V) (K : (Finset V)ᵒᵖ) : (SimpleGraph.componentComplFunctor G).obj K = SimpleGraph.ComponentCompl G ↑K.unop

@[simp]

theorem SimpleGraph.componentComplFunctor_map {V : Type u} (G : SimpleGraph V) : ∀ {X Y : (Finset V)ᵒᵖ} (f : X ⟶ Y) (C : SimpleGraph.ComponentCompl G ↑X.unop), (SimpleGraph.componentComplFunctor G).map f C = SimpleGraph.ComponentCompl.hom ⋯ C

def SimpleGraph.componentComplFunctor {V : Type u} (G : SimpleGraph V) : CategoryTheory.Functor (Finset V)ᵒᵖ (Type u)

The functor assigning, to a finite set in V, the set of connected components in its complement.

Equations

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

def SimpleGraph.end {V : Type u} (G : SimpleGraph V) : Set ((j : (Finset V)ᵒᵖ) → (SimpleGraph.componentComplFunctor G).obj j)

The end of a graph, defined as the sections of the functor component_compl_functor .

Equations

• SimpleGraph.end G = CategoryTheory.Functor.sections (SimpleGraph.componentComplFunctor G)

theorem SimpleGraph.end_hom_mk_of_mk {V : Type u} (G : SimpleGraph V) {s : (j : (Finset V)ᵒᵖ) → (SimpleGraph.componentComplFunctor G).obj j} (sec : s ∈ SimpleGraph.end G) {K : (Finset V)ᵒᵖ} {L : (Finset V)ᵒᵖ} (h : L ⟶ K) {v : V} (vnL : v ∉ L.unop) (hs : s L = SimpleGraph.componentComplMk G vnL) : s K = SimpleGraph.componentComplMk G ⋯

theorem SimpleGraph.infinite_iff_in_eventualRange {V : Type u} (G : SimpleGraph V) {K : (Finset V)ᵒᵖ} (C : (SimpleGraph.componentComplFunctor G).obj K) : Set.Infinite (SimpleGraph.ComponentCompl.supp C) ↔ C ∈ CategoryTheory.Functor.eventualRange (SimpleGraph.componentComplFunctor G) K