Inversion sets

This file gives a characterization of the inversion set of ASP permutations. It corresponds to Theorem 2.13 of An extended Demazure product.

structure LeanPool.DemazureProduct.AspSet_prop (I : Set (ℤ × ℤ)) : Prop

The axioms characterizing inversion sets of ASP permutations: directedness, closure, coclosure, and finite in/out degree. Definition 2.12 (defn:aspSet) of An extended Demazure product.

• directed (u v : ℤ) : (u, v) ∈ I → u < v
• closed (u v w : ℤ) : (u, v) ∈ I → (v, w) ∈ I → (u, w) ∈ I
• coclosed (u v w : ℤ) : u < v → v < w → (u, v) ∉ I → (v, w) ∉ I → (u, w) ∉ I
• finiteOutdegree (u : ℤ) : {v : ℤ | (u, v) ∈ I}.Finite
• finiteIndegree (v : ℤ) : {u : ℤ | (u, v) ∈ I}.Finite

structure LeanPool.DemazureProduct.AspSet : Type

An abstract ASP inversion set: a set of boxes equipped with the axioms of AspSet_prop.

• I : Set (ℤ × ℤ)

  The underlying set of inversion boxes.

• prop : AspSet_prop self.I

  The axioms satisfied by the underlying inversion-box set.

@[implicit_reducible]

instance LeanPool.DemazureProduct.instSetLikeAspSetProdInt : SetLike AspSet (ℤ × ℤ)

Equations

• LeanPool.DemazureProduct.instSetLikeAspSetProdInt = { coe := LeanPool.DemazureProduct.AspSet.I, coe_injective := LeanPool.DemazureProduct.instSetLikeAspSetProdInt._proof_1 }

@[simp]

theorem LeanPool.DemazureProduct.mem_AspSet (asps : AspSet) (u v : ℤ) : (u, v) ∈ asps ↔ (u, v) ∈ asps.I

theorem LeanPool.DemazureProduct.AspSet.ext {A B : AspSet} (hI : A.I = B.I) : A = B

Two AspSets are equal if their underlying sets of boxes are equal.

theorem LeanPool.DemazureProduct.AspSet.directed (asps : AspSet) (u v : ℤ) : (u, v) ∈ asps → u < v

Every inversion box of an abstract ASP set is directed upward.

theorem LeanPool.DemazureProduct.AspSet.closed (asps : AspSet) (u v w : ℤ) : (u, v) ∈ asps → (v, w) ∈ asps → (u, w) ∈ asps

Abstract ASP inversion sets are transitively closed.

theorem LeanPool.DemazureProduct.AspSet.coclosed (asps : AspSet) (u v w : ℤ) : u < v → v < w → (u, v) ∉ asps → (v, w) ∉ asps → (u, w) ∉ asps

Abstract ASP inversion sets are transitively coclosed.

theorem LeanPool.DemazureProduct.AspSet.finiteOutdegree (asps : AspSet) (u : ℤ) : {v : ℤ | (u, v) ∈ asps}.Finite

Each row of an abstract ASP inversion set is finite.

theorem LeanPool.DemazureProduct.AspSet.finiteIndegree (asps : AspSet) (v : ℤ) : {u : ℤ | (u, v) ∈ asps}.Finite

Each column of an abstract ASP inversion set is finite.

instance LeanPool.DemazureProduct.AspSet.instIsStrictTotalOrderIntPost_lt (asps : AspSet) : IsStrictTotalOrder ℤ (LeanPool.DemazureProduct.AspSet.post_lt✝ asps)

theorem LeanPool.DemazureProduct.AspSet.AspSet_InvSet_of_AspPerm (τ : AspPerm) : AspSet_prop (invSet τ.func)

The inversion set of an ASP permutation forms an ASP set.

def LeanPool.DemazureProduct.AspSet.ofAspPerm (τ : AspPerm) : AspSet

The abstract inversion set associated to an ASP permutation.

Equations

• LeanPool.DemazureProduct.AspSet.ofAspPerm τ = { I := LeanPool.DemazureProduct.invSet τ.func, prop := ⋯ }

@[reducible, inline]

noncomputable abbrev LeanPool.DemazureProduct.AspSet.inset (asps : AspSet) (n : ℤ) : Finset ℤ

The finite set of inversion sources ending at n.

Equations

• asps.inset n = ⋯.toFinset

@[reducible, inline]

noncomputable abbrev LeanPool.DemazureProduct.AspSet.outset (asps : AspSet) (n : ℤ) : Finset ℤ

The finite set of inversion targets starting at n.

Equations

• asps.outset n = ⋯.toFinset

theorem LeanPool.DemazureProduct.AspSet.mem_inset (asps : AspSet) (n x : ℤ) : x ∈ asps.inset n ↔ (x, n) ∈ asps

theorem LeanPool.DemazureProduct.AspSet.mem_outset (asps : AspSet) (n x : ℤ) : x ∈ asps.outset n ↔ (n, x) ∈ asps

noncomputable def LeanPool.DemazureProduct.AspSet.recon (asps : AspSet) (χ : ℤ) : ℤ → ℤ

Reconstruct a function ℤ → ℤ from an abstract ASP inversion set and a shift parameter χ.

Equations

• asps.recon χ n = n + ↑(asps.outset n).card - ↑(asps.inset n).card - χ

@[reducible, inline]

noncomputable abbrev LeanPool.DemazureProduct.AspSet.σ (asps : AspSet) (χ : ℤ) : ℤ → ℤ

The reconstructed function with the fixed shift χ.

Equations

• asps.σ χ = asps.recon χ

Reconstructing ASP permutations from ASP sets

Starting from an abstract ASP set asps and a shift χ, this section proves that the reconstructed function is bijective, ASP, and has the expected inversion data, yielding an AspPerm.

theorem LeanPool.DemazureProduct.AspSet.invSet_func (asps : AspSet) (χ : ℤ) : invSet (asps.recon χ) = ↑asps

The reconstructed function from an inversion set has that inversion set.

theorem LeanPool.DemazureProduct.AspSet.func_asp (asps : AspSet) (χ : ℤ) : isAsp (asps.recon χ)

The function reconstructed from an ASP set is an ASP permutation.

noncomputable def LeanPool.DemazureProduct.AspSet.toAspPerm (asps : AspSet) (χ : ℤ) : AspPerm

Package the function reconstructed from an ASP set and a shift as an AspPerm.

Equations

• asps.toAspPerm χ = { func := asps.recon χ, bijective := ⋯, asp := ⋯ }

theorem LeanPool.DemazureProduct.AspSet.invSet_of_toAspPerm (asps : AspSet) (χ : ℤ) : invSet (asps.toAspPerm χ).func = ↑asps

theorem LeanPool.DemazureProduct.AspSet.inset_of_toAspPerm (asps : AspSet) (χ n : ℤ) : (asps.toAspPerm χ).inset n = ↑(asps.inset n)

theorem LeanPool.DemazureProduct.AspSet.outset_of_toAspPerm (asps : AspSet) (χ n : ℤ) : (asps.toAspPerm χ).outset n = ↑(asps.outset n)

theorem LeanPool.DemazureProduct.AspSet.chi_of_toAspPerm (asps : AspSet) (χ : ℤ) : (asps.toAspPerm χ).χ = χ

noncomputable def LeanPool.DemazureProduct.AspSet.aspPermEquivAspSet : AspPerm ≃ AspSet × ℤ

ASP permutations are equivalent to abstract ASP inversion sets together with a shift parameter. Theorem 2.13 (thm:aspSetReconstruction) of An extended Demazure product.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem LeanPool.DemazureProduct.AspSet.AspPerm_equiv_AspSet_toFun_fst (τ : AspPerm) : ↑(aspPermEquivAspSet τ).1 = invSet τ.func

@[simp]

theorem LeanPool.DemazureProduct.AspSet.AspPerm_equiv_AspSet_toFun_snd (τ : AspPerm) : (aspPermEquivAspSet τ).2 = τ.χ

@[simp]

theorem LeanPool.DemazureProduct.AspSet.inv_set_AspPerm_equiv_AspSet_invFun (asps : AspSet) (χ : ℤ) : invSet (aspPermEquivAspSet.symm (asps, χ)).func = ↑asps

@[simp]

theorem LeanPool.DemazureProduct.AspSet.chi_AspPerm_equiv_AspSet_invFun (asps : AspSet) (χ : ℤ) : (aspPermEquivAspSet.symm (asps, χ)).χ = χ

A set $I \subseteq \mathbb{Z} \times \mathbb{Z}$ is the inversion set of an ASP permutation with shift parameter $\chi$ if and only if it satisfies the ASP set properties. Theorem 2.13 (thm:aspSetReconstruction) from An extended Demazure product.

theorem LeanPool.DemazureProduct.AspSet.invSets_of_AspPerms (I : Set (ℤ × ℤ)) (χ : ℤ) : (∃ (τ : AspPerm), invSet τ.func = I ∧ τ.χ = χ) ↔ AspSet_prop I