Orientations for Fox--Neuwirth cells

This file chooses a concrete orientation for every barred-permutation cell. The choice is the parity of the inversion number of the displayed permutation. We avoid quotienting orientations: the chosen sign is an integer equal to 1 or -1, and relabelling is recorded by an explicit orientation-transport sign.

The transport sign is deliberately part of the API. A signed incidence matrix is not invariant under an arbitrary change of chosen cell orientations; it is covariant by the product of the two transport signs. This is the correct datum needed by the later cellular mod-p argument.

def NRR.BarredPermutation.inversionSet {p : ℕ} (c : BarredPermutation p) : Finset (Fin p × Fin p)

Inversions of the displayed permutation, expressed using the natural order on labels and ranks.

Equations

• c.inversionSet = {ij : Fin p × Fin p | ↑ij.1 < ↑ij.2 ∧ ↑(c.rank ij.2) < ↑(c.rank ij.1)}

def NRR.BarredPermutation.inversionCount {p : ℕ} (c : BarredPermutation p) : ℕ

Number of inversions of the displayed permutation.

Equations

• c.inversionCount = c.inversionSet.card

def NRR.BarredPermutation.orientationSign {p : ℕ} (c : BarredPermutation p) : ℤ

Canonical orientation sign of a Fox--Neuwirth cell.

Equations

• c.orientationSign = if Even c.inversionCount then 1 else -1

theorem NRR.BarredPermutation.orientationSign_eq_one_or_neg_one {p : ℕ} (c : BarredPermutation p) : c.orientationSign = 1 ∨ c.orientationSign = -1

Every chosen orientation is represented by one of the two units 1 and -1.

@[simp]

theorem NRR.BarredPermutation.orientationSign_sq {p : ℕ} (c : BarredPermutation p) : c.orientationSign * c.orientationSign = 1

The chosen orientation sign is a unit.

@[simp]

theorem NRR.BarredPermutation.orientationSign_ne_zero {p : ℕ} (c : BarredPermutation p) : c.orientationSign ≠ 0

The chosen orientation never vanishes.

def NRR.BarredPermutation.orientationTransport {p : ℕ} (sigma : Equiv.Perm (Fin p)) (c : BarredPermutation p) : ℤ

Sign comparing the chosen orientation before and after relabelling.

Equations

• NRR.BarredPermutation.orientationTransport sigma c = (NRR.BarredPermutation.relabel sigma c).orientationSign * c.orientationSign

@[simp]

theorem NRR.BarredPermutation.orientationTransport_sq {p : ℕ} (sigma : Equiv.Perm (Fin p)) (c : BarredPermutation p) : orientationTransport sigma c * orientationTransport sigma c = 1

Orientation transport is itself a sign.

theorem NRR.BarredPermutation.orientationTransport_mul_orientationSign {p : ℕ} (sigma : Equiv.Perm (Fin p)) (c : BarredPermutation p) : orientationTransport sigma c * c.orientationSign = (relabel sigma c).orientationSign

Transport followed by the old orientation gives the relabelled orientation.

theorem NRR.BarredPermutation.isFace_relabel_iff {p : ℕ} (sigma : Equiv.Perm (Fin p)) (a b : BarredPermutation p) : (relabel sigma a).IsFace (relabel sigma b) ↔ a.IsFace b

Relabelling reflects as well as preserves the face relation.

theorem NRR.BarredPermutation.isFacet_relabel_iff {p : ℕ} (sigma : Equiv.Perm (Fin p)) (a b : BarredPermutation p) : (relabel sigma a).IsFacet (relabel sigma b) ↔ a.IsFacet b

Relabelling reflects as well as preserves the facet relation.