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 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
• finite_outdegree (u : ℤ) : {v : ℤ | (u, v) ∈ I}.Finite
• finite_indegree (v : ℤ) : {u : ℤ | (u, v) ∈ I}.Finite

structure AspSet : Type

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

• I : Set (ℤ × ℤ)
• prop : AspSet_prop self.I

@[instance_reducible]

instance instSetLikeAspSetProdInt : SetLike AspSet (ℤ × ℤ)

Equations

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

@[simp]

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

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

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

@[reducible, inline]

abbrev AspSet.directed (asps : AspSet) (u v : ℤ) : (u, v) ∈ asps.I → u < v

Equations

• ⋯ = ⋯

@[reducible, inline]

abbrev AspSet.closed (asps : AspSet) (u v w : ℤ) : (u, v) ∈ asps.I → (v, w) ∈ asps.I → (u, w) ∈ asps.I

Equations

• ⋯ = ⋯

@[reducible, inline]

abbrev AspSet.coclosed (asps : AspSet) (u v w : ℤ) : u < v → v < w → (u, v) ∉ asps.I → (v, w) ∉ asps.I → (u, w) ∉ asps.I

Equations

• ⋯ = ⋯

@[reducible, inline]

abbrev AspSet.finite_outdegree (asps : AspSet) (u : ℤ) : {v : ℤ | (u, v) ∈ asps.I}.Finite

Equations

• ⋯ = ⋯

@[reducible, inline]

abbrev AspSet.finite_indegree (asps : AspSet) (v : ℤ) : {u : ℤ | (u, v) ∈ asps.I}.Finite

Equations

• ⋯ = ⋯

def AspSet.post_lt (asps : AspSet) (m n : ℤ) : Prop

The order on indices after the inversions in asps are applied.

Equations

• asps.post_lt m n = (m < n ∧ (m, n) ∉ asps ∨ n < m ∧ (n, m) ∈ asps)

instance AspSet.instIsStrictTotalOrderIntPost_lt (asps : AspSet) : IsStrictTotalOrder ℤ asps.post_lt

theorem AspSet.AspSet_InvSet_of_AspPerm (τ : AspPerm) : AspSet_prop (inv_set τ.func)

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

def AspSet.of_AspPerm (τ : AspPerm) : AspSet

Equations

• AspSet.of_AspPerm τ = { I := inv_set τ.func, prop := ⋯ }

@[reducible, inline]

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

Equations

• asps.inset n = ⋯.toFinset

@[reducible, inline]

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

Equations

• asps.outset n = ⋯.toFinset

@[simp]

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

@[simp]

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

noncomputable def 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 AspSet.σ (asps : AspSet) (χ : ℤ) : ℤ → ℤ

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 AspSet.invSet_func (asps : AspSet) (χ : ℤ) : inv_set (asps.recon χ) = ↑asps

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

theorem AspSet.func_asp (asps : AspSet) (χ : ℤ) : is_asp (asps.recon χ)

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

noncomputable def 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 AspSet.invSet_of_toAspPerm (asps : AspSet) (χ : ℤ) : inv_set (asps.toAspPerm χ).func = ↑asps

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

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

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

noncomputable def AspSet.AspPerm_equiv_AspSet : 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 AspSet.AspPerm_equiv_AspSet_toFun_fst (τ : AspPerm) : ↑(AspPerm_equiv_AspSet τ).1 = inv_set τ.func

@[simp]

theorem AspSet.AspPerm_equiv_AspSet_toFun_snd (τ : AspPerm) : (AspPerm_equiv_AspSet τ).2 = τ.χ

@[simp]

theorem AspSet.inv_set_AspPerm_equiv_AspSet_invFun (asps : AspSet) (χ : ℤ) : inv_set (AspPerm_equiv_AspSet.invFun (asps, χ)).func = ↑asps

@[simp]

theorem AspSet.chi_AspPerm_equiv_AspSet_invFun (asps : AspSet) (χ : ℤ) : (AspPerm_equiv_AspSet.invFun (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 AspSet.invSets_of_AspPerms (I : Set (ℤ × ℤ)) (χ : ℤ) : (∃ (τ : AspPerm), inv_set τ.func = I ∧ τ.χ = χ) ↔ AspSet_prop I