Orbit quotients of finite incidence cycles

This module turns a finite equivariant incidence cycle into a finite incidence cycle on symmetry orbits. Top and facet cells are represented by the standard quotient types for the group action. The quotient incidence from a facet orbit to a top orbit is the sum of the covering incidences over all members of the top orbit. This is the correct finite operation for orbit zero counts: one keeps one coefficient per top orbit, while incidence is transferred by summing over the covering orbit.

The construction does not divide by the group order. This is essential in characteristic p, where the prime symmetry group has order divisible by p.

structure NRR.FiniteIncidenceCycle.EquivariantData {R : Type u_1} {G : Type u_2} [CommRing R] [Group G] (C : FiniteIncidenceCycle R) [MulAction G C.TopCell] [MulAction G C.Facet] : Prop

Equivariance data for a finite incidence cycle.

• coefficient_smul (g : G) (c : C.TopCell) : C.coefficient (g • c) = C.coefficient c
• incidence_smul (g : G) (f : C.Facet) (c : C.TopCell) : C.incidence (g • f) (g • c) = C.incidence f c

@[reducible, inline]

abbrev NRR.FiniteIncidenceCycle.TopOrbit {R : Type u_1} {G : Type u_2} [CommRing R] [Group G] (C : FiniteIncidenceCycle R) [MulAction G C.TopCell] : Type u_3

Orbit type of top cells.

Equations

• C.TopOrbit = MulAction.orbitRel.Quotient G C.TopCell

@[reducible, inline]

abbrev NRR.FiniteIncidenceCycle.FacetOrbit {R : Type u_1} {G : Type u_2} [CommRing R] [Group G] (C : FiniteIncidenceCycle R) [MulAction G C.Facet] : Type u_4

Orbit type of facets.

Equations

• C.FacetOrbit = MulAction.orbitRel.Quotient G C.Facet

@[instance_reducible]

noncomputable instance NRR.FiniteIncidenceCycle.topOrbitFintype {R : Type u_1} {G : Type u_2} [CommRing R] [Group G] (C : FiniteIncidenceCycle R) [MulAction G C.TopCell] : Fintype C.TopOrbit

Equations

• C.topOrbitFintype = Fintype.ofFinite C.TopOrbit

@[instance_reducible]

noncomputable instance NRR.FiniteIncidenceCycle.facetOrbitFintype {R : Type u_1} {G : Type u_2} [CommRing R] [Group G] (C : FiniteIncidenceCycle R) [MulAction G C.Facet] : Fintype C.FacetOrbit

Equations

• C.facetOrbitFintype = Fintype.ofFinite C.FacetOrbit

@[instance_reducible]

noncomputable instance NRR.FiniteIncidenceCycle.topOrbitDecidableEq {R : Type u_1} {G : Type u_2} [CommRing R] [Group G] (C : FiniteIncidenceCycle R) [MulAction G C.TopCell] : DecidableEq C.TopOrbit

Equations

• C.topOrbitDecidableEq = Classical.decEq C.TopOrbit

@[instance_reducible]

noncomputable instance NRR.FiniteIncidenceCycle.facetOrbitDecidableEq {R : Type u_1} {G : Type u_2} [CommRing R] [Group G] (C : FiniteIncidenceCycle R) [MulAction G C.Facet] : DecidableEq C.FacetOrbit

Equations

• C.facetOrbitDecidableEq = Classical.decEq C.FacetOrbit

noncomputable def NRR.FiniteIncidenceCycle.topRepresentative {R : Type u_1} {G : Type u_2} [CommRing R] [Group G] (C : FiniteIncidenceCycle R) [MulAction G C.TopCell] (q : C.TopOrbit) : C.TopCell

Canonical representative selected by Quotient.out.

Equations

• C.topRepresentative q = Quotient.out q

noncomputable def NRR.FiniteIncidenceCycle.facetRepresentative {R : Type u_1} {G : Type u_2} [CommRing R] [Group G] (C : FiniteIncidenceCycle R) [MulAction G C.Facet] (q : C.FacetOrbit) : C.Facet

Canonical facet representative selected by Quotient.out.

Equations

• C.facetRepresentative q = Quotient.out q

noncomputable def NRR.FiniteIncidenceCycle.orbitCoefficient {R : Type u_1} {G : Type u_2} [CommRing R] [Group G] (C : FiniteIncidenceCycle R) [MulAction G C.TopCell] (q : C.TopOrbit) : R

One coefficient per top-cell orbit.

Equations

• C.orbitCoefficient q = C.coefficient (C.topRepresentative q)

noncomputable def NRR.FiniteIncidenceCycle.orbitIncidence {R : Type u_1} {G : Type u_2} [CommRing R] [Group G] (C : FiniteIncidenceCycle R) [MulAction G C.TopCell] [MulAction G C.Facet] (qf : C.FacetOrbit) (qt : C.TopOrbit) : R

Incidence from a facet orbit to a top orbit, obtained by summing the covering incidences over that top orbit.

Equations

• C.orbitIncidence qf qt = ∑ c : ↑(MulAction.orbitRel.Quotient.orbit qt), C.incidence (C.facetRepresentative qf) ↑c

theorem NRR.FiniteIncidenceCycle.coefficient_eq_representative {R : Type u_1} {G : Type u_2} [CommRing R] [Group G] (C : FiniteIncidenceCycle R) [MulAction G C.TopCell] [MulAction G C.Facet] (E : C.EquivariantData) (q : C.TopOrbit) (c : ↑(MulAction.orbitRel.Quotient.orbit q)) : C.coefficient ↑c = C.orbitCoefficient q

Coefficients are constant on every top orbit.

theorem NRR.FiniteIncidenceCycle.orbitBoundary_eq_coveringBoundary {R : Type u_1} {G : Type u_2} [CommRing R] [Group G] (C : FiniteIncidenceCycle R) [MulAction G C.TopCell] [MulAction G C.Facet] (E : C.EquivariantData) (qf : C.FacetOrbit) : ∑ qt : C.TopOrbit, C.orbitIncidence qf qt * C.orbitCoefficient qt = ∑ c : C.TopCell, C.incidence (C.facetRepresentative qf) c * C.coefficient c

The quotient boundary sum is the original boundary sum at the chosen facet representative.

noncomputable def NRR.FiniteIncidenceCycle.orbitQuotient {R : Type u_1} {G : Type u_2} [CommRing R] [Group G] (C : FiniteIncidenceCycle R) [MulAction G C.TopCell] [MulAction G C.Facet] (E : C.EquivariantData) : FiniteIncidenceCycle R

Orbit quotient of an equivariant finite incidence cycle.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem NRR.FiniteIncidenceCycle.orbitQuotient_coefficient {R : Type u_1} {G : Type u_2} [CommRing R] [Group G] (C : FiniteIncidenceCycle R) [MulAction G C.TopCell] [MulAction G C.Facet] (E : C.EquivariantData) (q : C.TopOrbit) : (C.orbitQuotient E).coefficient q = C.orbitCoefficient q

@[simp]

theorem NRR.FiniteIncidenceCycle.orbitQuotient_incidence {R : Type u_1} {G : Type u_2} [CommRing R] [Group G] (C : FiniteIncidenceCycle R) [MulAction G C.TopCell] [MulAction G C.Facet] (E : C.EquivariantData) (qf : C.FacetOrbit) (qt : C.TopOrbit) : (C.orbitQuotient E).incidence qf qt = C.orbitIncidence qf qt