Oriented Fox--Neuwirth facet incidences

The cells are all barred permutations. A codimension-one incidence is supported exactly on the facet relation. Its sign is the product of the chosen orientations of the two incident cells. This gives a concrete finite signed incidence matrix. Under relabelling it transforms by the two orientation-transport signs, while its unsigned support is strictly invariant.

This module records the oriented cell model and its boundary relation. The cycle and boundary- cancellation results are proved in the chain modules.

noncomputable def NRR.FoxNeuwirth.faces {p : ℕ} (b : BarredPermutation p) : Finset (BarredPermutation p)

Finite set of all faces of a cell.

Equations

• NRR.FoxNeuwirth.faces b = {a : NRR.BarredPermutation p | a.IsFace b}

noncomputable def NRR.FoxNeuwirth.facets {p : ℕ} (b : BarredPermutation p) : Finset (BarredPermutation p)

Finite set of all codimension-one faces of a cell.

Equations

• NRR.FoxNeuwirth.facets b = {a : NRR.BarredPermutation p | a.IsFacet b}

@[simp]

theorem NRR.FoxNeuwirth.mem_faces_iff {p : ℕ} (a b : BarredPermutation p) : a ∈ faces b ↔ a.IsFace b

@[simp]

theorem NRR.FoxNeuwirth.mem_facets_iff {p : ℕ} (a b : BarredPermutation p) : a ∈ facets b ↔ a.IsFacet b

noncomputable def NRR.FoxNeuwirth.unsignedIncidence {p : ℕ} (a b : BarredPermutation p) : ℤ

Unsigned incidence indicator for a codimension-one face.

Equations

• NRR.FoxNeuwirth.unsignedIncidence a b = if a.IsFacet b then 1 else 0

noncomputable def NRR.FoxNeuwirth.signedIncidence {p : ℕ} (a b : BarredPermutation p) : ℤ

Signed incidence associated with the canonical orientation choices.

Equations

• NRR.FoxNeuwirth.signedIncidence a b = if a.IsFacet b then a.orientationSign * b.orientationSign else 0

@[simp]

theorem NRR.FoxNeuwirth.unsignedIncidence_of_facet {p : ℕ} {a b : BarredPermutation p} (h : a.IsFacet b) : unsignedIncidence a b = 1

@[simp]

theorem NRR.FoxNeuwirth.unsignedIncidence_of_not_facet {p : ℕ} {a b : BarredPermutation p} (h : ¬a.IsFacet b) : unsignedIncidence a b = 0

@[simp]

theorem NRR.FoxNeuwirth.signedIncidence_of_facet {p : ℕ} {a b : BarredPermutation p} (h : a.IsFacet b) : signedIncidence a b = a.orientationSign * b.orientationSign

@[simp]

theorem NRR.FoxNeuwirth.signedIncidence_of_not_facet {p : ℕ} {a b : BarredPermutation p} (h : ¬a.IsFacet b) : signedIncidence a b = 0

theorem NRR.FoxNeuwirth.signedIncidence_ne_zero_iff {p : ℕ} (a b : BarredPermutation p) : signedIncidence a b ≠ 0 ↔ a.IsFacet b

The signed incidence is nonzero exactly for facets.

theorem NRR.FoxNeuwirth.signedIncidence_vanishes_unless_adjacent {p : ℕ} (a b : BarredPermutation p) (h : a.dualDimension + 1 ≠ b.dualDimension) : signedIncidence a b = 0

Incidence can only occur in adjacent dimensions.

theorem NRR.FoxNeuwirth.unsignedIncidence_relabel {p : ℕ} (sigma : Equiv.Perm (Fin p)) (a b : BarredPermutation p) : unsignedIncidence (BarredPermutation.relabel sigma a) (BarredPermutation.relabel sigma b) = unsignedIncidence a b

The unsigned incidence relation is invariant under relabelling.

theorem NRR.FoxNeuwirth.signedIncidence_relabel {p : ℕ} (sigma : Equiv.Perm (Fin p)) (a b : BarredPermutation p) : signedIncidence (BarredPermutation.relabel sigma a) (BarredPermutation.relabel sigma b) = BarredPermutation.orientationTransport sigma a * BarredPermutation.orientationTransport sigma b * signedIncidence a b

Signed incidences are covariant under a change of cell orientations.

noncomputable def NRR.FoxNeuwirth.boundarySupport {p : ℕ} (b : BarredPermutation p) : Finset (BarredPermutation p)

Finite support of the signed boundary of a cell.

Equations

• NRR.FoxNeuwirth.boundarySupport b = {a : NRR.BarredPermutation p | NRR.FoxNeuwirth.signedIncidence a b ≠ 0}

theorem NRR.FoxNeuwirth.boundarySupport_eq_facets {p : ℕ} (b : BarredPermutation p) : boundarySupport b = facets b

Boundary support agrees exactly with the combinatorial facet set.

noncomputable def NRR.FoxNeuwirth.cellularBoundary {p : ℕ} (b : BarredPermutation p) : BarredPermutation p → ℤ

Formal cellular boundary of one oriented cell.

Equations

• NRR.FoxNeuwirth.cellularBoundary b a = NRR.FoxNeuwirth.signedIncidence a b

@[simp]

theorem NRR.FoxNeuwirth.cellularBoundary_apply {p : ℕ} (a b : BarredPermutation p) : cellularBoundary b a = signedIncidence a b

theorem NRR.FoxNeuwirth.cellularBoundary_ne_zero_iff {p : ℕ} (a b : BarredPermutation p) : cellularBoundary b a ≠ 0 ↔ a.IsFacet b

The support of a formal cellular boundary is exactly the set of facets.

theorem NRR.FoxNeuwirth.signedIncidence_prime_smul (p : ℕ) (g : ↥(PrimeSymmetry p)) (a b : BarredPermutation p) : signedIncidence (g • a) (g • b) = BarredPermutation.orientationTransport ((PrimeSymmetry.toPerm p) g) a * BarredPermutation.orientationTransport ((PrimeSymmetry.toPerm p) g) b * signedIncidence a b

Prime-symmetry form of signed incidence covariance.