Occurrence-sensitive relabeling of ordered subdivision cores

A cubic-core census most naturally compares only unordered vertex-pair multiplicities. Subdivision transport, however, must also match each parallel slot occurrence and record whether that occurrence is reversed. This module provides that neutral bridge, independently of any genus, atlas, or marked graph application.

Relabeling one core by a vertex permutation

def Utilities.Certificate.ExplicitPotential.Core.relabel {n p : ℕ} (core : Core n p) (vertexPerm : Equiv.Perm (Fin n)) : Core n p

Relabel the vertices of a core while leaving slot occurrences fixed.

Equations

• core.relabel vertexPerm = { tail := fun (edge : Fin p) => vertexPerm (core.tail edge), head := fun (edge : Fin p) => vertexPerm (core.head edge) }

@[simp]

theorem Utilities.Certificate.ExplicitPotential.Core.relabel_tail {n p : ℕ} (core : Core n p) (vertexPerm : Equiv.Perm (Fin n)) (edge : Fin p) : (core.relabel vertexPerm).tail edge = vertexPerm (core.tail edge)

@[simp]

theorem Utilities.Certificate.ExplicitPotential.Core.relabel_head {n p : ℕ} (core : Core n p) (vertexPerm : Equiv.Perm (Fin n)) (edge : Fin p) : (core.relabel vertexPerm).head edge = vertexPerm (core.head edge)

theorem Utilities.Certificate.ExplicitPotential.Core.relabel_loopless {n p : ℕ} (core : Core n p) (vertexPerm : Equiv.Perm (Fin n)) (hLoopless : ∀ (edge : Fin p), core.tail edge ≠ core.head edge) (edge : Fin p) : (core.relabel vertexPerm).tail edge ≠ (core.relabel vertexPerm).head edge

theorem Utilities.Certificate.ExplicitPotential.Core.pairMultiplicity_relabel {n p : ℕ} (core : Core n p) (vertexPerm : Equiv.Perm (Fin n)) (i j : Fin n) : (core.relabel vertexPerm).pairMultiplicity (vertexPerm i) (vertexPerm j) = core.pairMultiplicity i j

theorem Utilities.Certificate.ExplicitPotential.Core.incidenceDegree_relabel {n p : ℕ} (core : Core n p) (vertexPerm : Equiv.Perm (Fin n)) (vertex : Fin n) : (core.relabel vertexPerm).incidenceDegree (vertexPerm vertex) = core.incidenceDegree vertex

theorem Utilities.Certificate.ExplicitPotential.Core.incidenceDegree_relabel_apply {n p : ℕ} (core : Core n p) (vertexPerm : Equiv.Perm (Fin n)) {degree : ℕ} (hDegree : ∀ (vertex : Fin n), core.incidenceDegree vertex = degree) (vertex : Fin n) : (core.relabel vertexPerm).incidenceDegree vertex = degree

theorem Utilities.Certificate.ExplicitPotential.Core.relabel_connected {n p : ℕ} (core : Core n p) (vertexPerm : Equiv.Perm (Fin n)) (hConnected : core.Connected) : (core.relabel vertexPerm).Connected

structure Utilities.Certificate.ExplicitPotential.Core.Relabeling {n p m q : ℕ} (source : Core n p) (target : Core m q) : Type

An occurrence-sensitive relabeling between two ordered cores.

• coreEquiv : Fin n ≃ Fin m

  The bijection of core vertices between the two ordered presentations.

• slotEquiv : Fin p ≃ Fin q

  The bijection of slot occurrences, retaining the distinction between parallel slots.

• reversed : Fin p → Bool

  Whether each source slot has its endpoint orientation reversed in the target presentation.

• tail_eq (edge : Fin p) : target.tail (self.slotEquiv edge) = if self.reversed edge = true then self.coreEquiv (source.head edge) else self.coreEquiv (source.tail edge)
• head_eq (edge : Fin p) : target.head (self.slotEquiv edge) = if self.reversed edge = true then self.coreEquiv (source.tail edge) else self.coreEquiv (source.head edge)

def Utilities.Certificate.ExplicitPotential.Core.Relabeling.reindexedLength {n p m q : ℕ} {source : Core n p} {target : Core m q} (relabeling : source.Relabeling target) (length : Fin p → ℕ) (edge : Fin q) : ℕ

Transport a source length vector through the slot equivalence.

Equations

• relabeling.reindexedLength length edge = length (relabeling.slotEquiv.symm edge)

theorem Utilities.Certificate.ExplicitPotential.Core.Relabeling.reindexedLength_pos {n p m q : ℕ} {source : Core n p} {target : Core m q} (relabeling : source.Relabeling target) (length : Fin p → ℕ) (hLength : ∀ (edge : Fin p), 0 < length edge) (edge : Fin q) : 0 < relabeling.reindexedLength length edge

@[simp]

theorem Utilities.Certificate.ExplicitPotential.Core.Relabeling.reindexedLength_slotEquiv {n p m q : ℕ} {source : Core n p} {target : Core m q} (relabeling : source.Relabeling target) (length : Fin p → ℕ) (edge : Fin p) : relabeling.reindexedLength length (relabeling.slotEquiv edge) = length edge

def Utilities.Certificate.ExplicitPotential.Core.Relabeling.subdivisionRelabeling {n p m q : ℕ} {source : Core n p} {target : Core m q} (relabeling : source.Relabeling target) (source_nonempty : 0 < n) (source_loopless : ∀ (edge : Fin p), source.tail edge ≠ source.head edge) (target_nonempty : 0 < m) (target_loopless : ∀ (edge : Fin q), target.tail edge ≠ target.head edge) (length : Fin p → ℕ) (hLength : ∀ (edge : Fin p), 0 < length edge) : (SubdivisionGraph.Spec.ofCore source source_nonempty source_loopless length hLength).Relabeling (SubdivisionGraph.Spec.ofCore target target_nonempty target_loopless (relabeling.reindexedLength length) ⋯)

The corresponding relabeling of positive subdivision specifications.

Equations

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

def Utilities.Certificate.ExplicitPotential.Core.Relabeling.laplacianEquiv {n p m q : ℕ} {source : Core n p} {target : Core m q} (relabeling : source.Relabeling target) (source_nonempty : 0 < n) (source_loopless : ∀ (edge : Fin p), source.tail edge ≠ source.head edge) (target_nonempty : 0 < m) (target_loopless : ∀ (edge : Fin q), target.tail edge ≠ target.head edge) (length : Fin p → ℕ) (hLength : ∀ (edge : Fin p), 0 < length edge) : LaplacianEquiv (SubdivisionGraph.Spec.ofCore source source_nonempty source_loopless length hLength).graph (SubdivisionGraph.Spec.ofCore target target_nonempty target_loopless (relabeling.reindexedLength length) ⋯).graph

Positive subdivisions of occurrence-relabelled cores are Laplacian equivalent.

Equations

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

Multiplicity fibres

def Utilities.Certificate.ExplicitPotential.Core.edgeKey {n p : ℕ} (core : Core n p) (edge : Fin p) : Sym2 (Fin n)

The unordered endpoint pair of one ordered slot.

Equations

• core.edgeKey edge = s(core.tail edge, core.head edge)

def Utilities.Certificate.ExplicitPotential.Core.mappedEdgeKey {n p m : ℕ} (core : Core n p) (vertexEquiv : Fin n ≃ Fin m) (edge : Fin p) : Sym2 (Fin m)

The endpoint pair after a vertex relabeling.

Equations

• core.mappedEdgeKey vertexEquiv edge = s(vertexEquiv (core.tail edge), vertexEquiv (core.head edge))

theorem Utilities.Certificate.ExplicitPotential.Core.card_edgeKey_fiber {n p : ℕ} (core : Core n p) (i j : Fin n) : Fintype.card { edge : Fin p // core.edgeKey edge = s(i, j) } = core.pairMultiplicity i j

theorem Utilities.Certificate.ExplicitPotential.Core.card_mappedEdgeKey_fiber {n p m : ℕ} (core : Core n p) (vertexEquiv : Fin n ≃ Fin m) (i j : Fin n) : Fintype.card { edge : Fin p // core.mappedEdgeKey vertexEquiv edge = s(vertexEquiv i, vertexEquiv j) } = core.pairMultiplicity i j

theorem Utilities.Certificate.ExplicitPotential.Core.nonempty_relabeling_of_pairMultiplicity_eq {n p m q : ℕ} (source : Core n p) (target : Core m q) (source_loopless : ∀ (edge : Fin p), source.tail edge ≠ source.head edge) (vertexEquiv : Fin n ≃ Fin m) (hMultiplicity : ∀ (i j : Fin n), source.pairMultiplicity i j = target.pairMultiplicity (vertexEquiv i) (vertexEquiv j)) : Nonempty (source.Relabeling target)

A vertex equivalence preserving all unordered pair multiplicities lifts to a full occurrence-sensitive core relabeling.