Tuples mapped into pairwise disjoint ranges

An ordered tuple mapped pointwise into pairwise disjoint ranges is determined by the unordered tuple it presents. This file proves that injectivity statement and characterizes the range by counting how many points lie in each component range. The corresponding topological open embedding is in TauCeti/Topology/Sym/Disjoint.lean.

Main declarations

• TauCeti.Sym.ofFn_map_injective: ordered tuples mapped into pairwise disjoint ranges are determined by the unordered tuples they present, with TauCeti.Sym.mem_range_ofFn_map describing those unordered tuples.

Tuples mapped into pairwise disjoint ranges

theorem TauCeti.Sym.ofFn_map_injective {α : Type u_1} {n : ℕ} {X : Fin n → Type u_2} (f : (i : Fin n) → X i → α) (hf : ∀ (i : Fin n), Function.Injective (f i)) (h : Pairwise (Function.onFun Disjoint fun (i : Fin n) => Set.range (f i))) : Function.Injective fun (x : (i : Fin n) → X i) => ofFn fun (i : Fin n) => f i (x i)

An ordered tuple mapped pointwise into pairwise disjoint ranges is determined by the unordered tuple it presents. A permutation matching two such tuples must fix every index.

theorem TauCeti.Sym.mem_range_ofFn_map {α : Type u_1} {n : ℕ} {X : Fin n → Type u_2} (f : (i : Fin n) → X i → α) (h : Pairwise (Function.onFun Disjoint fun (i : Fin n) => Set.range (f i))) {w : Sym α n} : (w ∈ Set.range fun (x : (i : Fin n) → X i) => ofFn fun (i : Fin n) => f i (x i)) ↔ ∀ (i : Fin n), (Multiset.filter (fun (x : α) => x ∈ Set.range (f i)) ↑w).card = 1

The range of ordered tuples mapped pointwise into pairwise disjoint ranges consists exactly of the unordered tuples having one point in each range.