The spanning-tree computation for finite quivers

This file builds the combinatorial fundamental group of a finite weakly connected quiver from Mathlib's free groupoid and identifies a basis indexed by the edges outside a geodesic spanning tree.

def FiniteGraphFreeGroup.totalEquiv {V : Type u} [Quiver V] (T : WideSubquiver V) : Quiver.Total (WideSubquiver.toType V T) ≃ (a : V) × (b : V) × { e : a ⟶ b // e ∈ T a b }

Identifies total arrows of a wide subquiver with their endpoints and underlying arrow.

Equations

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

@[reducible]

noncomputable def FiniteGraphFreeGroup.totalFintype {V : Type u} [Quiver V] [Fintype V] [(a b : V) → Fintype (a ⟶ b)] (T : WideSubquiver V) : Fintype (Quiver.Total (WideSubquiver.toType V T))

The finite structure on the total arrows of a finite wide subquiver.

Equations

• FiniteGraphFreeGroup.totalFintype T = Fintype.ofEquiv ((a : V) × (b : V) × { e : a ⟶ b // e ∈ T a b }) (FiniteGraphFreeGroup.totalEquiv T).symm

@[instance_reducible]

noncomputable instance FiniteGraphFreeGroup.wideSubquiverHomFintype {V : Type u} [Quiver V] [(a b : V) → Fintype (a ⟶ b)] (T : WideSubquiver V) (a b : WideSubquiver.toType V T) : Fintype (a ⟶ b)

Equations

• FiniteGraphFreeGroup.wideSubquiverHomFintype T a b = Fintype.subtype {e : a ⟶ b | e ∈ T a b} ⋯

@[instance_reducible]

noncomputable instance FiniteGraphFreeGroup.wideSubquiverVertexFintype {V : Type u} [Quiver V] [Fintype V] (T : WideSubquiver V) : Fintype (WideSubquiver.toType V T)

Equations

• FiniteGraphFreeGroup.wideSubquiverVertexFintype T = Fintype.ofEquiv V (Equiv.refl V)

def FiniteGraphFreeGroup.baseTotalEquiv (V : Type u) [Quiver V] : Quiver.Total V ≃ (a : V) × (b : V) × (a ⟶ b)

Identifies total arrows of a quiver with their endpoints and arrow data.

Equations

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

@[reducible]

noncomputable def FiniteGraphFreeGroup.baseTotalFintype {V : Type u} [Quiver V] [Fintype V] [(a b : V) → Fintype (a ⟶ b)] : Fintype (Quiver.Total V)

The finite structure on total arrows of a finite quiver.

Equations

• FiniteGraphFreeGroup.baseTotalFintype = Fintype.ofEquiv ((a : V) × (b : V) × (a ⟶ b)) (FiniteGraphFreeGroup.baseTotalEquiv V).symm

@[instance_reducible]

noncomputable instance FiniteGraphFreeGroup.baseTotalFintypeInst {V : Type u} [Quiver V] [Fintype V] [(a b : V) → Fintype (a ⟶ b)] : Fintype (Quiver.Total V)

Equations

• FiniteGraphFreeGroup.baseTotalFintypeInst = FiniteGraphFreeGroup.baseTotalFintype

@[instance_reducible]

noncomputable instance FiniteGraphFreeGroup.symmetrifyFintype {V : Type u} [Fintype V] : Fintype (Quiver.Symmetrify V)

Equations

• FiniteGraphFreeGroup.symmetrifyFintype = Fintype.ofEquiv V (Equiv.refl V)

@[instance_reducible]

noncomputable instance FiniteGraphFreeGroup.symmetrifyHomFintype {V : Type u} [Quiver V] [(a b : V) → Fintype (a ⟶ b)] (a b : Quiver.Symmetrify V) : Fintype (a ⟶ b)

Equations

• FiniteGraphFreeGroup.symmetrifyHomFintype a b = id inferInstance

def FiniteGraphFreeGroup.wideTotalEquiv {V : Type u} [Quiver V] (H : WideSubquiver V) : Quiver.Total (WideSubquiver.toType V H) ≃ ↑(Quiver.wideSubquiverEquivSetTotal H)

Identifies a wide subquiver's total arrows with the corresponding subset of base arrows.

Equations

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

@[instance_reducible]

noncomputable instance FiniteGraphFreeGroup.wideSubquiverSetTotalFintype {V : Type u} [Quiver V] [Fintype V] [(a b : V) → Fintype (a ⟶ b)] (H : WideSubquiver V) : Fintype ↑(Quiver.wideSubquiverEquivSetTotal H)

Equations

• FiniteGraphFreeGroup.wideSubquiverSetTotalFintype H = Fintype.ofEquiv (Quiver.Total (WideSubquiver.toType V H)) (FiniteGraphFreeGroup.wideTotalEquiv H)

theorem FiniteGraphFreeGroup.exists_last_data {V : Type u} [Quiver V] (T : WideSubquiver V) [Quiver.Arborescence (WideSubquiver.toType V T)] {b : WideSubquiver.toType V T} (hb : b ≠ Quiver.root (WideSubquiver.toType V T)) : Nonempty ((a : WideSubquiver.toType V T) × Quiver.Path (Quiver.root (WideSubquiver.toType V T)) a × (a ⟶ b))

noncomputable def FiniteGraphFreeGroup.lastData {V : Type u} [Quiver V] (T : WideSubquiver V) [Quiver.Arborescence (WideSubquiver.toType V T)] (b : { b : WideSubquiver.toType V T // b ≠ Quiver.root (WideSubquiver.toType V T) }) : (a : WideSubquiver.toType V T) × Quiver.Path (Quiver.root (WideSubquiver.toType V T)) a × (a ⟶ ↑b)

The penultimate vertex, prefix path, and last edge of the rooted path to a non-root vertex.

Equations

• FiniteGraphFreeGroup.lastData T b = Classical.choice ⋯

theorem FiniteGraphFreeGroup.default_path_length_root {V : Type u} [Quiver V] (T : WideSubquiver V) [Quiver.Arborescence (WideSubquiver.toType V T)] (b : WideSubquiver.toType V T) (h : b = Quiver.root (WideSubquiver.toType V T)) : default.length = 0

theorem FiniteGraphFreeGroup.target_ne_root {V : Type u} [Quiver V] (T : WideSubquiver V) [Quiver.Arborescence (WideSubquiver.toType V T)] (e : Quiver.Total (WideSubquiver.toType V T)) : e.right ≠ Quiver.root (WideSubquiver.toType V T)

noncomputable def FiniteGraphFreeGroup.treeEdgeEquiv {V : Type u} [Quiver V] (T : WideSubquiver V) [Quiver.Arborescence (WideSubquiver.toType V T)] : Quiver.Total (WideSubquiver.toType V T) ≃ { b : WideSubquiver.toType V T // b ≠ Quiver.root (WideSubquiver.toType V T) }

Identifies the edges of an arborescence with its non-root vertices.

Equations

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

theorem FiniteGraphFreeGroup.arborescence_card {V : Type u} [Quiver V] [Fintype V] [(a b : V) → Fintype (a ⟶ b)] (T : WideSubquiver V) [Quiver.Arborescence (WideSubquiver.toType V T)] : Fintype.card (Quiver.Total (WideSubquiver.toType V T)) = Fintype.card V - 1

theorem FiniteGraphFreeGroup.no_reverse_edges {V : Type u} [Quiver V] (T : WideSubquiver (Quiver.Symmetrify V)) [Quiver.Arborescence (WideSubquiver.toType (Quiver.Symmetrify V) T)] {a b : V} (e : a ⟶ b) (h₁ : T a b (Sum.inl e)) (h₂ : T b a (Sum.inr e)) : False

def FiniteGraphFreeGroup.symEdgeForget {V : Type u} [Quiver V] (T : WideSubquiver (Quiver.Symmetrify V)) (e : Quiver.Total (WideSubquiver.toType (Quiver.Symmetrify V) T)) : Quiver.Total (WideSubquiver.toType V (Quiver.wideSubquiverSymmetrify T))

Forgets the orientation tag on an edge of a symmetric wide subquiver.

Equations

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

noncomputable def FiniteGraphFreeGroup.symEdgeForgetInv {V : Type u} [Quiver V] (T : WideSubquiver (Quiver.Symmetrify V)) (e : Quiver.Total (WideSubquiver.toType V (Quiver.wideSubquiverSymmetrify T))) : Quiver.Total (WideSubquiver.toType (Quiver.Symmetrify V) T)

Recovers the uniquely oriented tree edge from its underlying graph edge.

Equations

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

theorem FiniteGraphFreeGroup.symEdgeForgetInv_forget {V : Type u} [Quiver V] (T : WideSubquiver (Quiver.Symmetrify V)) [Quiver.Arborescence (WideSubquiver.toType (Quiver.Symmetrify V) T)] (e : Quiver.Total (WideSubquiver.toType (Quiver.Symmetrify V) T)) : symEdgeForgetInv T (symEdgeForget T e) = e

theorem FiniteGraphFreeGroup.symEdgeForget_forgetInv {V : Type u} [Quiver V] (T : WideSubquiver (Quiver.Symmetrify V)) (e : Quiver.Total (WideSubquiver.toType V (Quiver.wideSubquiverSymmetrify T))) : symEdgeForget T (symEdgeForgetInv T e) = e

noncomputable def FiniteGraphFreeGroup.symEdgeEquiv {V : Type u} [Quiver V] (T : WideSubquiver (Quiver.Symmetrify V)) [Quiver.Arborescence (WideSubquiver.toType (Quiver.Symmetrify V) T)] : Quiver.Total (WideSubquiver.toType (Quiver.Symmetrify V) T) ≃ Quiver.Total (WideSubquiver.toType V (Quiver.wideSubquiverSymmetrify T))

Equates oriented tree edges with the underlying edges of the symmetrified subquiver.

Equations

• FiniteGraphFreeGroup.symEdgeEquiv T = { toFun := FiniteGraphFreeGroup.symEdgeForget T, invFun := FiniteGraphFreeGroup.symEdgeForgetInv T, left_inv := ⋯, right_inv := ⋯ }

theorem FiniteGraphFreeGroup.symmetrified_tree_card {V : Type u} [Quiver V] [Fintype V] [(a b : V) → Fintype (a ⟶ b)] (T : WideSubquiver (Quiver.Symmetrify V)) [Quiver.Arborescence (WideSubquiver.toType (Quiver.Symmetrify V) T)] : Fintype.card (Quiver.Total (WideSubquiver.toType V (Quiver.wideSubquiverSymmetrify T))) = Fintype.card V - 1

theorem FiniteGraphFreeGroup.symmetrified_tree_set_card {V : Type u} [Quiver V] [Fintype V] [(a b : V) → Fintype (a ⟶ b)] (T : WideSubquiver (Quiver.Symmetrify V)) [Quiver.Arborescence (WideSubquiver.toType (Quiver.Symmetrify V) T)] : Fintype.card ↑(Quiver.wideSubquiverEquivSetTotal (Quiver.wideSubquiverSymmetrify T)) = Fintype.card V - 1

noncomputable def FiniteGraphFreeGroup.spanningTreeBasis {G : Type u} [CategoryTheory.Groupoid G] [IsFreeGroupoid G] (T : WideSubquiver (Quiver.Symmetrify (IsFreeGroupoid.Generators G))) [Quiver.Arborescence (WideSubquiver.toType (Quiver.Symmetrify (IsFreeGroupoid.Generators G)) T)] : FreeGroupBasis (↑(Quiver.wideSubquiverEquivSetTotal (Quiver.wideSubquiverSymmetrify T))ᶜ) (CategoryTheory.End (have this := Quiver.root (WideSubquiver.toType (Quiver.Symmetrify (IsFreeGroupoid.Generators G)) T); this))

The free-group basis obtained from the arrows outside a spanning tree.

Equations

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

@[instance_reducible]

instance FiniteGraphFreeGroup.freeGroupoidIsFree {V : Type u} [Quiver V] : IsFreeGroupoid (Quiver.FreeGroupoid V)

Equations

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

class FiniteGraphFreeGroup.FiniteQuiver (V : Type u) [Quiver V] : Type u

A quiver with a finite hom-set between every ordered pair of vertices.

• finiteHom (a b : V) : Fintype (a ⟶ b)

  The finite structure on each hom-set.

@[reducible]

instance FiniteGraphFreeGroup.finiteHom {V : Type u} [Quiver V] [FiniteQuiver V] (a b : V) : Fintype (a ⟶ b)

Equations

• FiniteGraphFreeGroup.finiteHom a b = FiniteGraphFreeGroup.FiniteQuiver.finiteHom a b

class FiniteGraphFreeGroup.WeaklyConnected (V : Type u) [Quiver V] : Prop

A quiver whose symmetrification has a path between every pair of vertices.

• path (a b : V) : Nonempty (Quiver.Path a b)

instance FiniteGraphFreeGroup.rootedConnectedFree {V : Type u} [Quiver V] [WeaklyConnected V] (root : V) : Quiver.RootedConnected ((Quiver.FreeGroupoid.of V).obj root)

def FiniteGraphFreeGroup.generatorObjEquiv {V : Type u} [Quiver V] : IsFreeGroupoid.Generators (Quiver.FreeGroupoid V) ≃ V

Identifies the objects of the generated free groupoid with graph vertices.

Equations

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

@[instance_reducible]

noncomputable instance FiniteGraphFreeGroup.freeGroupoidObjFintype {V : Type u} [Quiver V] [Fintype V] : Fintype (IsFreeGroupoid.Generators (Quiver.FreeGroupoid V))

Equations

• FiniteGraphFreeGroup.freeGroupoidObjFintype = Fintype.ofEquiv V FiniteGraphFreeGroup.generatorObjEquiv.symm

@[instance_reducible]

noncomputable instance FiniteGraphFreeGroup.freeGroupoidGeneratorHomFintype {V : Type u} [Quiver V] [FiniteQuiver V] (a b : IsFreeGroupoid.Generators (Quiver.FreeGroupoid V)) : Fintype (a ⟶ b)

Equations

• FiniteGraphFreeGroup.freeGroupoidGeneratorHomFintype a b = id (FiniteGraphFreeGroup.FiniteQuiver.finiteHom a.as b.as)

def FiniteGraphFreeGroup.vertexCount {V : Type u} [Fintype V] : ℕ

The number of vertices in a finite graph.

Equations

• FiniteGraphFreeGroup.vertexCount = Fintype.card V

noncomputable def FiniteGraphFreeGroup.edgeCount {V : Type u} [Quiver V] [Fintype V] [FiniteQuiver V] : ℕ

The total number of directed edges in a finite quiver.

Equations

• FiniteGraphFreeGroup.edgeCount = Fintype.card (Quiver.Total V)

@[reducible, inline]

noncomputable abbrev FiniteGraphFreeGroup.cycleRank {V : Type u} [Quiver V] [Fintype V] [FiniteQuiver V] : ℕ

The graph cycle rank, written to account for truncated subtraction in ℕ.

The spanning-tree inequality below identifies it with E - (V - 1) for a weakly connected graph.

Equations

• FiniteGraphFreeGroup.cycleRank = FiniteGraphFreeGroup.edgeCount + 1 - FiniteGraphFreeGroup.vertexCount

@[reducible, inline]

abbrev FiniteGraphFreeGroup.graphFundamentalGroup {V : Type u} [Quiver V] (root : V) : Type u

The endomorphism group at a root in the free groupoid generated by the graph.

Equations

• FiniteGraphFreeGroup.graphFundamentalGroup root = CategoryTheory.End ((Quiver.FreeGroupoid.of V).obj root)

@[reducible, inline]

abbrev FiniteGraphFreeGroup.graphTree {V : Type u} [Quiver V] [WeaklyConnected V] (root : V) : WideSubquiver (Quiver.Symmetrify (IsFreeGroupoid.Generators (Quiver.FreeGroupoid V)))

The canonical geodesic spanning tree rooted at the chosen graph vertex.

Equations

• FiniteGraphFreeGroup.graphTree root = Quiver.geodesicSubtree ((Quiver.FreeGroupoid.of V).obj root)

@[instance_reducible]

noncomputable instance FiniteGraphFreeGroup.graphTreeArborescence {V : Type u} [Quiver V] [WeaklyConnected V] (root : V) : Quiver.Arborescence (WideSubquiver.toType (Quiver.Symmetrify (IsFreeGroupoid.Generators (Quiver.FreeGroupoid V))) (graphTree root))

Equations

• FiniteGraphFreeGroup.graphTreeArborescence root = inferInstance

def FiniteGraphFreeGroup.generatorTotalEquiv {V : Type u} [Quiver V] : Quiver.Total (IsFreeGroupoid.Generators (Quiver.FreeGroupoid V)) ≃ Quiver.Total V

Identifies total free-groupoid generator arrows with total graph arrows.

Equations

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

noncomputable def FiniteGraphFreeGroup.graphGeneratorSet {V : Type u} [Quiver V] [WeaklyConnected V] (root : V) : Set (Quiver.Total (IsFreeGroupoid.Generators (Quiver.FreeGroupoid V)))

The complement of the geodesic tree, indexed by the actual non-tree generator arrows.

Equations

• FiniteGraphFreeGroup.graphGeneratorSet root = (Quiver.wideSubquiverEquivSetTotal (Quiver.wideSubquiverSymmetrify (FiniteGraphFreeGroup.graphTree root)))ᶜ

@[instance_reducible]

noncomputable instance FiniteGraphFreeGroup.graphGeneratorSetFintype {V : Type u} [Quiver V] [Fintype V] [FiniteQuiver V] [WeaklyConnected V] (root : V) : Fintype ↑(graphGeneratorSet root)

Equations

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

theorem FiniteGraphFreeGroup.graphGeneratorSet_card {V : Type u} [Quiver V] [Fintype V] [FiniteQuiver V] [WeaklyConnected V] (root : V) : Fintype.card ↑(graphGeneratorSet root) = edgeCount + 1 - vertexCount

The final theorem is kept in the original statement form for the Palomar Challenge/Solution correspondence. The reusable, basis-valued API and the consequences of the computation live in Consequences.lean.

theorem FiniteGraphFreeGroup.proved_graph_fundamental_group_free_rank {V : Type u} [Quiver V] [Fintype V] [FiniteQuiver V] [WeaklyConnected V] (root : V) : Nonempty (graphFundamentalGroup root ≃* FreeGroup (Fin (edgeCount + 1 - vertexCount)))