toEquivTriple
plain-language theorem explainer
Projects an exact-complex relabeling to its underlying triple of index bijections on vertices, edges, and tetrahedra, discarding the incidence-commutation proofs. Anyone proving that relabelings are determined by those bijections, or building the total torsor of relabelings, cites this forgetful map. The body is a one-line field projection.
Claim. Given a relabeling isomorphism $r$ between two exact combinatorial complexes of the same signature $(v,e,t)$, return the triple of index bijections $(r_V : \mathrm{Fin}\,v \simeq \mathrm{Fin}\,v,\; r_E : \mathrm{Fin}\,e \simeq \mathrm{Fin}\,e,\; r_T : \mathrm{Fin}\,t \simeq \mathrm{Fin}\,t)$ carried by $r$.
background
The ambient module builds exact complexity shells for the quotient-class path sum: configurations with fixed vertex/edge/tetrahedron counts and no size caps, then a Gaussian UV-regulated shell series. Honesty tags in the module doc stress that the regulator is inserted by hand and regulator removal remains open.
An exact complex of signature $(v,e,t)$ is abstract incidence data: edge endpoints in $\mathrm{Fin},v$ and tetrahedron vertex maps $\mathrm{Fin},4\to\mathrm{Fin},v$, with no cap inequalities. A relabeling between two such complexes is a triple of bijections on the three index sets that commute with those incidence maps (edge and tet commutation fields are propositions).
This definition is the exact-shell twin of the same forgetful map on capped BoundedComplex relabelings in PathSumMeasure. It isolates the group-like data (the bijection triple) from the proof obligations that make the triple a genuine isomorphism of incidence structures.
proof idea
One-line field projection: pack the three equivalence fields of the relabeling structure into a product of equivalences. No lemmas, no tactics; the commutation propositions are simply dropped from the type.
why it matters
This forgetful map is the hinge for extensionality of exact relabelings: injectivity of the projection yields that two relabelings with equal index bijections are equal (commutation fields being props). Downstream, toEquivTriple_injective and ext in this module, and the parallel pair in PathSumMeasure, rest on it.
It also supplies the inverse direction of the total torsor in RegulatorRemovalNoGo.relabelSigmaEquiv: every pair (target complex, witness relabeling) recovers a unique triple in the full relabeling group via this projection. That torsor is infrastructure for gauge-orbit bookkeeping on exact shells, not a continuum or regulator-removal claim. The module still leaves HasZRSRegulatorRemoval open and flips no continuum-limit ledger flag.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.