Based cores of Serre graphs

The core at a vertex consists of the darts occurring in reduced loops at that vertex, together with their endpoints and the base vertex itself. It retains the stem from a base vertex to a circuit. Every reduced based loop lifts to the core, and every core vertex is reachable from the base within the core. Finite graphs have finite cores.

References

• I. Kapovich and A. Myasnikov, Stallings foldings and subgroups of free groups, Section 3, Definition 3.5 and Lemma 3.7.

def TauCeti.SerreGraph.coreDarts (Γ : SerreGraph) (v : Γ.V) : Set Γ.E

The darts occurring in reduced loops at the specified base vertex.

theorem TauCeti.SerreGraph.mem_coreDarts_iff (Γ : SerreGraph) (v : Γ.V) (e : Γ.E) : e ∈ Γ.coreDarts v ↔ ∃ (p : Γ.Path v v), Path.IsReduced Γ p ∧ e ∈ Path.darts Γ p

Membership in the core is witnessed by a reduced based loop.

@[simp]

theorem TauCeti.SerreGraph.rev_mem_coreDarts_iff (Γ : SerreGraph) (v : Γ.V) (e : Γ.E) : Γ.rev e ∈ Γ.coreDarts v ↔ e ∈ Γ.coreDarts v

The dart set of a based core is closed under reversal.

def TauCeti.SerreGraph.coreVertices (Γ : SerreGraph) (v : Γ.V) : Set Γ.V

The vertices of the based core, including an isolated base vertex.

@[simp]

theorem TauCeti.SerreGraph.mem_coreVertices_iff (Γ : SerreGraph) (v a : Γ.V) : a ∈ Γ.coreVertices v ↔ a = v ∨ ∃ e ∈ Γ.coreDarts v, Γ.src e = a

theorem TauCeti.SerreGraph.src_mem_coreVertices (Γ : SerreGraph) (v : Γ.V) {e : Γ.E} (he : e ∈ Γ.coreDarts v) : Γ.src e ∈ Γ.coreVertices v

Both endpoints of a retained dart are retained vertices.

theorem TauCeti.SerreGraph.tgt_mem_coreVertices (Γ : SerreGraph) (v : Γ.V) {e : Γ.E} (he : e ∈ Γ.coreDarts v) : Γ.tgt e ∈ Γ.coreVertices v

def TauCeti.SerreGraph.core (Γ : SerreGraph) (v : Γ.V) : SerreGraph

The union of reduced loops at a base vertex, retaining the base even when there are no nonempty reduced loops. The carrier subtypes compute so paths can be lifted through them.

def TauCeti.SerreGraph.coreBase (Γ : SerreGraph) (v : Γ.V) : (Γ.core v).V

The distinguished vertex in a based core. It computes to the ambient base, so paths mapped by the inclusion have the corresponding ambient endpoints.

def TauCeti.SerreGraph.coreInclusion (Γ : SerreGraph) (v : Γ.V) : (Γ.core v).Hom Γ

Inclusion of the based core into the ambient graph.

@[simp]

theorem TauCeti.SerreGraph.coreInclusion_mapV (Γ : SerreGraph) (v : Γ.V) (a : (Γ.core v).V) : (Γ.coreInclusion v).mapV a = ↑a

@[simp]

theorem TauCeti.SerreGraph.coreInclusion_mapE (Γ : SerreGraph) (v : Γ.V) (e : (Γ.core v).E) : (Γ.coreInclusion v).mapE e = ↑e

@[simp]

theorem TauCeti.SerreGraph.coreBase_val (Γ : SerreGraph) (v : Γ.V) : ↑(Γ.coreBase v) = v

@[simp]

theorem TauCeti.SerreGraph.core_src_val (Γ : SerreGraph) (v : Γ.V) (e : (Γ.core v).E) : ↑((Γ.core v).src e) = Γ.src ↑e

@[simp]

theorem TauCeti.SerreGraph.core_rev_val (Γ : SerreGraph) (v : Γ.V) (e : (Γ.core v).E) : ↑((Γ.core v).rev e) = Γ.rev ↑e

@[simp]

theorem TauCeti.SerreGraph.core_tgt_val (Γ : SerreGraph) (v : Γ.V) (e : (Γ.core v).E) : ↑((Γ.core v).tgt e) = Γ.tgt ↑e

instance TauCeti.SerreGraph.instFiniteVCore (Γ : SerreGraph) (v : Γ.V) [Finite Γ.V] : Finite (Γ.core v).V

instance TauCeti.SerreGraph.instFiniteECore (Γ : SerreGraph) (v : Γ.V) [Finite Γ.E] : Finite (Γ.core v).E

theorem TauCeti.SerreGraph.exists_core_path (Γ : SerreGraph) (v : Γ.V) {a b : Γ.V} (p : Γ.Path a b) (hp : ∀ e ∈ Path.darts Γ p, e ∈ Γ.coreDarts v) (ha : a ∈ Γ.coreVertices v) (hb : b ∈ Γ.coreVertices v) : ∃ (q : (Γ.core v).Path ⟨a, ha⟩ ⟨b, hb⟩), (Γ.coreInclusion v).toPrefunctor.mapPath q = p

A path all of whose darts belong to the core lifts through its inclusion.

theorem TauCeti.SerreGraph.exists_core_loop (Γ : SerreGraph) (v : Γ.V) (p : Γ.Path v v) (hp : Path.IsReduced Γ p) : ∃ (q : (Γ.core v).Path (Γ.coreBase v) (Γ.coreBase v)), (Γ.coreInclusion v).toPrefunctor.mapPath q = p

Every reduced loop based at the chosen vertex is a loop in its core.

theorem TauCeti.SerreGraph.core_reachable (Γ : SerreGraph) (v : Γ.V) (a : (Γ.core v).V) : Nonempty ((Γ.core v).Path (Γ.coreBase v) a)

Every core vertex is reached from its base by a path entirely inside the core.

def TauCeti.SerreGraph.IsCore (Γ : SerreGraph) (v : Γ.V) : Prop

A graph is a core at v if every vertex is reachable from v and every dart lies on a reduced loop based at v. The base vertex may be isolated or have degree one.

theorem TauCeti.SerreGraph.isCore_iff (Γ : SerreGraph) (v : Γ.V) : Γ.IsCore v ↔ (∀ (a : Γ.V), Nonempty (Γ.Path v a)) ∧ ∀ (e : Γ.E), ∃ (p : Γ.Path v v), Path.IsReduced Γ p ∧ e ∈ Path.darts Γ p

Characterization of a based core by reachability and reduced-loop coverage.

theorem TauCeti.SerreGraph.IsCore.connected (Γ : SerreGraph) (v : Γ.V) (hΓ : Γ.IsCore v) : Γ.Connected

A based core is connected, including when its base is an isolated vertex.

theorem TauCeti.SerreGraph.core_isCore (Γ : SerreGraph) (v : Γ.V) : (Γ.core v).IsCore (Γ.coreBase v)

The union of reduced based loops is itself a based core.

theorem TauCeti.SerreGraph.IsCore.exists_outgoing_ne (Γ : SerreGraph) (v : Γ.V) (hΓ : Γ.IsCore v) (e : Γ.E) (he : Γ.src e ≠ v) : ∃ (f : Γ.E), Γ.src f = Γ.src e ∧ f ≠ e

At any vertex other than the base, an outgoing dart of a core has a different outgoing dart. Thus the base is the only possible degree-one vertex, even for an infinite core.