English
There is a natural equivalence between the nth symmetric power of insert a s and the sigma-type Σ i Fin(n+1) · s^{(n−i)} when a ∉ s, given by a natural forward and inverse construction.
Русский
Существует естественная биекция между n-ой симметрической мощностью вставки a в s и суммарным типом Σ i Fin(n+1) · s^{(n−i)} при условии a ∉ s, заданная естественным переходом вперёд и обратно.
LaTeX
$$$ (\\mathrm{sym}^n(\\mathrm{insert}\\ a\\ s)) \\cong \\Sigma i: Fin(n+1), s^{(n-i)} \\quad (a \\notin s)$$
Lean4
/-- If `a` does not belong to the finset `s`, then the `n`th symmetric power of `{a} ∪ s` is
in 1-1 correspondence with the disjoint union of the `n - i`th symmetric powers of `s`,
for `0 ≤ i ≤ n`. -/
@[simps]
def symInsertEquiv (h : a ∉ s) : (insert a s).sym n ≃ Σ i : Fin (n + 1), s.sym (n - i)
where
toFun m := ⟨_, (m.1.filterNe a).2, by convert sym_filterNe_mem a m.2; rw [erase_insert h]⟩
invFun m := ⟨m.2.1.fill a m.1, sym_fill_mem a m.2.2⟩
left_inv m := Subtype.ext <| m.1.fill_filterNe a
right_inv := fun ⟨i, m, hm⟩ ↦
by
refine Function.Injective.sigma_map (β₂ := ?_) (f₂ := ?_) (Function.injective_id) (fun i ↦ ?_) ?_
· exact fun i ↦ Sym α (n - i)
swap
· exact Subtype.coe_injective
refine Eq.trans ?_ (Sym.filter_ne_fill a _ ?_)
exacts [rfl, h ∘ mem_sym_iff.1 hm a]
