Consequences of the spanning-tree computation

This module exposes the free basis, rank identities, basepoint independence, and abelianization.

The reusable consequences of the spanning-tree computation

The proof file establishes the cardinality calculation and the free-group equivalence required by the Palomar statement. This file exposes the data that is useful to downstream developments: the actual tree basis, basepoint independence, the natural-number cycle-rank identities, and the abelianized version of the computation.

noncomputable def FiniteGraphFreeGroup.graphCycleBasisIndexEquiv {V : Type u} [Quiver V] [Fintype V] [FiniteQuiver V] [WeaklyConnected V] (root : V) : ↑(graphGeneratorSet root) ≃ Fin cycleRank

The finite index type used to enumerate the non-tree edges.

Equations

• FiniteGraphFreeGroup.graphCycleBasisIndexEquiv root = id (⋯ ▸ Fintype.equivFin ↑(FiniteGraphFreeGroup.graphGeneratorSet root))

noncomputable def FiniteGraphFreeGroup.graphFundamentalGroupBasis {V : Type u} [Quiver V] [WeaklyConnected V] (root : V) : FreeGroupBasis (↑(graphGeneratorSet root)) (graphFundamentalGroup root)

The spanning-tree basis of the graph fundamental group.

Its index is the complement of the certified geodesic tree, so the basis remembers which graph edges create the independent cycles rather than merely asserting that some free basis exists.

Equations

• FiniteGraphFreeGroup.graphFundamentalGroupBasis root = id (FiniteGraphFreeGroup.spanningTreeBasis (FiniteGraphFreeGroup.graphTree root))

theorem FiniteGraphFreeGroup.graphFundamentalGroupBasis_repr_apply {V : Type u} [Quiver V] [WeaklyConnected V] (root : V) (e : ↑(graphGeneratorSet root)) : (graphFundamentalGroupBasis root).repr ((graphFundamentalGroupBasis root) e) = FreeGroup.of e

noncomputable def FiniteGraphFreeGroup.graphFundamentalGroupEquiv {V : Type u} [Quiver V] [Fintype V] [FiniteQuiver V] [WeaklyConnected V] (root : V) : graphFundamentalGroup root ≃* FreeGroup (Fin cycleRank)

An explicit equivalence, not just a Nonempty existence statement.

Equations

• FiniteGraphFreeGroup.graphFundamentalGroupEquiv root = ((FiniteGraphFreeGroup.graphFundamentalGroupBasis root).reindex (FiniteGraphFreeGroup.graphCycleBasisIndexEquiv root)).repr

noncomputable def FiniteGraphFreeGroup.graphRootChangeHom {V : Type u} [Quiver V] [WeaklyConnected V] (root₁ root₂ : V) : (Quiver.FreeGroupoid.of V).obj root₁ ⟶ (Quiver.FreeGroupoid.of V).obj root₂

A weak-connectivity path, interpreted as a morphism in the free groupoid.

Equations

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

noncomputable def FiniteGraphFreeGroup.graphFundamentalGroupRootEquiv {V : Type u} [Quiver V] [WeaklyConnected V] (root₁ root₂ : V) : graphFundamentalGroup root₁ ≃* graphFundamentalGroup root₂

Changing the root produces a group equivalence by conjugating along a weak-connectivity path. No finiteness assumption or topological realization is needed.

Equations

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

@[simp]

theorem FiniteGraphFreeGroup.graphFundamentalGroupRootEquiv_refl {V : Type u} [Quiver V] [WeaklyConnected V] (root : V) : graphFundamentalGroupRootEquiv root root = MulEquiv.refl (graphFundamentalGroup root)

theorem FiniteGraphFreeGroup.graph_tree_edge_count_le {V : Type u} [Quiver V] [Fintype V] [FiniteQuiver V] [WeaklyConnected V] (root : V) : vertexCount - 1 ≤ edgeCount

The geodesic tree has V - 1 edges and therefore cannot exceed the edge set.

This identity is the usual E - (V - 1) formula, expressed in ℕ.

theorem FiniteGraphFreeGroup.cycleRank_eq_edgeCount_sub_tree {V : Type u} [Quiver V] [Fintype V] [FiniteQuiver V] [WeaklyConnected V] (root : V) : cycleRank = edgeCount - (vertexCount - 1)

theorem FiniteGraphFreeGroup.cycleRank_pos_iff {V : Type u} [Quiver V] [Fintype V] [FiniteQuiver V] [WeaklyConnected V] (root : V) : 0 < cycleRank ↔ vertexCount - 1 < edgeCount

theorem FiniteGraphFreeGroup.cycleRank_eq_zero_iff_tree_edge_count {V : Type u} [Quiver V] [Fintype V] [FiniteQuiver V] [WeaklyConnected V] (root : V) : cycleRank = 0 ↔ edgeCount = vertexCount - 1

theorem FiniteGraphFreeGroup.graphFundamentalGroup_subsingleton_iff_cycleRank_zero {V : Type u} [Quiver V] [Fintype V] [FiniteQuiver V] [WeaklyConnected V] (root : V) : Subsingleton (graphFundamentalGroup root) ↔ cycleRank = 0

The combinatorial fundamental group is trivial exactly in the tree case.

noncomputable def FiniteGraphFreeGroup.graphFundamentalGroupAbelianizationEquiv {V : Type u} [Quiver V] [Fintype V] [FiniteQuiver V] [WeaklyConnected V] (root : V) : Abelianization (graphFundamentalGroup root) ≃* Abelianization (FreeGroup (Fin cycleRank))

Abelianization preserves the explicitly computed rank.

Equations

• FiniteGraphFreeGroup.graphFundamentalGroupAbelianizationEquiv root = (FiniteGraphFreeGroup.graphFundamentalGroupEquiv root).abelianizationCongr

noncomputable def FiniteGraphFreeGroup.graphFundamentalGroupFreeAbelianizationEquiv {V : Type u} [Quiver V] [Fintype V] [FiniteQuiver V] [WeaklyConnected V] (root : V) : Additive (Abelianization (graphFundamentalGroup root)) ≃+ FreeAbelianGroup (Fin cycleRank)

The additive free-abelian form of the same consequence.

Equations

• FiniteGraphFreeGroup.graphFundamentalGroupFreeAbelianizationEquiv root = MulEquiv.toAdditive (FiniteGraphFreeGroup.graphFundamentalGroupAbelianizationEquiv root)