Incoming occurrences in orbit quotients

An equivariant map from arrow occurrences to their target vertices descends to every subgroup-orbit quotient. When the action on vertices is free, the arrows ending at a chosen lift are in bijection with the arrow-orbits ending at its quotient vertex: every orbit has a unique representative with that target. This is the combinatorial content of preservation of incoming arrow multiplicity, and hence of the arrow term in the manuscript's local density.

def MagnitudeConjecture.CoveringAction.groupOrbitQuotientMap {G : Type u} [Group G] {X : Type v} {Y : Type w} [MulAction G X] [MulAction G Y] (f : X → Y) (equivariant : ∀ (g : G) (x : X), f (g • x) = g • f x) : MulAction.orbitRel.Quotient G X → MulAction.orbitRel.Quotient G Y

An equivariant map descends to the orbit quotient by the whole acting group.

@[simp]

theorem MagnitudeConjecture.CoveringAction.groupOrbitQuotientMap_mk {G : Type u} [Group G] {X : Type v} {Y : Type w} [MulAction G X] [MulAction G Y] (f : X → Y) (equivariant : ∀ (g : G) (x : X), f (g • x) = g • f x) (x : X) : groupOrbitQuotientMap f equivariant (Quotient.mk'' x) = Quotient.mk'' (f x)

def MagnitudeConjecture.CoveringAction.orbitQuotientMap {G : Type u} [Group G] {X : Type v} {Y : Type w} [MulAction G X] [MulAction G Y] (N : Subgroup G) (f : X → Y) (equivariant : ∀ (g : G) (x : X), f (g • x) = g • f x) : MulAction.orbitRel.Quotient (↥N) X → MulAction.orbitRel.Quotient (↥N) Y

An equivariant map descends to the orbit quotients by any subgroup.

@[simp]

theorem MagnitudeConjecture.CoveringAction.orbitQuotientMap_mk {G : Type u} [Group G] {X : Type v} {Y : Type w} [MulAction G X] [MulAction G Y] (N : Subgroup G) (f : X → Y) (equivariant : ∀ (g : G) (x : X), f (g • x) = g • f x) (x : X) : orbitQuotientMap N f equivariant (Quotient.mk'' x) = Quotient.mk'' (f x)

theorem MagnitudeConjecture.CoveringAction.orbitQuotientMap_quotient_equivariant {G : Type u} [Group G] {X : Type v} {Y : Type w} [MulAction G X] [MulAction G Y] (N : Subgroup G) [N.Normal] (f : X → Y) (equivariant : ∀ (g : G) (x : X), f (g • x) = g • f x) (q : G ⧸ N) (z : MulAction.orbitRel.Quotient (↥N) X) : orbitQuotientMap N f equivariant (q • z) = q • orbitQuotientMap N f equivariant z

The map on N-orbits remains equivariant for the residual G / N action.

theorem MagnitudeConjecture.CoveringAction.orbitTowerEquiv_naturality {G : Type u} [Group G] {X : Type v} {Y : Type w} [MulAction G X] [MulAction G Y] (N : Subgroup G) [N.Normal] (f : X → Y) (equivariant : ∀ (g : G) (x : X), f (g • x) = g • f x) (z : MulAction.orbitRel.Quotient (G ⧸ N) (MulAction.orbitRel.Quotient (↥N) X)) : (orbitTowerEquiv N) (groupOrbitQuotientMap (orbitQuotientMap N f equivariant) ⋯ z) = groupOrbitQuotientMap f equivariant ((orbitTowerEquiv N) z)

The orbit-tower equivalence is natural for equivariant maps: descending first by N and then by G / N agrees with descending directly by G.

noncomputable def MagnitudeConjecture.CoveringAction.groupOrbitQuotientMapFiberEquiv {G : Type u} [Group G] {X : Type v} {Y : Type w} [MulAction G X] [MulAction G Y] [IsCancelSMul G Y] (f : X → Y) (equivariant : ∀ (g : G) (x : X), f (g • x) = g • f x) (y : Y) : { x : X // f x = y } ≃ { q : MulAction.orbitRel.Quotient G X // groupOrbitQuotientMap f equivariant q = Quotient.mk'' y }

For a free action on the target, every whole-group orbit in a fibre of the descended map has a unique representative in the corresponding original fibre.

noncomputable def MagnitudeConjecture.CoveringAction.orbitQuotientMapFiberEquiv {G : Type u} [Group G] {X : Type v} {Y : Type w} [MulAction G X] [MulAction G Y] [IsCancelSMul G Y] (N : Subgroup G) (f : X → Y) (equivariant : ∀ (g : G) (x : X), f (g • x) = g • f x) (y : Y) : { x : X // f x = y } ≃ { q : MulAction.orbitRel.Quotient (↥N) X // orbitQuotientMap N f equivariant q = Quotient.mk'' y }

For a free action on the target, every orbit in a fibre of the descended map has a unique representative in the corresponding original fibre.

theorem MagnitudeConjecture.CoveringAction.card_orbitQuotientMap_fiber_eq {G : Type u} [Group G] {X : Type v} {Y : Type w} [MulAction G X] [MulAction G Y] [IsCancelSMul G Y] [Finite X] (N : Subgroup G) (f : X → Y) (equivariant : ∀ (g : G) (x : X), f (g • x) = g • f x) (y : Y) : Nat.card { q : MulAction.orbitRel.Quotient (↥N) X // orbitQuotientMap N f equivariant q = Quotient.mk'' y } = Nat.card { x : X // f x = y }

Cardinal form of the fibre equivalence.

theorem MagnitudeConjecture.CoveringAction.card_groupOrbitQuotientMap_fiber_eq {G : Type u} [Group G] {X : Type v} {Y : Type w} [MulAction G X] [MulAction G Y] [IsCancelSMul G Y] [Finite X] (f : X → Y) (equivariant : ∀ (g : G) (x : X), f (g • x) = g • f x) (y : Y) : Nat.card { q : MulAction.orbitRel.Quotient G X // groupOrbitQuotientMap f equivariant q = Quotient.mk'' y } = Nat.card { x : X // f x = y }

Cardinal form of the whole-group fibre equivalence.

noncomputable def MagnitudeConjecture.CoveringAction.occurrenceIndegree {Arrow : Type u_1} {Vertex : Type u_2} [Finite Arrow] (target : Arrow → Vertex) (v : Vertex) : ℤ

Incoming arrow occurrences at a vertex, counted with multiplicity.

noncomputable def MagnitudeConjecture.CoveringAction.occurrenceLocalDensity {Arrow : Type u_1} {Vertex : Type u_2} [Finite Arrow] (target : Arrow → Vertex) (IsProjective : Vertex → Prop) (v : Vertex) : ℤ

The local density written directly in terms of incoming arrow occurrences.

noncomputable def MagnitudeConjecture.CoveringAction.arrowMultiplicityOfOccurrences {Arrow : Type u_1} {Vertex : Type u_2} [Finite Arrow] (source target : Arrow → Vertex) (x y : Vertex) : ℕ

The arrow-multiplicity matrix obtained by counting a type of arrow occurrences with specified source and target.

noncomputable def MagnitudeConjecture.CoveringAction.targetFiberEquivSigmaSourceFibers {Arrow : Type u_1} {Vertex : Type u_2} (source target : Arrow → Vertex) (y : Vertex) : { a : Arrow // target a = y } ≃ (x : Vertex) × { a : Arrow // source a = x ∧ target a = y }

Partition the arrows ending at y according to their source.

theorem MagnitudeConjecture.CoveringAction.indegree_arrowMultiplicityOfOccurrences_eq {Arrow : Type u_1} {Vertex : Type u_2} [Finite Arrow] [Fintype Vertex] (source target : Arrow → Vertex) (y : Vertex) : ARCount.indegree (arrowMultiplicityOfOccurrences source target) y = occurrenceIndegree target y

Summing the occurrence multiplicities over all sources gives the literal cardinality of the incoming-arrow fibre.

theorem MagnitudeConjecture.CoveringAction.localDensity_arrowMultiplicityOfOccurrences_eq {Arrow : Type u_1} {Vertex : Type u_2} [Finite Arrow] [Fintype Vertex] (source target : Arrow → Vertex) (IsProjective : Vertex → Prop) [DecidablePred IsProjective] (y : Vertex) : ARCount.localDensity (arrowMultiplicityOfOccurrences source target) IsProjective y = occurrenceLocalDensity target IsProjective y

The occurrence form of local density is exactly the manuscript's arrow-multiplicity-matrix form.

def MagnitudeConjecture.CoveringAction.OrbitQuotientProperty {G : Type u} [Group G] {Y : Type w} [MulAction G Y] (N : Subgroup G) (P : Y → Prop) (q : MulAction.orbitRel.Quotient (↥N) Y) : Prop

An orbit has a property when one of its representatives has it.

def MagnitudeConjecture.CoveringAction.GroupOrbitQuotientProperty {G : Type u} [Group G] {Y : Type w} [MulAction G Y] (P : Y → Prop) (q : MulAction.orbitRel.Quotient G Y) : Prop

A whole-group orbit has a property when one of its representatives has it.

theorem MagnitudeConjecture.CoveringAction.orbitQuotientProperty_mk_iff {G : Type u} [Group G] {Y : Type w} [MulAction G Y] (N : Subgroup G) (P : Y → Prop) (invariant : ∀ (g : G) (y : Y), P (g • y) ↔ P y) (y : Y) : OrbitQuotientProperty N P (Quotient.mk'' y) ↔ P y

An invariant property holds on the orbit of a point exactly when it holds at that point.

theorem MagnitudeConjecture.CoveringAction.groupOrbitQuotientProperty_mk_iff {G : Type u} [Group G] {Y : Type w} [MulAction G Y] (P : Y → Prop) (invariant : ∀ (g : G) (y : Y), P (g • y) ↔ P y) (y : Y) : GroupOrbitQuotientProperty P (Quotient.mk'' y) ↔ P y

An invariant property holds on the whole-group orbit of a point exactly when it holds at that point.

theorem MagnitudeConjecture.CoveringAction.orbitQuotientProperty_quotient_invariant {G : Type u} [Group G] {Y : Type w} [MulAction G Y] (N : Subgroup G) [N.Normal] (P : Y → Prop) (invariant : ∀ (g : G) (y : Y), P (g • y) ↔ P y) (q : G ⧸ N) (z : MulAction.orbitRel.Quotient (↥N) Y) : OrbitQuotientProperty N P (q • z) ↔ OrbitQuotientProperty N P z

An invariant property on Y induces an invariant property of N-orbits under the residual G / N action.

theorem MagnitudeConjecture.CoveringAction.groupOrbitQuotientProperty_orbitTowerEquiv_iff {G : Type u} [Group G] {Y : Type w} [MulAction G Y] (N : Subgroup G) [N.Normal] (P : Y → Prop) (invariant : ∀ (g : G) (y : Y), P (g • y) ↔ P y) (z : MulAction.orbitRel.Quotient (G ⧸ N) (MulAction.orbitRel.Quotient (↥N) Y)) : GroupOrbitQuotientProperty (OrbitQuotientProperty N P) z ↔ GroupOrbitQuotientProperty P ((orbitTowerEquiv N) z)

The property on the two-stage orbit agrees, through orbit flattening, with the corresponding property on the direct whole-group orbit.

theorem MagnitudeConjecture.CoveringAction.occurrenceIndegree_orbitQuotientMap_mk {G : Type u} [Group G] {X : Type v} {Y : Type w} [MulAction G X] [MulAction G Y] [IsCancelSMul G Y] [Finite X] (N : Subgroup G) (target : X → Y) (target_equivariant : ∀ (g : G) (a : X), target (g • a) = g • target a) (y : Y) : occurrenceIndegree (orbitQuotientMap N target target_equivariant) (Quotient.mk'' y) = occurrenceIndegree target y

Incoming occurrence multiplicity is unchanged at a chosen lift after passing to a subgroup-orbit quotient.

theorem MagnitudeConjecture.CoveringAction.occurrenceIndegree_groupOrbitQuotientMap_mk {G : Type u} [Group G] {X : Type v} {Y : Type w} [MulAction G X] [MulAction G Y] [IsCancelSMul G Y] [Finite X] (target : X → Y) (target_equivariant : ∀ (g : G) (a : X), target (g • a) = g • target a) (y : Y) : occurrenceIndegree (groupOrbitQuotientMap target target_equivariant) (Quotient.mk'' y) = occurrenceIndegree target y

Incoming occurrence multiplicity is unchanged at a chosen lift after passing to the whole-group orbit quotient.

theorem MagnitudeConjecture.CoveringAction.occurrenceLocalDensity_orbitQuotientMap_mk {G : Type u} [Group G] {X : Type v} {Y : Type w} [MulAction G X] [MulAction G Y] [IsCancelSMul G Y] [Finite X] (N : Subgroup G) (target : X → Y) (target_equivariant : ∀ (g : G) (a : X), target (g • a) = g • target a) (IsProjective : Y → Prop) (projective_invariant : ∀ (g : G) (y : Y), IsProjective (g • y) ↔ IsProjective y) (y : Y) : occurrenceLocalDensity (orbitQuotientMap N target target_equivariant) (OrbitQuotientProperty N IsProjective) (Quotient.mk'' y) = occurrenceLocalDensity target IsProjective y

If projectivity is invariant on vertex orbits, then the full local density is unchanged at a chosen lift.

theorem MagnitudeConjecture.CoveringAction.occurrenceLocalDensity_groupOrbitQuotientMap_mk {G : Type u} [Group G] {X : Type v} {Y : Type w} [MulAction G X] [MulAction G Y] [IsCancelSMul G Y] [Finite X] (target : X → Y) (target_equivariant : ∀ (g : G) (a : X), target (g • a) = g • target a) (IsProjective : Y → Prop) (projective_invariant : ∀ (g : G) (y : Y), IsProjective (g • y) ↔ IsProjective y) (y : Y) : occurrenceLocalDensity (groupOrbitQuotientMap target target_equivariant) (GroupOrbitQuotientProperty IsProjective) (Quotient.mk'' y) = occurrenceLocalDensity target IsProjective y

If projectivity is invariant on vertex orbits, then the full local density is unchanged at a chosen lift after the whole-group quotient.

theorem MagnitudeConjecture.CoveringAction.occurrenceLocalDensity_invariant {G : Type u} [Group G] {X : Type v} {Y : Type w} [MulAction G X] [MulAction G Y] [IsCancelSMul G Y] [Finite X] (target : X → Y) (target_equivariant : ∀ (g : G) (a : X), target (g • a) = g • target a) (IsProjective : Y → Prop) (projective_invariant : ∀ (g : G) (y : Y), IsProjective (g • y) ↔ IsProjective y) (g : G) (y : Y) : occurrenceLocalDensity target IsProjective (g • y) = occurrenceLocalDensity target IsProjective y

Occurrence local density is invariant under the group action whenever the target action is free and projectivity is invariant.

theorem MagnitudeConjecture.CoveringAction.orbitInvariantDescend_occurrenceLocalDensity {G : Type u} [Group G] {X : Type v} {Y : Type w} [MulAction G X] [MulAction G Y] [IsCancelSMul G Y] [Finite X] (target : X → Y) (target_equivariant : ∀ (g : G) (a : X), target (g • a) = g • target a) (IsProjective : Y → Prop) (projective_invariant : ∀ (g : G) (y : Y), IsProjective (g • y) ↔ IsProjective y) (q : MulAction.orbitRel.Quotient G Y) : orbitInvariantDescend (occurrenceLocalDensity target IsProjective) ⋯ q = occurrenceLocalDensity (groupOrbitQuotientMap target target_equivariant) (GroupOrbitQuotientProperty IsProjective) q

Descending the invariant upstairs local density gives exactly the local density formed from the quotient occurrence and projectivity data.

theorem MagnitudeConjecture.CoveringAction.sum_occurrenceLocalDensity_eq_group_card_mul_quotient {G : Type u} [Group G] {X : Type v} {Y : Type w} [MulAction G X] [MulAction G Y] [Fintype G] [Fintype X] [Fintype Y] [Fintype (MulAction.orbitRel.Quotient G Y)] [IsCancelSMul G Y] (target : X → Y) (target_equivariant : ∀ (g : G) (a : X), target (g • a) = g • target a) (IsProjective : Y → Prop) (projective_invariant : ∀ (g : G) (y : Y), IsProjective (g • y) ↔ IsProjective y) : ∑ y : Y, occurrenceLocalDensity target IsProjective y = ↑(Fintype.card G) * ∑ q : MulAction.orbitRel.Quotient G Y, occurrenceLocalDensity (groupOrbitQuotientMap target target_equivariant) (GroupOrbitQuotientProperty IsProjective) q

Endpoint scaling in local-density form: the total upstairs occurrence local density is the covering degree times the total quotient density. No separate free action on a chosen set of arrow bases is required.

theorem MagnitudeConjecture.CoveringAction.occurrenceLocalDensity_iteratedOrbitQuotientMap_mk {G : Type u} [Group G] {X : Type v} {Y : Type w} [MulAction G X] [MulAction G Y] [IsCancelSMul G Y] [Finite X] (N : Subgroup G) [N.Normal] (target : X → Y) (target_equivariant : ∀ (g : G) (a : X), target (g • a) = g • target a) (IsProjective : Y → Prop) (projective_invariant : ∀ (g : G) (y : Y), IsProjective (g • y) ↔ IsProjective y) (y : Y) : occurrenceLocalDensity (groupOrbitQuotientMap (orbitQuotientMap N target target_equivariant) ⋯) (GroupOrbitQuotientProperty (OrbitQuotientProperty N IsProjective)) (Quotient.mk'' (Quotient.mk'' y)) = occurrenceLocalDensity target IsProjective y

Local density is unchanged by first quotienting by N and then by the residual G / N action.

theorem MagnitudeConjecture.CoveringAction.occurrenceLocalDensity_orbitTowerEquiv {G : Type u} [Group G] {X : Type v} {Y : Type w} [MulAction G X] [MulAction G Y] [IsCancelSMul G Y] [Finite X] (N : Subgroup G) [N.Normal] (target : X → Y) (target_equivariant : ∀ (g : G) (a : X), target (g • a) = g • target a) (IsProjective : Y → Prop) (projective_invariant : ∀ (g : G) (y : Y), IsProjective (g • y) ↔ IsProjective y) (z : MulAction.orbitRel.Quotient (G ⧸ N) (MulAction.orbitRel.Quotient (↥N) Y)) : occurrenceLocalDensity (groupOrbitQuotientMap (orbitQuotientMap N target target_equivariant) ⋯) (GroupOrbitQuotientProperty (OrbitQuotientProperty N IsProjective)) z = occurrenceLocalDensity (groupOrbitQuotientMap target target_equivariant) (GroupOrbitQuotientProperty IsProjective) ((orbitTowerEquiv N) z)

Through orbit flattening, the two-stage occurrence local density is the direct whole-group occurrence local density at every quotient vertex.