Finite control windows in orbit quotients

Once residual finiteness has separated distinct subgroup translates of a finite control window, passage to the subgroup-orbit quotient is faithful on that window: its points remain distinct and the quotient creates no new instances of the chosen interaction relation. This is the set-theoretic locality statement used before transporting vertices, arrows, and meshes in the covering argument.

def MagnitudeConjecture.CoveringSeparation.OrbitQuotientInteracts {G : Type u} [Group G] {X : Type v} [MulAction G X] (N : Subgroup G) (R : X → X → Prop) (x y : MulAction.orbitRel.Quotient (↥N) X) : Prop

Two subgroup-orbits interact when some representatives interact. This definition is representative-free and does not require the relation to be invariant under translating its two variables independently.

theorem MagnitudeConjecture.CoveringSeparation.orbitQuotientInteracts_mk_iff_of_pairwise_windowSeparated {G : Type u} [Group G] {X : Type v} [MulAction G X] (N : Subgroup G) (R : X → X → Prop) (invariant : ∀ (g : G) (x y : X), R (g • x) (g • y) ↔ R x y) (W : Set X) (separated : ∀ ⦃n₁ n₂ : G⦄, n₁ ∈ N → n₂ ∈ N → n₁ ≠ n₂ → ∀ ⦃x y : X⦄, x ∈ W → y ∈ W → ¬R (n₁ • x) (n₂ • y)) {x y : X} (hx : x ∈ W) (hy : y ∈ W) : OrbitQuotientInteracts N R (Quotient.mk'' x) (Quotient.mk'' y) ↔ R x y

A window whose distinct subgroup translates are interaction-free has exactly its original interaction relation after passing to subgroup-orbits.

theorem MagnitudeConjecture.CoveringSeparation.orbitQuotient_mk_injOn_of_pairwise_windowSeparated {G : Type u} [Group G] {X : Type v} [MulAction G X] (N : Subgroup G) (R : X → X → Prop) (reflexive : ∀ (x : X), R x x) (W : Set X) (separated : ∀ ⦃n₁ n₂ : G⦄, n₁ ∈ N → n₂ ∈ N → n₁ ≠ n₂ → ∀ ⦃x y : X⦄, x ∈ W → y ∈ W → ¬R (n₁ • x) (n₂ • y)) : Set.InjOn (fun (x : X) => Quotient.mk'' x) W

If the separated relation contains equality, the orbit map is injective on the control window.

theorem MagnitudeConjecture.CoveringSeparation.exists_finiteIndexNormalSubgroup_preserving_window {G : Type u} [Group G] {X : Type v} [MulAction G X] [Group.ResiduallyFinite G] (R : X → X → Prop) (invariant : ∀ (g : G) (x y : X), R (g • x) (g • y) ↔ R x y) (reflexive : ∀ (x : X), R x x) (W : Set X) (hW : W.Finite) (locallyFinite : ∀ (x y : X), {g : G | R x (g • y)}.Finite) : ∃ (N : FiniteIndexNormalSubgroup G), Set.InjOn (fun (x : X) => Quotient.mk'' x) W ∧ ∀ ⦃x y : X⦄, x ∈ W → y ∈ W → (OrbitQuotientInteracts N.toSubgroup R (Quotient.mk'' x) (Quotient.mk'' y) ↔ R x y)

Residual separation simultaneously embeds a finite window in a finite index subgroup quotient and preserves its interaction relation there.

theorem MagnitudeConjecture.CoveringSeparation.exists_finiteIndexNormalSubgroup_preserving_window_of_finite_support {G : Type u} [Group G] {X : Type v} [MulAction G X] {O : Type w} [MulAction G O] [IsCancelSMul G O] [Group.ResiduallyFinite G] (support : X → Set O) (support_finite : ∀ (x : X), (support x).Finite) (support_smul : ∀ (g : G) (x : X) (o : O), o ∈ support (g • x) ↔ g⁻¹ • o ∈ support x) (R : X → X → Prop) (invariant : ∀ (g : G) (x y : X), R (g • x) (g • y) ↔ R x y) (reflexive : ∀ (x : X), R x x) (interaction_meets_support : ∀ {x y : X}, R x y → ∃ o ∈ support x, o ∈ support y) (W : Set X) (hW : W.Finite) : ∃ (N : FiniteIndexNormalSubgroup G), Set.InjOn (fun (x : X) => Quotient.mk'' x) W ∧ ∀ ⦃x y : X⦄, x ∈ W → y ∈ W → (OrbitQuotientInteracts N.toSubgroup R (Quotient.mk'' x) (Quotient.mk'' y) ↔ R x y)

Finite equivariant supports and support-detectable interactions supply the finite quotient preserving a finite control window.