# Antidiagonal with values in general types #

We define a type class `Finset.HasAntidiagonal A` which contains a function `antidiagonal : A → Finset (A × A)` such that `antidiagonal n` is the finset of all pairs adding to `n`, as witnessed by `mem_antidiagonal`.

When `A` is a canonically ordered additive monoid with locally finite order this typeclass can be instantiated with `Finset.antidiagonalOfLocallyFinite`. This applies in particular when `A` is `ℕ`, more generally or `σ →₀ ℕ`, or even `ι →₀ A` under the additional assumption `OrderedSub A` that make it a canonically ordered additive monoid. (In fact, we would just need an `AddMonoid` with a compatible order, finite `Iic`, such that if `a + b = n`, then `a, b ≤ n`, and any finiteness condition would be OK.)

For computational reasons it is better to manually provide instances for `ℕ` and `σ →₀ ℕ`, to avoid quadratic runtime performance. These instances are provided as `Finset.Nat.instHasAntidiagonal` and `Finsupp.instHasAntidiagonal`. This is why `Finset.antidiagonalOfLocallyFinite` is an `abbrev` and not an `instance`.

This definition does not exactly match with that of `Multiset.antidiagonal` defined in `Mathlib/Data/Multiset/Antidiagonal.lean`, because of the multiplicities. Indeed, by counting multiplicities, `Multiset α` is equivalent to `α →₀ ℕ`, but `Finset.antidiagonal` and `Multiset.antidiagonal` will return different objects. For example, for `s : Multiset ℕ := {0,0,0}`, `Multiset.antidiagonal s` has 8 elements but `Finset.antidiagonal s` has only 4.

    def s : Multiset ℕ := {0, 0, 0}
    #eval (Finset.antidiagonal s).card -- 4
    #eval Multiset.card (Multiset.antidiagonal s) -- 8

## TODO #

- Define `HasMulAntidiagonal` (for monoids). For `PNat`, we will recover the set of divisors of a strictly positive integer.

source
class Finset.HasAntidiagonal (A : Type u_1) [AddMonoid A] :
Type u_1

The class of additive monoids with an antidiagonal

- antidiagonal : A → Finset (A × A)

  The antidiagonal of an element `n` is the finset of pairs `(i, j)` such that `i + j = n`.

- mem_antidiagonal {n : A} {a : A × A} : a ∈ antidiagonal n ↔ a.1 + a.2 = n

  A pair belongs to `antidiagonal n` iff the sum of its components is equal to `n`.

Instances

source
instance Finset.instSubsingletonHasAntidiagonal {A : Type u_1} [AddMonoid A] :
Subsingleton (HasAntidiagonal A)

All `HasAntidiagonal` instances are equal

source
theorem Finset.hasAntidiagonal_congr (A : Type u_2) [AddMonoid A] [H1 : HasAntidiagonal A] [H2 : HasAntidiagonal A] :
antidiagonal = antidiagonal
source
theorem Finset.swap_mem_antidiagonal {A : Type u_1} [AddCommMonoid A] [HasAntidiagonal A] {n : A} {xy : A × A} :
xy.swap ∈ antidiagonal n ↔ xy ∈ antidiagonal n
source
@[simp]
theorem Finset.map_prodComm_antidiagonal {A : Type u_1} [AddCommMonoid A] [HasAntidiagonal A] {n : A} :
map (Equiv.prodComm A A).toEmbedding (antidiagonal n) = antidiagonal n
source
@[simp]
theorem Finset.map_swap_antidiagonal {A : Type u_1} [AddCommMonoid A] [HasAntidiagonal A] {n : A} :
map { toFun := Prod.swap, inj' := ⋯ } (antidiagonal n) = antidiagonal n

See also `Finset.map_prodComm_antidiagonal`.

source
theorem Finset.antidiagonal_congr {A : Type u_1} [AddCancelMonoid A] [HasAntidiagonal A] {p q : A × A} {n : A} (hp : p ∈ antidiagonal n) (hq : q ∈ antidiagonal n) :
p = q ↔ p.1 = q.1

A point in the antidiagonal is determined by its first coordinate.

See also `Finset.antidiagonal_congr'`.

source
theorem Finset.antidiagonal_subtype_ext {A : Type u_1} [AddCancelMonoid A] [HasAntidiagonal A] {n : A} {p q : ↥(antidiagonal n)} (h : (↑p).1 = (↑q).1) :
p = q

A point in the antidiagonal is determined by its first co-ordinate (subtype version of `Finset.antidiagonal_congr`). This lemma is used by the `ext` tactic.

source
theorem Finset.antidiagonal_subtype_ext_iff {A : Type u_1} [AddCancelMonoid A] [HasAntidiagonal A] {n : A} {p q : ↥(antidiagonal n)} :
p = q ↔ (↑p).1 = (↑q).1
source
theorem Finset.antidiagonal_congr' {A : Type u_1} [AddCancelCommMonoid A] [HasAntidiagonal A] {p q : A × A} {n : A} (hp : p ∈ antidiagonal n) (hq : q ∈ antidiagonal n) :
p = q ↔ p.2 = q.2

A point in the antidiagonal is determined by its second coordinate.

See also `Finset.antidiagonal_congr`.

source
@[simp]
theorem Finset.antidiagonal_zero {A : Type u_1} [AddCommMonoid A] [PartialOrder A] [CanonicallyOrderedAdd A] [HasAntidiagonal A] :
antidiagonal 0 = {(0, 0)}
source
theorem Finset.antidiagonal.fst_le {A : Type u_1} [AddCommMonoid A] [PartialOrder A] [CanonicallyOrderedAdd A] [HasAntidiagonal A] {n : A} {kl : A × A} (hlk : kl ∈ antidiagonal n) :
kl.1 ≤ n
source
theorem Finset.antidiagonal.snd_le {A : Type u_1} [AddCommMonoid A] [PartialOrder A] [CanonicallyOrderedAdd A] [HasAntidiagonal A] {n : A} {kl : A × A} (hlk : kl ∈ antidiagonal n) :
kl.2 ≤ n
source
theorem Finset.filter_fst_eq_antidiagonal {A : Type u_1} [AddCommMonoid A] [PartialOrder A] [CanonicallyOrderedAdd A] [Sub A] [OrderedSub A] [AddLeftReflectLE A] [HasAntidiagonal A] (n m : A) [DecidablePred fun (x : A) => x = m] [Decidable (m ≤ n)] :
{x ∈ antidiagonal n | x.1 = m} = if m ≤ n then {(m, n - m)} else ∅
source
theorem Finset.filter_snd_eq_antidiagonal {A : Type u_1} [AddCommMonoid A] [PartialOrder A] [CanonicallyOrderedAdd A] [Sub A] [OrderedSub A] [AddLeftReflectLE A] [HasAntidiagonal A] (n m : A) [DecidablePred fun (x : A) => x = m] [Decidable (m ≤ n)] :
{x ∈ antidiagonal n | x.2 = m} = if m ≤ n then {(n - m, m)} else ∅
source
def Finset.sigmaAntidiagonalEquivProd {A : Type u_1} [AddMonoid A] [HasAntidiagonal A] :
(n : A) × ↥(antidiagonal n) ≃ A × A

The disjoint union of antidiagonals `Σ (n : A), antidiagonal n` is equivalent to the product `A × A`. This is such an equivalence, obtained by mapping `(n, (k, l))` to `(k, l)`.

Equations

- Finset.sigmaAntidiagonalEquivProd = { toFun := fun (x : (n : A) × ↥(Finset.antidiagonal n)) => ↑x.snd, invFun := fun (x : A × A) => ⟨x.1 + x.2, ⟨x, ⋯⟩⟩, left_inv := ⋯, right_inv := ⋯ }

Instances For

source
@[simp]
theorem Finset.sigmaAntidiagonalEquivProd_symm_apply_fst {A : Type u_1} [AddMonoid A] [HasAntidiagonal A] (x : A × A) :
(sigmaAntidiagonalEquivProd.symm x).fst = x.1 + x.2
source
@[simp]
theorem Finset.sigmaAntidiagonalEquivProd_symm_apply_snd_coe {A : Type u_1} [AddMonoid A] [HasAntidiagonal A] (x : A × A) :
↑(sigmaAntidiagonalEquivProd.symm x).snd = x
source
@[simp]
theorem Finset.sigmaAntidiagonalEquivProd_apply {A : Type u_1} [AddMonoid A] [HasAntidiagonal A] (x : (n : A) × ↥(antidiagonal n)) :
sigmaAntidiagonalEquivProd x = ↑x.snd
source
@[reducible, inline]
abbrev Finset.antidiagonalOfLocallyFinite {A : Type u_2} [AddCommMonoid A] [PartialOrder A] [CanonicallyOrderedAdd A] [LocallyFiniteOrderBot A] [DecidableEq A] :
HasAntidiagonal A

In a canonically ordered additive monoid, the antidiagonal can be construct by filtering.

Note that this is not an instance, as for some times a more efficient algorithm is available.

Equations

- Finset.antidiagonalOfLocallyFinite = { antidiagonal := fun (n : A) => {uv ∈ Finset.Iic n ×ˢ Finset.Iic n | uv.1 + uv.2 = n}, mem_antidiagonal := ⋯ }

Instances For