Documentation

Mathlib.Algebra.Order.Antidiag.Prod

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, 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 #

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

The class of additive monoids with an antidiagonal

  • antidiagonal : AFinset (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 Finset.antidiagonal n a.1 + a.2 = n

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

Instances
    @[simp]
    theorem Finset.HasAntidiagonal.mem_antidiagonal {A : Type u_1} :
    ∀ {inst : AddMonoid A} [self : Finset.HasAntidiagonal A] {n : A} {a : A × A}, a Finset.antidiagonal n a.1 + a.2 = n

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

    All HasAntidiagonal instances are equal

    Equations
    • =
    theorem Finset.hasAntidiagonal_congr (A : Type u_2) [AddMonoid A] [H1 : Finset.HasAntidiagonal A] [H2 : Finset.HasAntidiagonal A] :
    Finset.antidiagonal = Finset.antidiagonal
    theorem Finset.antidiagonal_congr {A : Type u_1} [AddCancelMonoid A] [Finset.HasAntidiagonal A] {p : A × A} {q : A × A} {n : A} (hp : p Finset.antidiagonal n) (hq : q Finset.antidiagonal n) :
    p = q p.1 = q.1

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

    See also Finset.antidiagonal_congr'.

    theorem Finset.antidiagonal_subtype_ext_iff {A : Type u_1} [AddCancelMonoid A] [Finset.HasAntidiagonal A] {n : A} {p : { x : A × A // x Finset.antidiagonal n }} {q : { x : A × A // x Finset.antidiagonal n }} :
    p = q (↑p).1 = (↑q).1
    theorem Finset.antidiagonal_subtype_ext {A : Type u_1} [AddCancelMonoid A] [Finset.HasAntidiagonal A] {n : A} {p : { x : A × A // x Finset.antidiagonal n }} {q : { x : A × A // x Finset.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.

    theorem Finset.antidiagonal_congr' {A : Type u_1} [AddCancelCommMonoid A] [Finset.HasAntidiagonal A] {p : A × A} {q : A × A} {n : A} (hp : p Finset.antidiagonal n) (hq : q Finset.antidiagonal n) :
    p = q p.2 = q.2

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

    See also Finset.antidiagonal_congr.

    theorem Finset.filter_fst_eq_antidiagonal {A : Type u_1} [CanonicallyOrderedAddCommMonoid A] [Sub A] [OrderedSub A] [AddLeftReflectLE A] [Finset.HasAntidiagonal A] (n : A) (m : A) [DecidablePred fun (x : A) => x = m] [Decidable (m n)] :
    Finset.filter (fun (x : A × A) => x.1 = m) (Finset.antidiagonal n) = if m n then {(m, n - m)} else
    theorem Finset.filter_snd_eq_antidiagonal {A : Type u_1} [CanonicallyOrderedAddCommMonoid A] [Sub A] [OrderedSub A] [AddLeftReflectLE A] [Finset.HasAntidiagonal A] (n : A) (m : A) [DecidablePred fun (x : A) => x = m] [Decidable (m n)] :
    Finset.filter (fun (x : A × A) => x.2 = m) (Finset.antidiagonal n) = if m n then {(n - m, m)} else
    @[simp]
    theorem Finset.sigmaAntidiagonalEquivProd_symm_apply_fst {A : Type u_1} [AddMonoid A] [Finset.HasAntidiagonal A] (x : A × A) :
    (Finset.sigmaAntidiagonalEquivProd.symm x).fst = x.1 + x.2
    @[simp]
    theorem Finset.sigmaAntidiagonalEquivProd_symm_apply_snd_coe {A : Type u_1} [AddMonoid A] [Finset.HasAntidiagonal A] (x : A × A) :
    (Finset.sigmaAntidiagonalEquivProd.symm x).snd = x
    @[simp]
    theorem Finset.sigmaAntidiagonalEquivProd_apply {A : Type u_1} [AddMonoid A] [Finset.HasAntidiagonal A] (x : (n : A) × { x : A × A // x Finset.antidiagonal n }) :
    Finset.sigmaAntidiagonalEquivProd x = x.snd
    def Finset.sigmaAntidiagonalEquivProd {A : Type u_1} [AddMonoid A] [Finset.HasAntidiagonal A] :
    (n : A) × { x : A × A // x Finset.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
    • One or more equations did not get rendered due to their size.
    Instances For
      @[reducible, inline]

      In a canonically ordered add 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
      • One or more equations did not get rendered due to their size.
      Instances For