Separating finite-support interactions #
For objects with finite support over a freely acted-on base, an interaction that forces the two supports to meet can occur for only finitely many translations. Combined with residual finiteness, this supplies the finite window separation mechanism used for modules over the universal cover.
theorem
MagnitudeConjecture.CoveringSeparation.smulTransporter_finite
{G : Type u}
[Group G]
{O : Type v}
[MulAction G O]
[IsCancelSMul G O]
(source target : O)
:
{g : G | g • source = target}.Finite
Under a free action, the set of group elements carrying one specified base object to another is finite (indeed, subsingleton).
theorem
MagnitudeConjecture.CoveringSeparation.interactionTranslations_finite_of_finite_support
{G : Type u}
[Group G]
{O : Type v}
[MulAction G O]
[IsCancelSMul G O]
{X : Type w}
[MulAction G X]
(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)
(interaction_meets_support : ∀ {x y : X}, R x y → ∃ o ∈ support x, o ∈ support y)
(x y : X)
:
{g : G | R x (g • y)}.Finite
Finite equivariant supports turn support-detectable interactions into pointwise finite sets of translations.
theorem
MagnitudeConjecture.CoveringSeparation.exists_finiteIndexNormalSubgroup_pairwise_windowSeparated_of_finite_support
{G : Type u}
[Group G]
{O : Type v}
[MulAction G O]
[IsCancelSMul G O]
{X : Type w}
[MulAction G X]
[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)
(interaction_meets_support : ∀ {x y : X}, R x y → ∃ o ∈ support x, o ∈ support y)
(W : Set X)
(hW : 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)
Residual finiteness separates a finite window whenever interaction is detected by meeting finite equivariant supports over a freely acted-on base.