Inserting a new coordinate into a maximal chain

Let σ encode a maximal chain on Fin n, and let J : Fin (n + 1) be an insertion rank. We identify the old ground set with the first n elements of Fin (n + 1) and use Fin.last n for the new element. Before rank J the new chain is the lifted old chain; after rank J it is the lifted old chain with the new element adjoined. These are the two cases of the inserted-chain construction used in the proof of Theorem 2.1.

def Feige.liftChainState {n : ℕ} (S : Finset (Fin n)) : Finset (Fin (n + 1))

Lift a Boolean-lattice state to the enlarged ground set.

Equations

• Feige.liftChainState S = Finset.map Fin.castSuccEmb S

@[simp]

theorem Feige.mem_liftChainState {n : ℕ} (S : Finset (Fin n)) (i : Fin n) : i.castSucc ∈ liftChainState S ↔ i ∈ S

@[simp]

theorem Feige.last_not_mem_liftChainState {n : ℕ} (S : Finset (Fin n)) : Fin.last n ∉ liftChainState S

@[simp]

theorem Feige.card_liftChainState {n : ℕ} (S : Finset (Fin n)) : (liftChainState S).card = S.card

def Feige.insertChainPerm {n : ℕ} (σ : Equiv.Perm (Fin n)) (J : Fin (n + 1)) : Equiv.Perm (Fin (n + 1))

The enlarged permutation obtained by inserting the new element Fin.last n at rank J and retaining the relative order σ on old elements.

Equations

• Feige.insertChainPerm σ J = (finSuccEquiv' J).trans ((Equiv.optionCongr σ).trans (finSuccEquiv' (Fin.last n)).symm)

@[simp]

theorem Feige.insertChainPerm_at {n : ℕ} (σ : Equiv.Perm (Fin n)) (J : Fin (n + 1)) : (insertChainPerm σ J) J = Fin.last n

@[simp]

theorem Feige.insertChainPerm_succAbove {n : ℕ} (σ : Equiv.Perm (Fin n)) (J : Fin (n + 1)) (i : Fin n) : (insertChainPerm σ J) (J.succAbove i) = (σ i).castSucc

@[simp]

theorem Feige.insertChainPerm_symm_last {n : ℕ} (σ : Equiv.Perm (Fin n)) (J : Fin (n + 1)) : (Equiv.symm (insertChainPerm σ J)) (Fin.last n) = J

@[simp]

theorem Feige.insertChainPerm_symm_castSucc {n : ℕ} (σ : Equiv.Perm (Fin n)) (J : Fin (n + 1)) (i : Fin n) : (Equiv.symm (insertChainPerm σ J)) i.castSucc = J.succAbove ((Equiv.symm σ) i)

def Feige.insertedChainState {n : ℕ} (σ : Equiv.Perm (Fin n)) (J : Fin (n + 1)) (j : Fin (n + 2)) : Finset (Fin (n + 1))

The states of the enlarged maximal chain, written directly in the two cases before and after the insertion rank.

Equations

• Feige.insertedChainState σ J j = if h : ↑j ≤ ↑J then Feige.liftChainState (Feige.chainState σ ⟨↑j, ⋯⟩) else insert (Fin.last n) (Feige.liftChainState (Feige.chainState σ ⟨↑j - 1, ⋯⟩))

theorem Feige.insertedChainState_before {n : ℕ} (σ : Equiv.Perm (Fin n)) (J r : Fin (n + 1)) (hr : r ≤ J) : insertedChainState σ J r.castSucc = liftChainState (chainState σ r)

The enlarged chain state before the insertion rank.

theorem Feige.insertedChainState_after {n : ℕ} (σ : Equiv.Perm (Fin n)) (J r : Fin (n + 1)) (hr : J ≤ r) : insertedChainState σ J r.succ = insert (Fin.last n) (liftChainState (chainState σ r))

After the insertion rank, the new state consists of the corresponding old state together with the inserted element.

@[simp]

theorem Feige.insertedChainState_zero {n : ℕ} (σ : Equiv.Perm (Fin n)) (J : Fin (n + 1)) : insertedChainState σ J 0 = ∅

@[simp]

theorem Feige.insertedChainState_last {n : ℕ} (σ : Equiv.Perm (Fin n)) (J : Fin (n + 1)) : insertedChainState σ J (Fin.last (n + 1)) = Finset.univ

@[simp]

theorem Feige.card_insertedChainState {n : ℕ} (σ : Equiv.Perm (Fin n)) (J : Fin (n + 1)) (j : Fin (n + 2)) : (insertedChainState σ J j).card = ↑j

theorem Feige.chainState_insertChainPerm_before {n : ℕ} (σ : Equiv.Perm (Fin n)) (J r : Fin (n + 1)) (hr : r ≤ J) : chainState (insertChainPerm σ J) r.castSucc = liftChainState (chainState σ r)

Before the insertion rank, insertChainPerm produces the lifted old chain state.

theorem Feige.chainState_insertChainPerm_after {n : ℕ} (σ : Equiv.Perm (Fin n)) (J r : Fin (n + 1)) (hr : J ≤ r) : chainState (insertChainPerm σ J) r.succ = insert (Fin.last n) (liftChainState (chainState σ r))

After the insertion rank, insertChainPerm produces the lifted old chain state with the new coordinate adjoined.

theorem Feige.chainState_insertChainPerm_eq_insertedChainState {n : ℕ} (σ : Equiv.Perm (Fin n)) (J : Fin (n + 1)) (j : Fin (n + 2)) : chainState (insertChainPerm σ J) j = insertedChainState σ J j

The direct inserted-state formula agrees at every level with the maximal chain encoded by the inserted permutation.