The occurrence presentation of a unit-length subdivision spec

regularSubdivision G k (Utilities/Gonality/GonalityTransport.lean) builds σ_k(G) on the occurrence presentation of G, which labels vertices and edge occurrences by arbitrary Fintype.equivFin bijections. A graph that is already given as spec.graph for a unit-length spec : Spec n p therefore has two descriptions of σ_k, and this module shows they agree:

Nonempty (LaplacianEquiv (spec.scale k hk).graph (regularSubdivision spec.graph k hk))

The content is a slot correspondence. spec.graph.edges is Multiset.map spec.unitEdge univ, so its multiset-as-type (x : V × V) × Fin (count x) is equivalent to spec.Step — compatibly with unitEdge, which is the only property the endpoint conditions of a Spec.Relabeling need. With unit lengths spec.Step ≃ Fin p and spec.Vertex ≃ Fin n, and the relabeling assembles.

The payoff is that the tricycle gap can be stated for regularSubdivisionGonality : CFGraph → ℕ, with no Spec in the statement.

The multiset of edges, as a type

noncomputable def Utilities.Certificate.SubdivisionGraph.Spec.stepEquivEdges {n p : ℕ} (spec : Spec n p) : spec.Step ≃ spec.graph.edges.ToType

The slot correspondence. The edge multiset of a subdivision, viewed as a type, enumerates the unit steps — compatibly with unitEdge.

Equations

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

@[simp]

theorem Utilities.Certificate.SubdivisionGraph.Spec.stepEquivEdges_coe {n p : ℕ} (spec : Spec n p) (step : spec.Step) : (spec.stepEquivEdges step).fst = spec.unitEdge step

Unit-length specs

def Utilities.Certificate.SubdivisionGraph.Spec.unitVertexEquiv {n p : ℕ} (spec : Spec n p) (hlen : ∀ (e : Fin p), spec.length e = 1) : Fin n ≃ spec.Vertex

With all lengths one there are no interior vertices.

Equations

• spec.unitVertexEquiv hlen = { toFun := spec.coreVertex, invFun := Sum.elim id fun (y : spec.Interior) => absurd ⋯ ⋯, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem Utilities.Certificate.SubdivisionGraph.Spec.unitVertexEquiv_apply {n p : ℕ} (spec : Spec n p) (hlen : ∀ (e : Fin p), spec.length e = 1) (v : Fin n) : (spec.unitVertexEquiv hlen) v = spec.coreVertex v

def Utilities.Certificate.SubdivisionGraph.Spec.unitStepEquiv {n p : ℕ} (spec : Spec n p) (hlen : ∀ (e : Fin p), spec.length e = 1) : Fin p ≃ spec.Step

With all lengths one, every slot has exactly one unit step.

Equations

• spec.unitStepEquiv hlen = { toFun := fun (e : Fin p) => ⟨e, ⟨0, ⋯⟩⟩, invFun := fun (step : spec.Step) => step.fst, left_inv := ⋯, right_inv := ⋯ }

theorem Utilities.Certificate.SubdivisionGraph.Spec.unitEdge_unitStepEquiv {n p : ℕ} (spec : Spec n p) (hlen : ∀ (e : Fin p), spec.length e = 1) (e : Fin p) : spec.unitEdge ((spec.unitStepEquiv hlen) e) = (spec.coreVertex (spec.core.tail e), spec.coreVertex (spec.core.head e))

The relabeling

noncomputable def Utilities.Certificate.SubdivisionGraph.Spec.unitCoreEquiv {n p : ℕ} (spec : Spec n p) (hlen : ∀ (e : Fin p), spec.length e = 1) : Fin n ≃ Fin (Fintype.card spec.graph.V)

The vertex labelling used by the occurrence presentation, restricted to the core vertices.

Equations

• spec.unitCoreEquiv hlen = (spec.unitVertexEquiv hlen).trans (Utilities.Certificate.UnitSubdivisionPresentation.vertexEquiv spec.graph)

noncomputable def Utilities.Certificate.SubdivisionGraph.Spec.unitSlotEquiv {n p : ℕ} (spec : Spec n p) (hlen : ∀ (e : Fin p), spec.length e = 1) : Fin p ≃ Fin spec.graph.edges.card

The slot labelling used by the occurrence presentation.

Equations

• spec.unitSlotEquiv hlen = ((spec.unitStepEquiv hlen).trans spec.stepEquivEdges).trans (Utilities.Certificate.UnitSubdivisionPresentation.edgeEquiv spec.graph)

theorem Utilities.Certificate.SubdivisionGraph.Spec.edgeAt_unitSlotEquiv {n p : ℕ} (spec : Spec n p) (hlen : ∀ (e : Fin p), spec.length e = 1) (e : Fin p) : UnitSubdivisionPresentation.edgeAt spec.graph ((spec.unitSlotEquiv hlen) e) = (spec.coreVertex (spec.core.tail e), spec.coreVertex (spec.core.head e))

noncomputable def Utilities.Certificate.SubdivisionGraph.Spec.scaleRelabeling {n p : ℕ} (spec : Spec n p) (hlen : ∀ (e : Fin p), spec.length e = 1) (k : ℕ) (hk : 0 < k) : (spec.scale k hk).Relabeling ((UnitSubdivisionPresentation.spec spec.graph).scale k hk)

The two presentations of σ_k agree.

Equations

• spec.scaleRelabeling hlen k hk = { coreEquiv := spec.unitCoreEquiv hlen, slotEquiv := spec.unitSlotEquiv hlen, reversed := fun (x : Fin p) => false, length_eq := ⋯, tail_eq := ⋯, head_eq := ⋯ }

noncomputable def Utilities.Certificate.SubdivisionGraph.Spec.scaleLaplacianEquiv {n p : ℕ} (spec : Spec n p) (hlen : ∀ (e : Fin p), spec.length e = 1) (k : ℕ) (hk : 0 < k) : LaplacianEquiv (spec.scale k hk).graph (Gonality.regularSubdivision spec.graph k hk)

The bridge. For a unit-length subdivision specification, scaling the specification by k and building σ_k on the occurrence presentation of its graph give the same graph up to Laplacian equivalence.

Equations

• spec.scaleLaplacianEquiv hlen k hk = (spec.scale k hk).laplacianEquiv ((Utilities.Certificate.UnitSubdivisionPresentation.spec spec.graph).scale k hk) (spec.scaleRelabeling hlen k hk)

theorem Utilities.Certificate.SubdivisionGraph.Spec.divisorialGonality_regularSubdivision {n p : ℕ} (spec : Spec n p) (hlen : ∀ (e : Fin p), spec.length e = 1) (k : ℕ) (hk : 0 < k) : Gonality.divisorialGonality (Gonality.regularSubdivision spec.graph k hk) = Gonality.divisorialGonality (spec.scale k hk).graph

theorem Utilities.Certificate.SubdivisionGraph.Spec.regularSubdivisionGonality_graph {n p : ℕ} (spec : Spec n p) (hlen : ∀ (e : Fin p), spec.length e = 1) : Gonality.regularSubdivisionGonality spec.graph = spec.regularSubdivisionGonality

The CFGraph-level invariant agrees with the Spec-level one on a unit-length specification.