Deck quotient action on orbit classes

If a group G acts on X and N is normal, then G / N acts on the set of N-orbits in X. A free G-action induces a free quotient action. This is the group-action calculation used for the endpoint scaling in the finite covering average.

def MagnitudeConjecture.CoveringAction.orbitInvariantDescend {G : Type u} [Group G] {X : Type v} [MulAction G X] {M : Type u_1} [AddCommMonoid M] (f : X → M) (invariant : ∀ (g : G) (x : X), f (g • x) = f x) : MulAction.orbitRel.Quotient G X → M

An invariant function descends to the orbit quotient.

@[simp]

theorem MagnitudeConjecture.CoveringAction.orbitInvariantDescend_mk {G : Type u} [Group G] {X : Type v} [MulAction G X] {M : Type u_1} [AddCommMonoid M] (f : X → M) (invariant : ∀ (g : G) (x : X), f (g • x) = f x) (x : X) : orbitInvariantDescend f invariant (Quotient.mk'' x) = f x

def MagnitudeConjecture.CoveringAction.orbitClassifierDescend {G : Type u} [Group G] {X : Type v} [MulAction G X] {Y : Type u_1} (c : X → Y) (invariant : ∀ (g : G) (x : X), c (g • x) = c x) : MulAction.orbitRel.Quotient G X → Y

A function constant on orbits descends to its orbit quotient, without any algebraic structure on the codomain.

@[simp]

theorem MagnitudeConjecture.CoveringAction.orbitClassifierDescend_mk {G : Type u} [Group G] {X : Type v} [MulAction G X] {Y : Type u_1} (c : X → Y) (invariant : ∀ (g : G) (x : X), c (g • x) = c x) (x : X) : orbitClassifierDescend c invariant (Quotient.mk'' x) = c x

theorem MagnitudeConjecture.CoveringAction.orbitClassifierDescend_bijective {G : Type u} [Group G] {X : Type v} [MulAction G X] {Y : Type u_1} (c : X → Y) (invariant : ∀ (g : G) (x : X), c (g • x) = c x) (surjective : Function.Surjective c) (fiber : ∀ (x y : X), c x = c y → ∃ (g : G), g • y = x) : Function.Bijective (orbitClassifierDescend c invariant)

An orbit classifier is bijective on the orbit quotient when it is surjective and its fibres are exactly the orbits.

noncomputable def MagnitudeConjecture.CoveringAction.orbitClassifierEquiv {G : Type u} [Group G] {X : Type v} [MulAction G X] {Y : Type u_1} (c : X → Y) (invariant : ∀ (g : G) (x : X), c (g • x) = c x) (surjective : Function.Surjective c) (fiber : ∀ (x y : X), c x = c y → ∃ (g : G), g • y = x) : MulAction.orbitRel.Quotient G X ≃ Y

The equivalence induced by a complete orbit classifier with orbit fibres.

theorem MagnitudeConjecture.CoveringAction.sum_orbitInvariantDescend_eq_sum_of_orbitClassifier {G : Type u} [Group G] {X : Type v} [MulAction G X] {Y : Type u_1} {M : Type u_2} [Fintype X] [Fintype (MulAction.orbitRel.Quotient G X)] [Fintype Y] [AddCommMonoid M] (c : X → Y) (c_invariant : ∀ (g : G) (x : X), c (g • x) = c x) (c_surjective : Function.Surjective c) (c_fiber : ∀ (x y : X), c x = c y → ∃ (g : G), g • y = x) (f : X → M) (f_invariant : ∀ (g : G) (x : X), f (g • x) = f x) (t : Y → M) (value_eq : ∀ (x : X), f x = t (c x)) : ∑ q : MulAction.orbitRel.Quotient G X, orbitInvariantDescend f f_invariant q = ∑ y : Y, t y

Reindex an orbit sum along a complete orbit classifier whose fibres are exactly the orbits.

theorem MagnitudeConjecture.CoveringAction.sum_eq_card_nsmul_sum_orbitInvariantDescend {G : Type u} [Group G] {X : Type v} [MulAction G X] {M : Type u_1} [AddCommMonoid M] [Fintype G] [Fintype X] [Fintype (MulAction.orbitRel.Quotient G X)] [IsCancelSMul G X] (f : X → M) (invariant : ∀ (g : G) (x : X), f (g • x) = f x) : ∑ x : X, f x = Fintype.card G • ∑ q : MulAction.orbitRel.Quotient G X, orbitInvariantDescend f invariant q

For a finite free action, the sum of an invariant function is the group order times its sum over the orbit quotient.

theorem MagnitudeConjecture.CoveringAction.sum_eq_card_mul_sum_orbitInvariantDescend {G : Type u} [Group G] {X : Type v} [MulAction G X] [Fintype G] [Fintype X] [Fintype (MulAction.orbitRel.Quotient G X)] [IsCancelSMul G X] (f : X → ℤ) (invariant : ∀ (g : G) (x : X), f (g • x) = f x) : ∑ x : X, f x = ↑(Fintype.card G) * ∑ q : MulAction.orbitRel.Quotient G X, orbitInvariantDescend f invariant q

Integer form of invariant-sum scaling, matching the covering-average arithmetic.

theorem MagnitudeConjecture.CoveringAction.card_eq_orbitQuotient_card_mul_group_card {Q : Type u} [Group Q] {Y : Type v} [MulAction Q Y] [IsCancelSMul Q Y] [Fintype Q] [Fintype Y] [Fintype (MulAction.orbitRel.Quotient Q Y)] : Fintype.card Y = Fintype.card (MulAction.orbitRel.Quotient Q Y) * Fintype.card Q

Every orbit quotient of a finite free action has uniform fibre size equal to the order of the acting group. This cardinal form is what scales the vertex, arrow-occurrence, and mesh counts at the covering endpoints.

theorem MagnitudeConjecture.CoveringAction.eulerSurplus_scale_of_free_actions {Q : Type u} [Group Q] {Arrow Mesh : Type v} [MulAction Q Arrow] [MulAction Q Mesh] [IsCancelSMul Q Arrow] [IsCancelSMul Q Mesh] [Fintype Q] [Fintype Arrow] [Fintype Mesh] [Fintype (MulAction.orbitRel.Quotient Q Arrow)] [Fintype (MulAction.orbitRel.Quotient Q Mesh)] : 2 * ↑(Fintype.card Mesh) - ↑(Fintype.card Arrow) = ↑(Fintype.card Q) * (2 * ↑(Fintype.card (MulAction.orbitRel.Quotient Q Mesh)) - ↑(Fintype.card (MulAction.orbitRel.Quotient Q Arrow)))

Uniform free fibres scale the integer mesh-minus-arrow surplus by the order of the acting group.

@[instance_reducible]

noncomputable instance MagnitudeConjecture.CoveringAction.orbitQuotientMulAction {G : Type u} [Group G] {X : Type v} [MulAction G X] (N : Subgroup G) [N.Normal] : MulAction (G ⧸ N) (MulAction.orbitRel.Quotient (↥N) X)

The canonical action of G / N on the set of N-orbits in X.

@[simp]

theorem MagnitudeConjecture.CoveringAction.quotient_smul_orbit_mk {G : Type u} [Group G] {X : Type v} [MulAction G X] (N : Subgroup G) [N.Normal] (g : G) (x : X) : ↑g • Quotient.mk'' x = Quotient.mk'' (g • x)

The quotient action is represented by applying a representative before passing to the orbit quotient.

noncomputable def MagnitudeConjecture.CoveringAction.orbitTowerEquiv {G : Type u} [Group G] {X : Type v} [MulAction G X] (N : Subgroup G) [N.Normal] : MulAction.orbitRel.Quotient (G ⧸ N) (MulAction.orbitRel.Quotient (↥N) X) ≃ MulAction.orbitRel.Quotient G X

Taking N-orbits and then G / N-orbits gives the same orbit set as taking G-orbits directly.

@[simp]

theorem MagnitudeConjecture.CoveringAction.orbitTowerEquiv_mk {G : Type u} [Group G] {X : Type v} [MulAction G X] (N : Subgroup G) [N.Normal] (x : X) : (orbitTowerEquiv N) (Quotient.mk'' (Quotient.mk'' x)) = Quotient.mk'' x

@[simp]

theorem MagnitudeConjecture.CoveringAction.orbitTowerEquiv_symm_mk {G : Type u} [Group G] {X : Type v} [MulAction G X] (N : Subgroup G) [N.Normal] (x : X) : (orbitTowerEquiv N).symm (Quotient.mk'' x) = Quotient.mk'' (Quotient.mk'' x)

instance MagnitudeConjecture.CoveringAction.orbitQuotientIsCancelSMul {G : Type u} [Group G] {X : Type v} [MulAction G X] (N : Subgroup G) [N.Normal] [IsCancelSMul G X] : IsCancelSMul (G ⧸ N) (MulAction.orbitRel.Quotient (↥N) X)

Freeness descends from a group action to the quotient action on subgroup orbits. This is the manuscript's endpoint-fibre freeness argument.