Top Fox--Neuwirth cells

Top dual cells are exactly one-block barred permutations. Consequently their finite type is canonically equivalent to the full permutation group. The prime symmetry action is the restriction of relabelling on this permutation torsor.

def NRR.BarredPermutation.TopCell (p : ℕ) : Type

Top-dimensional dual Fox--Neuwirth symbols.

Equations

• NRR.BarredPermutation.TopCell p = { c : NRR.BarredPermutation p // c.IsTop }

def NRR.BarredPermutation.TopCell.ofPerm {p : ℕ} (σ : Equiv.Perm (Fin p)) : TopCell p

A permutation determines the unique top symbol with that vertical order.

Equations

• NRR.BarredPermutation.TopCell.ofPerm σ = ⟨{ rank := σ, bars := ∅ }, ⋯⟩

@[simp]

theorem NRR.BarredPermutation.TopCell.ofPerm_rank {p : ℕ} (σ : Equiv.Perm (Fin p)) : (↑(ofPerm σ)).rank = σ

@[simp]

theorem NRR.BarredPermutation.TopCell.ofPerm_bars {p : ℕ} (σ : Equiv.Perm (Fin p)) : (↑(ofPerm σ)).bars = ∅

def NRR.BarredPermutation.TopCell.equivPerm {p : ℕ} : TopCell p ≃ Equiv.Perm (Fin p)

Top symbols are canonically the permutation torsor.

Equations

• NRR.BarredPermutation.TopCell.equivPerm = { toFun := fun (c : NRR.BarredPermutation.TopCell p) => (↑c).rank, invFun := NRR.BarredPermutation.TopCell.ofPerm, left_inv := ⋯, right_inv := ⋯ }

@[instance_reducible]

noncomputable instance NRR.BarredPermutation.TopCell.instFintype {p : ℕ} : Fintype (TopCell p)

Equations

• NRR.BarredPermutation.TopCell.instFintype = Fintype.ofEquiv (Equiv.Perm (Fin p)) NRR.BarredPermutation.TopCell.equivPerm.symm

@[instance_reducible]

noncomputable instance NRR.BarredPermutation.TopCell.instDecidableEq {p : ℕ} : DecidableEq (TopCell p)

Equations

• NRR.BarredPermutation.TopCell.instDecidableEq = Classical.decEq (NRR.BarredPermutation.TopCell p)

@[instance_reducible]

instance NRR.BarredPermutation.TopCell.instCoe {p : ℕ} : Coe (TopCell p) (BarredPermutation p)

A top cell is in particular a barred permutation.

Equations

• NRR.BarredPermutation.TopCell.instCoe = { coe := Subtype.val }

@[instance_reducible]

instance NRR.BarredPermutation.TopCell.primeSymmetryAction (p : ℕ) : MulAction (↥(PrimeSymmetry p)) (TopCell p)

Prime symmetry preserves top cells.

Equations

• NRR.BarredPermutation.TopCell.primeSymmetryAction p = { smul := fun (g : ↥(NRR.PrimeSymmetry p)) (c : NRR.BarredPermutation.TopCell p) => ⟨g • ↑c, ⋯⟩, mul_smul := ⋯, one_smul := ⋯ }

@[simp]

theorem NRR.BarredPermutation.TopCell.smul_coe (p : ℕ) (g : ↥(PrimeSymmetry p)) (c : TopCell p) : ↑(g • c) = g • ↑c

def NRR.BarredPermutation.TopCell.evenRepresentative {p : ℕ} : TopCell p

Distinguished even top-cell representative.

Equations

• NRR.BarredPermutation.TopCell.evenRepresentative = NRR.BarredPermutation.TopCell.ofPerm 1

def NRR.BarredPermutation.TopCell.transpositionRepresentative {p : ℕ} (i j : Fin p) : TopCell p

Distinguished transposition representative used for the second odd-prime orbit.

Equations

• NRR.BarredPermutation.TopCell.transpositionRepresentative i j = NRR.BarredPermutation.TopCell.ofPerm (Equiv.swap i j)

theorem NRR.BarredPermutation.TopCell.dimension {p : ℕ} (hp : Nat.Prime p) (c : TopCell p) : (↑c).dualDimension = p - 1