Explicit representatives for free finite group orbits

Orbit sums in characteristic p cannot be obtained by summing over the covering set and dividing by the group order. This module records chosen representatives together with existence and uniqueness up to the acting group.

structure NRR.OrbitRepresentativeData (G : Type u_1) (X : Type u_2) [Group G] [MulAction G X] [Fintype G] [Fintype X] [DecidableEq X] : Type u_2

Chosen representatives for a finite group action.

• representatives : Finset X

  A finite set containing exactly one representative from each symmetry orbit.

• covers (x : X) : ∃ r ∈ self.representatives, ∃ (g : G), g • r = x
• uniqueOrbit (r₁ : X) : r₁ ∈ self.representatives → ∀ r₂ ∈ self.representatives, (∃ (g : G), g • r₁ = r₂) → r₁ = r₂

def NRR.OrbitRepresentativeData.orbitSum {G : Type u_1} {X : Type u_2} {R : Type u_3} [Group G] [MulAction G X] [Fintype G] [Fintype X] [DecidableEq X] [CommRing R] (D : OrbitRepresentativeData G X) (f : X → R) : R

Sum a function once per chosen orbit.

Equations

• D.orbitSum f = ∑ x ∈ D.representatives, f x

theorem NRR.OrbitRepresentativeData.orbitSum_congr {G : Type u_1} {X : Type u_2} {R : Type u_3} [Group G] [MulAction G X] [Fintype G] [Fintype X] [DecidableEq X] [CommRing R] (D : OrbitRepresentativeData G X) {f g : X → R} (h : ∀ x ∈ D.representatives, f x = g x) : D.orbitSum f = D.orbitSum g

Orbit sums depend only on the values at representatives.

theorem NRR.OrbitRepresentativeData.exists_ne_zero_of_orbitSum_ne_zero {G : Type u_1} {X : Type u_2} {R : Type u_3} [Group G] [MulAction G X] [Fintype G] [Fintype X] [DecidableEq X] [CommRing R] (D : OrbitRepresentativeData G X) (f : X → R) (h : D.orbitSum f ≠ 0) : ∃ x ∈ D.representatives, f x ≠ 0

A nonzero orbit sum has a representative with nonzero contribution.

@[instance_reducible]

noncomputable instance NRR.FoxNeuwirth.instFintypePrimeSymmetry (p : ℕ) : Fintype ↥(PrimeSymmetry p)

C3 data needed for the cellular top cells. The action is already finite; the representative data and subgroup-index relation provide the quotient bookkeeping.

Equations

• NRR.FoxNeuwirth.instFintypePrimeSymmetry p = Fintype.ofFinite ↥(NRR.PrimeSymmetry p)

@[reducible, inline]

abbrev NRR.FoxNeuwirth.CellularTopOrbitRepresentatives (p : ℕ) : Type

Orbit-representative data for the prime action on top-dimensional cells.

Equations

• NRR.FoxNeuwirth.CellularTopOrbitRepresentatives p = NRR.OrbitRepresentativeData (↥(NRR.PrimeSymmetry p)) (NRR.BarredPermutation.TopCell p)