Module docstring

{"# 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.

```lean 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. "}

Finset.HasAntidiagonal structure

(A : Type*) [AddMonoid A]

Full source

/-- The class of additive monoids with an antidiagonal -/
class HasAntidiagonal (A : Type*) [AddMonoid A] where
  /-- The antidiagonal of an element `n` is the finset of pairs `(i, j)` such that `i + j = n`. -/
  antidiagonal : A → Finset (A × A)
  /-- A pair belongs to `antidiagonal n` iff the sum of its components is equal to `n`. -/
  mem_antidiagonal {n} {a} : a ∈ antidiagonal na ∈ antidiagonal n ↔ a.fst + a.snd = n

Antidiagonal of an Additive Monoid

Informal description

The structure `Finset.HasAntidiagonal A` represents an additive monoid `A` equipped with an antidiagonal function that, for any element `n ∈ A`, returns the finite set of all pairs `(a, b) ∈ A × A` such that `a + b = n`.

Finset.instSubsingletonHasAntidiagonal instance

[AddMonoid A] : Subsingleton (HasAntidiagonal A)

Full source

/-- All `HasAntidiagonal` instances are equal -/
instance [AddMonoid A] : Subsingleton (HasAntidiagonal A) where
  allEq := by
    rintro ⟨a, ha⟩ ⟨b, hb⟩
    congr with n xy
    rw [ha, hb]

Uniqueness of Antidiagonal Structures on Additive Monoids

Informal description

For any additive monoid $A$, the type of antidiagonal structures on $A$ is a subsingleton, meaning all such structures are equal.

Finset.hasAntidiagonal_congr theorem

(A : Type*) [AddMonoid A] [H1 : HasAntidiagonal A] [H2 : HasAntidiagonal A] : H1.antidiagonal = H2.antidiagonal

Full source

lemma hasAntidiagonal_congr (A : Type*) [AddMonoid A]
    [H1 : HasAntidiagonal A] [H2 : HasAntidiagonal A] :
    H1.antidiagonal = H2.antidiagonal := by congr!; subsingleton

Uniqueness of Antidiagonal Functions on Additive Monoids

Informal description

For any additive monoid $A$ with two antidiagonal structures $H_1$ and $H_2$, the antidiagonal functions associated with $H_1$ and $H_2$ are equal. That is, for any $n \in A$, the sets of pairs $(a, b) \in A \times A$ such that $a + b = n$ under $H_1$ and $H_2$ coincide.

Finset.swap_mem_antidiagonal theorem

[AddCommMonoid A] [HasAntidiagonal A] {n : A} {xy : A × A} : xy.swap ∈ antidiagonal n ↔ xy ∈ antidiagonal n

Full source

theorem swap_mem_antidiagonal [AddCommMonoid A] [HasAntidiagonal A] {n : A} {xy : A × A} :
    xy.swap ∈ antidiagonal nxy.swap ∈ antidiagonal n ↔ xy ∈ antidiagonal n := by
  simp [add_comm]

Swapped Pair Membership in Antidiagonal iff Original Pair Belongs

Informal description

Let $A$ be an additive commutative monoid equipped with an antidiagonal function. For any element $n \in A$ and any pair $(x, y) \in A \times A$, the swapped pair $(y, x)$ belongs to the antidiagonal of $n$ if and only if $(x, y)$ belongs to the antidiagonal of $n$. In other words, $(y, x) \in \text{antidiagonal}(n) \leftrightarrow (x, y) \in \text{antidiagonal}(n)$.

Finset.map_prodComm_antidiagonal theorem

[AddCommMonoid A] [HasAntidiagonal A] {n : A} : (antidiagonal n).map (Equiv.prodComm A A) = antidiagonal n

Full source

@[simp] theorem map_prodComm_antidiagonal [AddCommMonoid A] [HasAntidiagonal A] {n : A} :
    (antidiagonal n).map (Equiv.prodComm A A) = antidiagonal n :=
  Finset.ext fun ⟨a, b⟩ => by simp [add_comm]

Antidiagonal Invariance under Pair Swapping

Informal description

Let $A$ be an additive commutative monoid equipped with an antidiagonal function. For any element $n \in A$, the image of the antidiagonal set $\text{antidiagonal}(n)$ under the product commutativity equivalence $\text{Equiv.prodComm} : A \times A \simeq A \times A$ is equal to $\text{antidiagonal}(n)$ itself. In other words, mapping each pair $(x, y)$ in $\text{antidiagonal}(n)$ to $(y, x)$ preserves the antidiagonal set.

Finset.map_swap_antidiagonal theorem

 [AddCommMonoid A] [HasAntidiagonal A] {n : A} : (antidiagonal n).map ⟨Prod.swap, Prod.swap_injective⟩ = antidiagonal n

Full source

/-- See also `Finset.map_prodComm_antidiagonal`. -/
@[simp] theorem map_swap_antidiagonal [AddCommMonoid A] [HasAntidiagonal A] {n : A} :
    (antidiagonal n).map ⟨Prod.swap, Prod.swap_injective⟩ = antidiagonal n :=
  map_prodComm_antidiagonal

Antidiagonal Invariance under Pair Swapping via Swap Function

Informal description

Let $A$ be an additive commutative monoid equipped with an antidiagonal function. For any element $n \in A$, the image of the antidiagonal set $\text{antidiagonal}(n)$ under the pair swap function $\langle \text{swap}, \text{swap\_injective} \rangle$ is equal to $\text{antidiagonal}(n)$. That is, mapping each pair $(x, y) \in \text{antidiagonal}(n)$ to $(y, x)$ preserves the antidiagonal set.

Finset.antidiagonal_congr theorem

(hp : p ∈ antidiagonal n) (hq : q ∈ antidiagonal n) : p = q ↔ p.1 = q.1

Full source

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

See also `Finset.antidiagonal_congr'`. -/
theorem antidiagonal_congr (hp : p ∈ antidiagonal n) (hq : q ∈ antidiagonal n) :
    p = q ↔ p.1 = q.1 := by
  refine ⟨congr_arg Prod.fst, fun h ↦ Prod.ext h ((add_right_inj q.fst).mp ?_)⟩
  rw [mem_antidiagonal] at hp hq
  rw [hq, ← h, hp]

First Component Determines Antidiagonal Pair

Informal description

Let $A$ be an additive monoid with an antidiagonal function, and let $n \in A$. For any two pairs $p, q$ in the antidiagonal set of $n$ (i.e., $p, q \in \text{antidiagonal}(n)$ with $p_1 + p_2 = n$ and $q_1 + q_2 = n$), the pairs are equal if and only if their first components are equal, i.e., $p = q \Leftrightarrow p_1 = q_1$.

Finset.antidiagonal_subtype_ext theorem

{p q : antidiagonal n} (h : p.val.1 = q.val.1) : p = q

Full source

/-- 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. -/
@[ext] theorem antidiagonal_subtype_ext {p q : antidiagonal n} (h : p.val.1 = q.val.1) : p = q :=
  Subtype.ext ((antidiagonal_congr p.prop q.prop).mpr h)

Equality in Antidiagonal Subtype Determined by First Component

Informal description

For any two elements $p$ and $q$ in the antidiagonal of $n$ (i.e., pairs $(a,b)$ such that $a + b = n$), if their first components are equal ($p.1 = q.1$), then $p = q$.

Finset.antidiagonal_congr' theorem

(hp : p ∈ antidiagonal n) (hq : q ∈ antidiagonal n) : p = q ↔ p.2 = q.2

Full source

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

See also `Finset.antidiagonal_congr`. -/
lemma antidiagonal_congr' (hp : p ∈ antidiagonal n) (hq : q ∈ antidiagonal n) :
    p = q ↔ p.2 = q.2 := by
  rw [← Prod.swap_inj]
  exact antidiagonal_congr (swap_mem_antidiagonal.2 hp) (swap_mem_antidiagonal.2 hq)

Second Component Determines Antidiagonal Pair

Informal description

Let $A$ be an additive monoid equipped with an antidiagonal function, and let $n \in A$. For any two pairs $p, q$ in the antidiagonal set of $n$ (i.e., $p, q \in \text{antidiagonal}(n)$ with $p_1 + p_2 = n$ and $q_1 + q_2 = n$), the pairs are equal if and only if their second components are equal, i.e., $p = q \Leftrightarrow p_2 = q_2$.

Finset.antidiagonal_zero theorem

: antidiagonal (0 : A) = {(0, 0)}

Full source

@[simp]
theorem antidiagonal_zero : antidiagonal (0 : A) = {(0, 0)} := by
  ext ⟨x, y⟩
  simp

Antidiagonal of Zero is Singleton Zero Pair

Informal description

For an additive monoid $A$ equipped with an antidiagonal function, the antidiagonal of the zero element $0 \in A$ is the singleton set $\{(0, 0)\}$.

Finset.antidiagonal.fst_le theorem

{n : A} {kl : A × A} (hlk : kl ∈ antidiagonal n) : kl.1 ≤ n

Full source

theorem antidiagonal.fst_le {n : A} {kl : A × A} (hlk : kl ∈ antidiagonal n) : kl.1 ≤ n := by
  rw [le_iff_exists_add]
  use kl.2
  rwa [mem_antidiagonal, eq_comm] at hlk

First Component of Antidiagonal Pair is Bounded by Sum

Informal description

For any element $n$ in an additive monoid $A$ equipped with an antidiagonal function, and for any pair $(k, l)$ in the antidiagonal of $n$ (i.e., $k + l = n$), the first component $k$ satisfies $k \leq n$.

Finset.antidiagonal.snd_le theorem

{n : A} {kl : A × A} (hlk : kl ∈ antidiagonal n) : kl.2 ≤ n

Full source

theorem antidiagonal.snd_le {n : A} {kl : A × A} (hlk : kl ∈ antidiagonal n) : kl.2 ≤ n := by
  rw [le_iff_exists_add]
  use kl.1
  rwa [mem_antidiagonal, eq_comm, add_comm] at hlk

Second Component of Antidiagonal Pair is Bounded by Sum

Informal description

For any element $n$ in an additive monoid $A$ equipped with an antidiagonal function, and for any pair $(k, l)$ in the antidiagonal of $n$ (i.e., $k + l = n$), the second component $l$ satisfies $l \leq n$.

Finset.filter_fst_eq_antidiagonal theorem

 (n m : A) [DecidablePred (· = m)] [Decidable (m ≤ n)] :
  {x ∈ antidiagonal n | x.fst = m} = if m ≤ n then {(m, n - m)} else ∅

Full source

theorem filter_fst_eq_antidiagonal (n m : A) [DecidablePred (· = m)] [Decidable (m ≤ n)] :
    {x ∈ antidiagonal n | x.fst = m} = if m ≤ n then {(m, n - m)} else ∅ := by
  ext ⟨a, b⟩
  suffices a = m → (a + b = n ↔ m ≤ n ∧ b = n - m) by
    rw [mem_filter, mem_antidiagonal, apply_ite (fun n ↦ (a, b)(a, b) ∈ n), mem_singleton,
      Prod.mk_inj, ite_prop_iff_or]
    simpa [← and_assoc, @and_right_comm _ (a = _), and_congr_left_iff]
  rintro rfl
  constructor
  · rintro rfl
    exact ⟨le_add_right le_rfl, (add_tsub_cancel_left _ _).symm⟩
  · rintro ⟨h, rfl⟩
    exact add_tsub_cancel_of_le h

Filtered Antidiagonal by First Component: $\{(x,y) \in \text{antidiagonal}(n) \mid x = m\} = \text{if } m \leq n \text{ then } \{(m, n-m)\} \text{ else } \emptyset$

Informal description

For any elements $n$ and $m$ in an additive monoid $A$ with an antidiagonal function, the subset of pairs $(x,y)$ in the antidiagonal of $n$ (i.e., $x + y = n$) where the first component equals $m$ is: - the singleton set $\{(m, n - m)\}$ if $m \leq n$, - the empty set otherwise.

Finset.filter_snd_eq_antidiagonal theorem

 (n m : A) [DecidablePred (· = m)] [Decidable (m ≤ n)] :
  {x ∈ antidiagonal n | x.snd = m} = if m ≤ n then {(n - m, m)} else ∅

Full source

theorem filter_snd_eq_antidiagonal (n m : A) [DecidablePred (· = m)] [Decidable (m ≤ n)] :
    {x ∈ antidiagonal n | x.snd = m} = if m ≤ n then {(n - m, m)} else ∅ := by
  have : (fun x : A × A ↦ (x.snd = m)) ∘ Prod.swap = fun x : A × A ↦ x.fst = m := by
    ext; simp
  rw [← map_swap_antidiagonal, filter_map]
  simp [this, filter_fst_eq_antidiagonal, apply_ite (Finset.map _)]

Filtered Antidiagonal by Second Component: $\{(x,y) \in \text{antidiagonal}(n) \mid y = m\} = \text{if } m \leq n \text{ then } \{(n-m, m)\} \text{ else } \emptyset$

Informal description

For any elements $n$ and $m$ in an additive monoid $A$ with an antidiagonal function, the subset of pairs $(x,y)$ in the antidiagonal of $n$ (i.e., $x + y = n$) where the second component equals $m$ is: - the singleton set $\{(n - m, m)\}$ if $m \leq n$, - the empty set otherwise.

Finset.sigmaAntidiagonalEquivProd definition

[AddMonoid A] [HasAntidiagonal A] : (Σ n : A, antidiagonal n) ≃ A × A

Full source

/-- 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)`. -/
@[simps]
def sigmaAntidiagonalEquivProd [AddMonoid A] [HasAntidiagonal A] :
    (Σ n : A, antidiagonal n) ≃ A × A where
  toFun x := x.2
  invFun x := ⟨x.1 + x.2, x, mem_antidiagonal.mpr rfl⟩
  left_inv := by
    rintro ⟨n, ⟨k, l⟩, h⟩
    rw [mem_antidiagonal] at h
    exact Sigma.subtype_ext h rfl
  right_inv _ := rfl

Equivalence between antidiagonal union and product

Informal description

The equivalence between the disjoint union of antidiagonals $\Sigma (n : A), \text{antidiagonal}(n)$ and the product $A \times A$, where $\text{antidiagonal}(n)$ is the finite set of all pairs $(k, l) \in A \times A$ such that $k + l = n$. The equivalence maps $(n, (k, l))$ to $(k, l)$ and has an inverse that maps $(k, l)$ to $(k + l, (k, l))$.

Finset.antidiagonalOfLocallyFinite abbrev

: HasAntidiagonal A

Full source

/-- 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. -/
abbrev antidiagonalOfLocallyFinite : HasAntidiagonal A where
  antidiagonal n := {uv ∈ Iic n ×ˢ Iic n | uv.fst + uv.snd = n}
  mem_antidiagonal {n} {a} := by
    simp only [mem_filter, and_iff_right_iff_imp]
    intro h
    simp [← h]

Construction of Antidiagonal in Canonically Ordered Additive Monoids with Locally Finite Order

Informal description

In a canonically ordered additive monoid $A$ with a locally finite order, the antidiagonal can be constructed by filtering pairs $(a, b) \in A \times A$ such that $a + b = n$ for any given $n \in A$.