Finite Demazure factorizations

Finite ASP permutations admit Demazure factorizations at every prescribed inversion-length cut. This supplies the combinatorial input needed for unconditional opposite-side vertex-wedge transmission gluing.

noncomputable def AspPerm.simpleReflection (i : ℤ) : AspPerm

The adjacent reflection interchanging positions i and i + 1.

Equations

• AspPerm.simpleReflection i = Transpositions.sigma {i} ⋯

@[simp]

theorem AspPerm.simpleReflection_chi (i : ℤ) : (simpleReflection i).χ = 0

@[simp]

theorem AspPerm.simpleReflection_apply (i n : ℤ) : (simpleReflection i).func n = if n = i then i + 1 else if n = i + 1 then i else n

theorem AspPerm.simpleReflection_involutive (i n : ℤ) : (simpleReflection i).func ((simpleReflection i).func n) = n

@[simp]

theorem AspPerm.simpleReflection_inv_set (i : ℤ) : invSet (simpleReflection i).func = {(i, i + 1)}

noncomputable def AspPerm.swapPair (i : ℤ) (p : ℤ × ℤ) : ℤ × ℤ

Apply the adjacent reflection to both coordinates of an inversion pair.

Equations

• AspPerm.swapPair i p = ((AspPerm.simpleReflection i).func p.1, (AspPerm.simpleReflection i).func p.2)

noncomputable def AspPerm.invSetEraseSimpleEquiv (τ : AspPerm) (i : ℤ) : { p : ℤ × ℤ // p ∈ invSet (τ.mul (simpleReflection i)).func \ {(i, i + 1)} } ≃ { p : ℤ × ℤ // p ∈ invSet τ.func \ {(i, i + 1)} }

The nonexceptional inversions before and after right multiplication by an adjacent reflection are in canonical bijection.

Equations

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

theorem AspPerm.finite_invSet_mul_simple_iff (τ : AspPerm) (i : ℤ) : (invSet (τ.mul (simpleReflection i)).func).Finite ↔ (invSet τ.func).Finite

Right multiplication by an adjacent reflection preserves finiteness of the inversion set.

noncomputable def AspPerm.invLength (τ : AspPerm) : ℕ

Finite inversion length.

Equations

• τ.invLength = (invSet τ.func).ncard

theorem AspPerm.invLength_mul_simple_of_ascent (τ : AspPerm) (i : ℤ) (hfin : (invSet τ.func).Finite) (hasc : τ.func i < τ.func (i + 1)) : (τ.mul (simpleReflection i)).invLength = τ.invLength + 1

Right multiplication by an adjacent reflection adds one inversion at an ascent.

theorem AspPerm.invLength_mul_simple_add_one_of_descent (τ : AspPerm) (i : ℤ) (hfin : (invSet τ.func).Finite) (hdesc : τ.func (i + 1) < τ.func i) : (τ.mul (simpleReflection i)).invLength + 1 = τ.invLength

Right multiplication by an adjacent reflection removes one inversion at a descent, stated additively to avoid truncated subtraction.

theorem AspPerm.exists_adjacent_descent_of_mem_invSet (τ : AspPerm) {a b : ℤ} (hab : (a, b) ∈ invSet τ.func) : ∃ (i : ℤ), a ≤ i ∧ i < b ∧ τ.func (i + 1) < τ.func i

Every inversion contains an adjacent descent.

theorem AspPerm.exists_adjacent_descent_of_invLength_pos (τ : AspPerm) (hfin : (invSet τ.func).Finite) (hpos : 0 < τ.invLength) : ∃ (i : ℤ), τ.func (i + 1) < τ.func i

Positive finite inversion length gives an adjacent descent.

theorem AspPerm.exists_right_simple_factor_of_invLength_pos (τ : AspPerm) (hfin : (invSet τ.func).Finite) (hpos : 0 < τ.invLength) : ∃ (τ' : AspPerm) (i : ℤ), τ = τ' ⋆ simpleReflection i ∧ (invSet τ'.func).Finite ∧ τ'.invLength + 1 = τ.invLength

A positive-length finite ASP permutation is a shorter permutation Demazure-multiplied on the right by one adjacent reflection.

theorem AspPerm.exists_star_factorization_right_length (τ : AspPerm) (hfin : (invSet τ.func).Finite) (k : ℕ) (hk : k ≤ τ.invLength) : ∃ (α : AspPerm) (β : AspPerm), τ = α ⋆ β ∧ (invSet α.func).Finite ∧ (invSet β.func).Finite ∧ α.invLength = τ.invLength - k ∧ β.invLength = k ∧ β.χ = 0

Peel exactly k inversions into a zero-shift right factor.

theorem AspPerm.exists_star_factorization_invLength (τ : AspPerm) (hfin : (invSet τ.func).Finite) (m : ℕ) : ∃ (α : AspPerm) (β : AspPerm), τ = α ⋆ β ∧ (invSet α.func).Finite ∧ (invSet β.func).Finite ∧ α.invLength = min m τ.invLength ∧ β.invLength = τ.invLength - min m τ.invLength ∧ β.χ = 0

Split a finite ASP permutation at every prescribed inversion-length cut.

theorem Utilities.hasBoundedDemazureFactorizations_of_nonneg (gG gH : ℤ) (hG : 0 ≤ gG) (hH : 0 ≤ gH) : HasBoundedDemazureFactorizations gG gH

Every pair of nonnegative budgets has the required bounded finite Demazure-factorization property.

theorem Utilities.transmissionExistence_vertexWedge_opposite (G : CFGraph) (H : CFGraph) (x : G.V) (y : H.V) (u : G.V) (v : H.V) (hTG : TransmissionExistence G u x) (hTH : TransmissionExistence H y v) (hGenusG : 0 ≤ G.genus) (hGenusH : 0 ≤ H.genus) : TransmissionExistence (vertexWedge G H x y) (Sum.inl u) (wedgeRightVertex G H x y v)

Opposite-side transmission existence is closed under vertex wedges.