Extending a finite matching to a permutation respecting an equivalence relation #
Generic lemma (exists_equiv_of_matching): for an equivalence relation E on a type X
and finite families r s : Fin m → X with E (r j) (s j) that are compatible
(r j = r j' ↔ s j = s j', so repeated entries match consistently and the induced partial map is
well defined and injective), there is a permutation e : X ≃ X with e (r j) = s j, with
E x (e x) everywhere, and fixing every point outside the finite union of the sources and
targets. Proof by induction on m: an entry already handled by an earlier repeat is skipped;
otherwise the current permutation is followed by the transposition of s j and e (r j), which
respects E because both are E-related to r j, and moves only points of the finite union.
exists_equiv_of_matching_injective is the injective special case.
Pure combinatorics; no model theory. The names keep their original location in the
FiberAssembly namespace, where the lemma was first used.
The generic lemma #
Extending a finite compatible matching. For an equivalence relation E, families
r s : Fin m → X with E (r j) (s j) and r j = r j' ↔ s j = s j' extend to a permutation
e with e (r j) = s j, E x (e x) for all x, and e x = x for x outside the sources and
targets.
The injective special case: distinct sources and distinct targets.