Antidiagonal of finitely supported functions as finsets

This file defines the finset of finitely functions summing to a specific value on a finset. Such finsets should be thought of as the "antidiagonals" in the space of finitely supported functions.

Precisely, for a commutative monoid μ with antidiagonals (see Finset.HasAntidiagonal), Finset.finsuppAntidiag s n is the finset of all finitely supported functions f : ι →₀ μ with support contained in s and such that the sum of its values equals n : μ.

We define it using Finset.piAntidiag s n, the corresponding antidiagonal in ι → μ.

Main declarations

• Finset.finsuppAntidiag s n: Finset of all finitely supported functions f : ι →₀ μ with support contained in s and such that the sum of its values equals n : μ.

def Finset.finsuppAntidiag {ι : Type u_1} {μ : Type u_2} [DecidableEq ι] [AddCommMonoid μ] [HasAntidiagonal μ] [DecidableEq μ] (s : Finset ι) (n : μ) : Finset (ι →₀ μ)

The finset of functions ι →₀ μ with support contained in s and sum equal to n.

Equations

• s.finsuppAntidiag n = Finset.map { toFun := fun (f : ↥(s.piAntidiag n)) => { support := {x ∈ s | ↑f x ≠ 0}, toFun := ↑f, mem_support_toFun := ⋯ }, inj' := ⋯ } (s.piAntidiag n).attach

@[simp]

theorem Finset.mem_finsuppAntidiag {ι : Type u_1} {μ : Type u_2} [DecidableEq ι] [AddCommMonoid μ] [HasAntidiagonal μ] [DecidableEq μ] {s : Finset ι} {n : μ} {f : ι →₀ μ} : f ∈ s.finsuppAntidiag n ↔ s.sum ⇑f = n ∧ f.support ⊆ s

theorem Finset.mem_finsuppAntidiag' {ι : Type u_1} {μ : Type u_2} [DecidableEq ι] [AddCommMonoid μ] [HasAntidiagonal μ] [DecidableEq μ] {s : Finset ι} {n : μ} {f : ι →₀ μ} : f ∈ s.finsuppAntidiag n ↔ (f.sum fun (x : ι) (x_1 : μ) => x_1) = n ∧ f.support ⊆ s

@[simp]

theorem Finset.finsuppAntidiag_empty_zero {ι : Type u_1} {μ : Type u_2} [DecidableEq ι] [AddCommMonoid μ] [HasAntidiagonal μ] [DecidableEq μ] : ∅.finsuppAntidiag 0 = {0}

@[simp]

theorem Finset.finsuppAntidiag_empty_of_ne_zero {ι : Type u_1} {μ : Type u_2} [DecidableEq ι] [AddCommMonoid μ] [HasAntidiagonal μ] [DecidableEq μ] {n : μ} (hn : n ≠ 0) : ∅.finsuppAntidiag n = ∅

theorem Finset.finsuppAntidiag_empty {ι : Type u_1} {μ : Type u_2} [DecidableEq ι] [AddCommMonoid μ] [HasAntidiagonal μ] [DecidableEq μ] (n : μ) : ∅.finsuppAntidiag n = if n = 0 then {0} else ∅

theorem Finset.mem_finsuppAntidiag_insert {ι : Type u_1} {μ : Type u_2} [DecidableEq ι] [AddCommMonoid μ] [HasAntidiagonal μ] [DecidableEq μ] {a : ι} {s : Finset ι} (h : a ∉ s) (n : μ) {f : ι →₀ μ} : f ∈ (insert a s).finsuppAntidiag n ↔ ∃ m ∈ antidiagonal n, ∃ (g : ι →₀ μ), f = g.update a m.1 ∧ g ∈ s.finsuppAntidiag m.2

theorem Finset.finsuppAntidiag_insert {ι : Type u_1} {μ : Type u_2} [DecidableEq ι] [AddCommMonoid μ] [HasAntidiagonal μ] [DecidableEq μ] {a : ι} {s : Finset ι} (h : a ∉ s) (n : μ) : (insert a s).finsuppAntidiag n = (antidiagonal n).biUnion fun (p : μ × μ) => map { toFun := fun (f : ↥(s.finsuppAntidiag p.2)) => (↑f).update a p.1, inj' := ⋯ } (s.finsuppAntidiag p.2).attach

theorem Finset.finsuppAntidiag_mono {ι : Type u_1} {μ : Type u_2} [DecidableEq ι] [AddCommMonoid μ] [HasAntidiagonal μ] [DecidableEq μ] {s t : Finset ι} (h : s ⊆ t) (n : μ) : s.finsuppAntidiag n ⊆ t.finsuppAntidiag n

theorem Finset.mapRange_finsuppAntidiag_subset {ι : Type u_1} {μ : Type u_2} {μ' : Type u_3} [DecidableEq ι] [AddCommMonoid μ] [HasAntidiagonal μ] [DecidableEq μ] [AddCommMonoid μ'] [HasAntidiagonal μ'] [DecidableEq μ'] {e : μ ≃+ μ'} {s : Finset ι} {n : μ} : map (Finsupp.mapRange.addEquiv e).toEmbedding (s.finsuppAntidiag n) ⊆ s.finsuppAntidiag (e n)

theorem Finset.mapRange_finsuppAntidiag_eq {ι : Type u_1} {μ : Type u_2} {μ' : Type u_3} [DecidableEq ι] [AddCommMonoid μ] [HasAntidiagonal μ] [DecidableEq μ] [AddCommMonoid μ'] [HasAntidiagonal μ'] [DecidableEq μ'] {e : μ ≃+ μ'} {s : Finset ι} {n : μ} : map (Finsupp.mapRange.addEquiv e).toEmbedding (s.finsuppAntidiag n) = s.finsuppAntidiag (e n)

@[simp]

theorem Finset.finsuppAntidiag_zero {ι : Type u_1} {μ : Type u_2} [DecidableEq ι] [DecidableEq μ] [AddCommMonoid μ] [PartialOrder μ] [CanonicallyOrderedAdd μ] [HasAntidiagonal μ] (s : Finset ι) : s.finsuppAntidiag 0 = {0}