Documentation

LeanPool.NandakumarRamanaRao.NRR.PrimePolyhedron.FoxNeuwirth.PrimeOrbitCycle

Prime-symmetry orbit quotient of the Fox--Neuwirth top-flag cycle #

The completed top-flag chain is invariant over ZMod p under the selected prime symmetry group: for odd primes the group consists of even permutations, while for p = 2 both integer signs have the same image modulo two. Simplicial incidence is equivariant because relabelling commutes with face restriction.

This module proves freeness of relabelling on barred permutations and hence on every nonempty order-complex simplex. It then applies the generic orbit-incidence quotient construction to the unconditional top-flag cycle. The resulting finite incidence cycle has one top cell and one facet per prime-symmetry orbit and is the correct input for orbit-level zero counts.

source
theorem NRR.BarredPermutation.primeSymmetry_action_free (p : ℕ) {g : ↥(PrimeSymmetry p)} {c : BarredPermutation p} (hgc : g • c = c) :
g = 1

Relabelling of a barred permutation is free because its rank is a permutation.

source
theorem NRR.FoxNeuwirthOrderComplex.Simplex.primeSymmetry_action_free {d : ℕ} (p : ℕ) {g : ↥(PrimeSymmetry p)} {s : Simplex p d} (hgs : g • s = s) :
g = 1

The prime symmetry action is free on every order-complex simplex.

source
theorem NRR.FoxNeuwirthOrderComplex.PrimeOrbitCycle.primeSymmetry_sign_cast_eq_one (p : ℕ) (g : ↥(PrimeSymmetry p)) :
↑↑(Equiv.Perm.sign ((PrimeSymmetry.toPerm p) g)) = 1

The sign of every selected prime-symmetry permutation becomes one in ZMod p.

source
theorem NRR.FoxNeuwirthOrderComplex.PrimeOrbitCycle.barDifferenceMatrix_smul (p : ℕ) (g : ↥(PrimeSymmetry p)) (s : Simplex p (p - 1)) :
TopFlagSubdivision.barDifferenceMatrix (g • s) = TopFlagSubdivision.barDifferenceMatrix s

Bar indicators and hence bar-removal matrices are unchanged by relabelling.

source
theorem NRR.FoxNeuwirthOrderComplex.PrimeOrbitCycle.barRemovalDeterminant_smul (p : ℕ) (g : ↥(PrimeSymmetry p)) (s : Simplex p (p - 1)) :
TopFlagSubdivision.barRemovalDeterminant (g • s) = TopFlagSubdivision.barRemovalDeterminant s

The bar-removal determinant is invariant under prime-symmetry relabelling.

source
theorem NRR.FoxNeuwirthOrderComplex.PrimeOrbitCycle.permutationOrientationSign_smul (p : ℕ) (g : ↥(PrimeSymmetry p)) (c : BarredPermutation p) :
↑(TopFlagSubdivision.permutationOrientationSign (g • c)) = ↑(TopFlagSubdivision.permutationOrientationSign c)

The bottom-cell orientation changes by the label-permutation sign.

source
theorem NRR.FoxNeuwirthOrderComplex.PrimeOrbitCycle.chain_smul (p : ℕ) (g : ↥(PrimeSymmetry p)) (s : Simplex p (p - 1)) :
TopFlagSubdivision.chain (g • s) = TopFlagSubdivision.chain s

The completed top-flag chain coefficient is constant on prime-symmetry orbits.

source
theorem NRR.FoxNeuwirthOrderComplex.PrimeOrbitCycle.simplicialIncidence_smul {d : ℕ} (p : ℕ) (g : ↥(PrimeSymmetry p)) (target : Simplex p d) (source : Simplex p (d + 1)) :
SimplicialIncidence.incidence (g • target) (g • source) = SimplicialIncidence.incidence target source

Simplicial incidence is invariant under simultaneous relabelling.

source
@[reducible, inline]
noncomputable abbrev NRR.FoxNeuwirthOrderComplex.PrimeOrbitCycle.coveringCycle {p : ℕ} (hp : Nat.Prime p) :
FiniteIncidenceCycle (ZMod p)

The covering finite incidence cycle associated with the completed top-flag chain.

Equations
Instances For
    source
    @[instance_reducible]
    noncomputable instance NRR.FoxNeuwirthOrderComplex.PrimeOrbitCycle.instMulActionCoveringTopCell {p : ℕ} (hp : Nat.Prime p) :
    MulAction (↥(PrimeSymmetry p)) (coveringCycle hp).TopCell
    Equations
    source
    @[instance_reducible]
    noncomputable instance NRR.FoxNeuwirthOrderComplex.PrimeOrbitCycle.instMulActionCoveringFacet {p : ℕ} (hp : Nat.Prime p) :
    MulAction (↥(PrimeSymmetry p)) (coveringCycle hp).Facet
    Equations
    source
    theorem NRR.FoxNeuwirthOrderComplex.PrimeOrbitCycle.coveringEquivariantData {p : ℕ} (hp : Nat.Prime p) :
    (coveringCycle hp).EquivariantData

    Equivariance data for the covering top-flag cycle.

    source
    noncomputable def NRR.FoxNeuwirthOrderComplex.PrimeOrbitCycle.orbitCycle {p : ℕ} (hp : Nat.Prime p) :
    FiniteIncidenceCycle (ZMod p)

    Prime-symmetry orbit quotient of the unconditional top-flag cycle.

    Equations
    Instances For
      source
      theorem NRR.FoxNeuwirthOrderComplex.PrimeOrbitCycle.orbitCycle_boundary_zero {p : ℕ} (hp : Nat.Prime p) (f : (orbitCycle hp).Facet) :
      ∑ c : (orbitCycle hp).TopCell, (orbitCycle hp).incidence f c * (orbitCycle hp).coefficient c = 0

      The quotient cycle has zero boundary by construction.

      source
      @[reducible, inline]
      abbrev NRR.FoxNeuwirthOrderComplex.PrimeOrbitCycle.TopOrbit {p : ℕ} (hp : Nat.Prime p) :
      Type

      Top orbit type of the prime-symmetry quotient.

      Equations
      Instances For
        source
        @[reducible, inline]
        abbrev NRR.FoxNeuwirthOrderComplex.PrimeOrbitCycle.FacetOrbit {p : ℕ} (hp : Nat.Prime p) :
        Type

        Facet orbit type of the prime-symmetry quotient.

        Equations
        Instances For
          source
          noncomputable def NRR.FoxNeuwirthOrderComplex.PrimeOrbitCycle.topRepresentative {p : ℕ} (hp : Nat.Prime p) (q : TopOrbit hp) :
          (coveringCycle hp).TopCell

          Canonical representative of a top orbit.

          Equations
          Instances For
            source
            noncomputable def NRR.FoxNeuwirthOrderComplex.PrimeOrbitCycle.facetRepresentative {p : ℕ} (hp : Nat.Prime p) (q : FacetOrbit hp) :
            (coveringCycle hp).Facet

            Canonical representative of a facet orbit.

            Equations
            Instances For
              source
              theorem NRR.AAK.simplestRoute_primeOrbitCycle_complete {p : ℕ} (_hp : Nat.Prime p) :
              Nonempty (FiniteIncidenceCycle (ZMod p))

              Step S4: the completed Fox--Neuwirth simplicial cycle descends to a finite incidence cycle on prime-symmetry top and facet orbits.