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 add 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 add 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

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.

Documentation

Mathlib.Algebra.Order.Antidiag.Prod

Antidiagonal with values in general types #

TODO #