Relabeling contracted subdivisions

This is the closed-face analogue of SubdivisionIso. The core vertices of a DegSpec are quotient classes, rather than Fin n; consequently a symmetry on the uncontracted core is not by itself enough to relabel a face. A caller must also provide the induced equivalence of the fixed-point classes.

Keeping that class equivalence explicit is intentional. In particular it lets an AUTO certificate replay the finite class map selected by its checker, without claiming that compFold's canonical representatives commute with a permutation definitionally.

Slot reversal is part of the datum, just as it is for the positive-length SubdivisionGraph.Spec.Relabeling. It changes only the finite coordinates inside a surviving slot; the quotient-class boundary is unchanged.

structure Utilities.Certificate.DegenerateSpec.DegSpec.Relabeling {n p n' p' : ℕ} (source : DegSpec n p) (target : DegSpec n' p') : Type

An occurrence-sensitive, orientation-preserving relabeling of two closed subdivision presentations. classEquiv is the essential extra datum beyond SubdivisionGraph.Spec.Relabeling: it names the bijection after zero slots have identified core vertices.

• classEquiv : source.Class ≃ target.Class

  The bijection of surviving core classes after each presentation has identified its zero-slot endpoints.

• slotEquiv : Fin p ≃ Fin p'

  The bijection of source and target slot occurrences, including slots of length zero.

• reversed : Fin p → Bool

  Whether a source slot is mapped with its endpoint orientation reversed.

• length_eq (e : Fin p) : source.length e = target.length (self.slotEquiv e)
• tail_eq (e : Fin p) : (if self.reversed e = true then self.classEquiv ⟨source.rep (source.core.head e), ⋯⟩ else self.classEquiv ⟨source.rep (source.core.tail e), ⋯⟩) = ⟨target.rep (target.core.tail (self.slotEquiv e)), ⋯⟩
• head_eq (e : Fin p) : (if self.reversed e = true then self.classEquiv ⟨source.rep (source.core.tail e), ⋯⟩ else self.classEquiv ⟨source.rep (source.core.head e), ⋯⟩) = ⟨target.rep (target.core.head (self.slotEquiv e)), ⋯⟩

def Utilities.Certificate.DegenerateSpec.DegSpec.Relabeling.interiorEquiv {n p n' p' : ℕ} (source : DegSpec n p) (target : DegSpec n' p') (r : source.Relabeling target) (e : Fin p) : Fin (source.length e - 1) ≃ Fin (target.length (r.slotEquiv e) - 1)

Interior coordinates on a reversed slot are read from the other end.

Equations

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

def Utilities.Certificate.DegenerateSpec.DegSpec.Relabeling.stepOffsetEquiv {n p n' p' : ℕ} (source : DegSpec n p) (target : DegSpec n' p') (r : source.Relabeling target) (e : Fin p) : Fin (source.length e) ≃ Fin (target.length (r.slotEquiv e))

Unit-step coordinates on a reversed slot are read from the other end.

Equations

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

def Utilities.Certificate.DegenerateSpec.DegSpec.Relabeling.vertexEquiv {n p n' p' : ℕ} (source : DegSpec n p) (target : DegSpec n' p') (r : source.Relabeling target) : source.Vertex ≃ target.Vertex

The vertex equivalence induced by a closed-face relabeling.

Equations

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

def Utilities.Certificate.DegenerateSpec.DegSpec.Relabeling.stepEquiv {n p n' p' : ℕ} (source : DegSpec n p) (target : DegSpec n' p') (r : source.Relabeling target) : source.Step ≃ target.Step

The unit-step occurrence equivalence induced by a closed-face relabeling.

Equations

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

@[simp]

theorem Utilities.Certificate.DegenerateSpec.DegSpec.Relabeling.vertexEquiv_coreVertex {n p n' p' : ℕ} (source : DegSpec n p) (target : DegSpec n' p') (r : source.Relabeling target) (v : Fin n) : (vertexEquiv source target r) (source.coreVertex v) = Sum.inl (r.classEquiv ⟨source.rep v, ⋯⟩)

@[simp]

theorem Utilities.Certificate.DegenerateSpec.DegSpec.Relabeling.vertexEquiv_interiorVertex {n p n' p' : ℕ} (source : DegSpec n p) (target : DegSpec n' p') (r : source.Relabeling target) (e : Fin p) (o : Fin (source.length e - 1)) : (vertexEquiv source target r) (source.interiorVertex e o) = target.interiorVertex (r.slotEquiv e) ((interiorEquiv source target r e) o)

@[simp]

theorem Utilities.Certificate.DegenerateSpec.DegSpec.Relabeling.stepEquiv_apply {n p n' p' : ℕ} (source : DegSpec n p) (target : DegSpec n' p') (r : source.Relabeling target) (e : Fin p) (o : Fin (source.length e)) : (stepEquiv source target r) ⟨e, o⟩ = ⟨r.slotEquiv e, (stepOffsetEquiv source target r e) o⟩

theorem Utilities.Certificate.DegenerateSpec.DegSpec.Relabeling.vertexEquiv_tail_of_not_reversed {n p n' p' : ℕ} (source : DegSpec n p) (target : DegSpec n' p') (r : source.Relabeling target) (e : Fin p) (hr : r.reversed e = false) : (vertexEquiv source target r) (source.coreVertex (source.core.tail e)) = target.coreVertex (target.core.tail (r.slotEquiv e))

theorem Utilities.Certificate.DegenerateSpec.DegSpec.Relabeling.vertexEquiv_head_of_not_reversed {n p n' p' : ℕ} (source : DegSpec n p) (target : DegSpec n' p') (r : source.Relabeling target) (e : Fin p) (hr : r.reversed e = false) : (vertexEquiv source target r) (source.coreVertex (source.core.head e)) = target.coreVertex (target.core.head (r.slotEquiv e))

theorem Utilities.Certificate.DegenerateSpec.DegSpec.Relabeling.vertexEquiv_tail_of_reversed {n p n' p' : ℕ} (source : DegSpec n p) (target : DegSpec n' p') (r : source.Relabeling target) (e : Fin p) (hr : r.reversed e = true) : (vertexEquiv source target r) (source.coreVertex (source.core.tail e)) = target.coreVertex (target.core.head (r.slotEquiv e))

theorem Utilities.Certificate.DegenerateSpec.DegSpec.Relabeling.vertexEquiv_head_of_reversed {n p n' p' : ℕ} (source : DegSpec n p) (target : DegSpec n' p') (r : source.Relabeling target) (e : Fin p) (hr : r.reversed e = true) : (vertexEquiv source target r) (source.coreVertex (source.core.head e)) = target.coreVertex (target.core.tail (r.slotEquiv e))

theorem Utilities.Certificate.DegenerateSpec.DegSpec.Relabeling.stepLeft_map_of_not_reversed {n p n' p' : ℕ} (source : DegSpec n p) (target : DegSpec n' p') (r : source.Relabeling target) (e : Fin p) (o : Fin (source.length e)) (hr : r.reversed e = false) : target.stepLeft (r.slotEquiv e) ((stepOffsetEquiv source target r e) o) = (vertexEquiv source target r) (source.stepLeft e o)

theorem Utilities.Certificate.DegenerateSpec.DegSpec.Relabeling.stepRight_map_of_not_reversed {n p n' p' : ℕ} (source : DegSpec n p) (target : DegSpec n' p') (r : source.Relabeling target) (e : Fin p) (o : Fin (source.length e)) (hr : r.reversed e = false) : target.stepRight (r.slotEquiv e) ((stepOffsetEquiv source target r e) o) = (vertexEquiv source target r) (source.stepRight e o)

theorem Utilities.Certificate.DegenerateSpec.DegSpec.Relabeling.stepLeft_map_of_reversed {n p n' p' : ℕ} (source : DegSpec n p) (target : DegSpec n' p') (r : source.Relabeling target) (e : Fin p) (o : Fin (source.length e)) (hr : r.reversed e = true) : target.stepLeft (r.slotEquiv e) ((stepOffsetEquiv source target r e) o) = (vertexEquiv source target r) (source.stepRight e o)

theorem Utilities.Certificate.DegenerateSpec.DegSpec.Relabeling.stepRight_map_of_reversed {n p n' p' : ℕ} (source : DegSpec n p) (target : DegSpec n' p') (r : source.Relabeling target) (e : Fin p) (o : Fin (source.length e)) (hr : r.reversed e = true) : target.stepRight (r.slotEquiv e) ((stepOffsetEquiv source target r e) o) = (vertexEquiv source target r) (source.stepLeft e o)

theorem Utilities.Certificate.DegenerateSpec.DegSpec.Relabeling.unitEdge_stepEquiv {n p n' p' : ℕ} (source : DegSpec n p) (target : DegSpec n' p') (r : source.Relabeling target) (s : source.Step) : target.unitEdge ((stepEquiv source target r) s) = ((vertexEquiv source target r) (source.unitEdge s).1, (vertexEquiv source target r) (source.unitEdge s).2) ∨ target.unitEdge ((stepEquiv source target r) s) = ((vertexEquiv source target r) (source.unitEdge s).2, (vertexEquiv source target r) (source.unitEdge s).1)

noncomputable def Utilities.Certificate.DegenerateSpec.DegSpec.Relabeling.laplacianEquiv {n p n' p' : ℕ} (source : DegSpec n p) (target : DegSpec n' p') (r : source.Relabeling target) : LaplacianEquiv source.graph target.graph

A vertex and unit-step bijection preserving endpoints gives the closed face Laplacian equivalence. This copy is polymorphic in DegSpec, while the older helper is specialized to positive SubdivisionGraph.Specs.

Equations

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

theorem Utilities.Certificate.DegenerateSpec.DegSpec.Relabeling.bnExists_iff {n p n' p' : ℕ} (source : DegSpec n p) (target : DegSpec n' p') (r : source.Relabeling target) (rnk deg : ℤ) : BNExists target.graph rnk deg ↔ BNExists source.graph rnk deg