Residual separation of a finite control window

The covering argument first isolates a finite family of group elements whose translates of a control window intersect or have a relevant morphism. A finite-index normal subgroup avoiding that family makes distinct subgroup translates disjoint and interaction-free. This file formalizes that exact group-theoretic step, independently of the later covering-category model.

theorem MagnitudeConjecture.CoveringSeparation.exists_finiteIndexNormalSubgroup_avoiding_finset {G : Type u} [Group G] [Group.ResiduallyFinite G] (bad : Finset G) (hne : ∀ g ∈ bad, g ≠ 1) : ∃ (N : FiniteIndexNormalSubgroup G), ∀ g ∈ bad, g ∉ N

Residual finiteness separates every member of a finite set from the identity using one finite-index normal subgroup.

theorem MagnitudeConjecture.CoveringSeparation.exists_finiteIndexNormalSubgroup_avoiding {G : Type u} [Group G] [Group.ResiduallyFinite G] {bad : Set G} (hfinite : bad.Finite) (hne : ∀ g ∈ bad, g ≠ 1) : ∃ (N : FiniteIndexNormalSubgroup G), ∀ g ∈ bad, g ∉ N

Set-valued form of simultaneous residual separation.

def MagnitudeConjecture.CoveringSeparation.WindowInteracts {G : Type u} [Group G] {X : Type v} [MulAction G X] (R : X → X → Prop) (W : Set X) (g : G) : Prop

A control window interacts with its g-translate when the chosen relation holds between some point of the window and some translated point.

def MagnitudeConjecture.CoveringSeparation.badTranslations {G : Type u} [Group G] {X : Type v} [MulAction G X] (R : X → X → Prop) (W : Set X) : Set G

The nonidentity translations whose windows interact.

theorem MagnitudeConjecture.CoveringSeparation.badTranslations_finite {G : Type u} [Group G] {X : Type v} [MulAction G X] (R : X → X → Prop) (W : Set X) (hW : W.Finite) (locallyFinite : ∀ (x y : X), {g : G | R x (g • y)}.Finite) : (badTranslations R W).Finite

Pointwise finiteness of interacting translates makes the bad-translation set of every finite window finite.

theorem MagnitudeConjecture.CoveringSeparation.exists_finiteIndexNormalSubgroup_pairwise_windowSeparated {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) (W : Set X) (hbad : (badTranslations R W).Finite) : ∃ (N : FiniteIndexNormalSubgroup G), ∀ ⦃n₁ n₂ : G⦄, n₁ ∈ N → n₂ ∈ N → n₁ ≠ n₂ → ∀ ⦃x y : X⦄, x ∈ W → y ∈ W → ¬R (n₁ • x) (n₂ • y)

If only finitely many nonidentity translations interact with a control window, residual finiteness supplies a finite-index normal subgroup whose distinct translates are pairwise interaction-free.

For the covering application, R x y means that x = y or that there is a nonzero Hom in either direction.

theorem MagnitudeConjecture.CoveringSeparation.exists_finiteIndexNormalSubgroup_pairwise_windowSeparated_of_localFinite {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) (W : Set X) (hW : W.Finite) (locallyFinite : ∀ (x y : X), {g : G | R x (g • y)}.Finite) : ∃ (N : FiniteIndexNormalSubgroup G), ∀ ⦃n₁ n₂ : G⦄, n₁ ∈ N → n₂ ∈ N → n₁ ≠ n₂ → ∀ ⦃x y : X⦄, x ∈ W → y ∈ W → ¬R (n₁ • x) (n₂ • y)

Local finiteness of interacting translates is the direct hypothesis used in the covering proof to obtain a pairwise separated finite quotient.