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

  The set of ordered integer pairs forming this abstract inversion 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

Every inversion pair has its first index strictly below its second.

Equations

• ⋯ = ⋯

@[reducible, inline]

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

Closure of inversion pairs under concatenating two increasing pairs.

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

An inversion spanning an intermediate index contains at least one of the two intervening pairs.

Equations

• ⋯ = ⋯

@[reducible, inline]

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

Each index has finitely many outgoing inversion pairs.

Equations

• ⋯ = ⋯

@[reducible, inline]

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

Each index has finitely many incoming inversion pairs.

Equations

• ⋯ = ⋯

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

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

The integer order obtained by reversing precisely the inversions in the ASP set.

Equations

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

instance AspSet.instIsStrictTotalOrderIntPostLt (asps : AspSet) : IsStrictTotalOrder ℤ asps.postLt

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

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

def AspSet.ofAspPerm (τ : AspPerm) : AspSet

The abstract inversion set carried by an almost sign-preserving permutation.

Equations

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

@[reducible, inline]

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

The finite set of integers whose inversions enter the vertex n.

Equations

• asps.inset n = ⋯.toFinset

@[reducible, inline]

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

The finite set of integers reached by inversions leaving the vertex n.

Equations

• asps.outset n = ⋯.toFinset

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

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) (χ : ℤ) : ℤ → ℤ

The integer permutation reconstructed from the ASP inversion set with prescribed 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 AspSet.invSet_func (asps : AspSet) (χ : ℤ) : invSet (asps.recon χ) = ↑asps

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

theorem AspSet.func_asp (asps : AspSet) (χ : ℤ) : isAsp (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) (χ : ℤ) : invSet (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.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 AspSet.AspPerm_equiv_AspSet_toFun_fst (τ : AspPerm) : ↑(AspPermEquivAspSet τ).1 = invSet τ.func

@[simp]

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

theorem AspSet.inv_set_AspPerm_equiv_AspSet_invFun (asps : AspSet) (χ : ℤ) : invSet (AspPermEquivAspSet.invFun (asps, χ)).func = ↑asps

theorem AspSet.chi_AspPerm_equiv_AspSet_invFun (asps : AspSet) (χ : ℤ) : (AspPermEquivAspSet.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), invSet τ.func = I ∧ τ.χ = χ) ↔ AspSet_prop I