Splitting an unordered tuple along a pairwise disjoint family of sets

This file concatenates unordered tuples along a finite family U : ι → Set α of pairwise disjoint sets: a family of unordered tuples, the i-th of them an m i-tuple of points of U i, concatenates into an unordered n-tuple of points of α as soon as ∑ i, m i = n, and the parts are recovered from the whole by filtering on membership in U i.

Nothing here is topological. TauCeti/Topology/Sym/Family.lean upgrades the concatenation to an open embedding when the U i are open, and shows that in a Hausdorff space every unordered tuple lies in the range of such a concatenation, with one member of the family for each of its distinct points and that point's multiplicity as the degree. That is the decomposition which charts the symmetric power of a surface near a tuple with repeated points.

Because the degrees are required to add up to a given n rather than the target degree being literally ∑ i, m i, the concatenation composes with other maps of symmetric powers without a cast.

Main declarations

• TauCeti.Sym.sumSubtype: the concatenation of a family of unordered tuples of points of the members of the family, as an unordered n-tuple of points of α.
• TauCeti.Sym.mem_sumSubtype_iff: if a point of U j belongs to no other member, it lies in the concatenation exactly when it lies in the j-th part.
• TauCeti.Sym.filter_mem_sumSubtype and TauCeti.Sym.sumSubtype_injective: for a pairwise disjoint family the concatenation determines all of its parts.
• TauCeti.Sym.mem_range_sumSubtype: its range consists of the tuples supported in the union of the family with exactly m i of their points in U i.
• TauCeti.Sym.sumSubtype_ofFn: the concatenation read on ordered tuples, along a bijection (Σ i, Fin (m i)) ≃ Fin n.

Ordered tuples and multiplicities

theorem TauCeti.Sym.nonempty_sigmaFinEquiv {ι : Type u_2} [Fintype ι] {m : ι → ℕ} {n : ℕ} (hn : ∑ i : ι, m i = n) : Nonempty ((i : ι) × Fin (m i) ≃ Fin n)

A sigma type of finite sets whose cardinalities add up to n is equivalent to Fin n.

Concatenation along a pairwise disjoint family

def TauCeti.Sym.sumSubtype {α : Type u_1} {ι : Type u_2} [Fintype ι] {n : ℕ} (U : ι → Set α) (m : ι → ℕ) (hn : ∑ i : ι, m i = n) (p : (i : ι) → Sym (↑(U i)) (m i)) : Sym α n

The concatenation of a family of unordered tuples, the i-th of them an unordered m i-tuple of points of U i, read as an unordered n-tuple of points of α, the degrees being required to add up to n.

This is the family used to chart a symmetric power near a tuple with repeated points: one member for each distinct point of the tuple, with its multiplicity as the degree.

Equations

• TauCeti.Sym.sumSubtype U m hn p = ⟨∑ i : ι, Multiset.map Subtype.val ↑(p i), ⋯⟩

@[simp]

theorem TauCeti.Sym.coe_sumSubtype {α : Type u_1} {ι : Type u_2} [Fintype ι] {U : ι → Set α} {m : ι → ℕ} {n : ℕ} (hn : ∑ i : ι, m i = n) (p : (i : ι) → Sym (↑(U i)) (m i)) : ↑(sumSubtype U m hn p) = ∑ i : ι, Multiset.map Subtype.val ↑(p i)

theorem TauCeti.Sym.exists_mem_of_mem_sumSubtype {α : Type u_1} {ι : Type u_2} [Fintype ι] {U : ι → Set α} {m : ι → ℕ} {n : ℕ} {a : α} {hn : ∑ i : ι, m i = n} {p : (i : ι) → Sym (↑(U i)) (m i)} (ha : a ∈ sumSubtype U m hn p) : ∃ (i : ι), a ∈ U i

Every point of a concatenated tuple lies in one of the sets of the family.

theorem TauCeti.Sym.mem_sumSubtype_iff {α : Type u_1} {ι : Type u_2} [Fintype ι] {U : ι → Set α} {m : ι → ℕ} {n : ℕ} {j : ι} {a : α} (h : ∀ (i : ι), i ≠ j → a ∉ U i) {hn : ∑ i : ι, m i = n} {p : (i : ι) → Sym (↑(U i)) (m i)} (ha : a ∈ U j) : a ∈ sumSubtype U m hn p ↔ ⟨a, ha⟩ ∈ p j

If the fixed point belongs to no other member of the family, it lies in a concatenated tuple exactly when it lies in the j-th part.

theorem TauCeti.Sym.filter_mem_sumSubtype {α : Type u_1} {ι : Type u_2} [Fintype ι] {U : ι → Set α} {m : ι → ℕ} {n : ℕ} [(i : ι) → DecidablePred fun (x : α) => x ∈ U i] (h : Pairwise (Function.onFun Disjoint U)) (hn : ∑ i : ι, m i = n) (p : (i : ι) → Sym (↑(U i)) (m i)) (i : ι) : Multiset.filter (fun (x : α) => x ∈ U i) ↑(sumSubtype U m hn p) = Multiset.map Subtype.val ↑(p i)

Filtering a concatenation on membership in U i recovers its i-th part: the other parts contribute nothing, being supported in sets disjoint from U i.

theorem TauCeti.Sym.card_filter_mem_sumSubtype {α : Type u_1} {ι : Type u_2} [Fintype ι] {U : ι → Set α} {m : ι → ℕ} {n : ℕ} [(i : ι) → DecidablePred fun (x : α) => x ∈ U i] (h : Pairwise (Function.onFun Disjoint U)) (hn : ∑ i : ι, m i = n) (p : (i : ι) → Sym (↑(U i)) (m i)) (i : ι) : (Multiset.filter (fun (x : α) => x ∈ U i) ↑(sumSubtype U m hn p)).card = m i

A concatenation has exactly m i points in U i.

theorem TauCeti.Sym.sumSubtype_injective {α : Type u_1} {ι : Type u_2} [Fintype ι] {U : ι → Set α} {m : ι → ℕ} {n : ℕ} (h : Pairwise (Function.onFun Disjoint U)) (hn : ∑ i : ι, m i = n) : Function.Injective (sumSubtype U m hn)

Concatenation along a pairwise disjoint family is injective: each part of the tuple is recovered by filtering on membership in the corresponding set.

theorem TauCeti.Sym.exists_sumSubtype_eq {α : Type u_1} {ι : Type u_2} [Fintype ι] {U : ι → Set α} {m : ι → ℕ} {n : ℕ} [(i : ι) → DecidablePred fun (x : α) => x ∈ U i] (hn : ∑ i : ι, m i = n) {w : Sym α n} (hw : ∀ a ∈ w, ∃ (i : ι), a ∈ U i) (hcard : ∀ (i : ι), (Multiset.filter (fun (x : α) => x ∈ U i) ↑w).card = m i) : ∃ (p : (i : ι) → Sym (↑(U i)) (m i)), sumSubtype U m hn p = w

A tuple supported in the union of a family, with exactly m i of its points in U i, is a concatenation.

theorem TauCeti.Sym.sumSubtype_ofFn {α : Type u_1} {ι : Type u_2} [Fintype ι] {U : ι → Set α} {m : ι → ℕ} {n : ℕ} (hn : ∑ i : ι, m i = n) (e : (i : ι) × Fin (m i) ≃ Fin n) (f : (i : ι) → Fin (m i) → ↑(U i)) : (sumSubtype U m hn fun (i : ι) => ofFn (f i)) = ofFn fun (j : Fin n) => ↑(f (e.symm j).fst (e.symm j).snd)

Concatenation along a family, read on ordered tuples. Along a bijection (Σ i, Fin (m i)) ≃ Fin n the family of ordered tuples regroups into a single ordered n-tuple, and concatenating the unordered tuples they present gives the unordered tuple it presents.

theorem TauCeti.Sym.mem_range_sumSubtype {α : Type u_1} {ι : Type u_2} [Fintype ι] {U : ι → Set α} {m : ι → ℕ} {n : ℕ} [(i : ι) → DecidablePred fun (x : α) => x ∈ U i] (h : Pairwise (Function.onFun Disjoint U)) (hn : ∑ i : ι, m i = n) {w : Sym α n} : w ∈ Set.range (sumSubtype U m hn) ↔ (∀ a ∈ w, ∃ (i : ι), a ∈ U i) ∧ ∀ (i : ι), (Multiset.filter (fun (x : α) => x ∈ U i) ↑w).card = m i

The range of concatenation along a pairwise disjoint family: the unordered tuples supported in the union of the family with exactly m i of their points in U i.