Hom interaction and translate orthogonality

The covering control relation joins equal objects and pairs carrying a nonzero Hom in either direction. Separation of distinct subgroup translates for this relation makes every nonidentity translated Hom space vanish. This file connects the set-theoretic residual-separation theorem to the exact TranslateHomOrthogonal input used by the orbit Hom formula.

def MagnitudeConjecture.CoveringSeparation.homInteraction {C : Type u} [CategoryTheory.Category.{v, u} C] (X Y : C) : Prop

The symmetric Hom-neighborhood relation used in the manuscript's control windows. Equality is included so that the relation is reflexive even before nonzeroness of the objects under consideration has been established.

@[simp]

theorem MagnitudeConjecture.CoveringSeparation.homInteraction_self {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) : homInteraction X X

theorem MagnitudeConjecture.CoveringSeparation.homInteraction_symm {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} : homInteraction X Y → homInteraction Y X

theorem MagnitudeConjecture.CoveringSeparation.hom_subsingleton_of_not_homInteraction {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (h : ¬homInteraction X Y) : Subsingleton (X ⟶ Y)

Failure of Hom interaction forces the forward Hom space to vanish.

@[reducible, inline]

abbrev MagnitudeConjecture.CoveringSeparation.WindowCategory {C : Type u} [CategoryTheory.Category.{v, u} C] (W : Set C) : Type u

The full subcategory on a set-valued control window.

@[reducible, inline]

abbrev MagnitudeConjecture.CoveringSeparation.windowTranslateHom {C : Type u} [CategoryTheory.Category.{v, u} C] {G : Type w} [Group G] [MulAction G C] (N : Subgroup G) (W : Set C) (X Y : WindowCategory W) (n : ↥N) : Type v

The translated ambient Hom family attached to two objects of a full control-window subcategory and a subgroup of deck transformations.

@[instance_reducible]

instance MagnitudeConjecture.CoveringSeparation.windowTranslateHomAddCommGroup {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {G : Type w} [Group G] [MulAction G C] (N : Subgroup G) (W : Set C) (X Y : WindowCategory W) (n : ↥N) : AddCommGroup (windowTranslateHom N W X Y n)

@[instance_reducible]

instance MagnitudeConjecture.CoveringSeparation.windowTranslateHomModule {C : Type u} [CategoryTheory.Category.{v, u} C] {k : Type w} [Semiring k] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {G : Type w} [Group G] [MulAction G C] (N : Subgroup G) (W : Set C) (X Y : WindowCategory W) (n : ↥N) : Module k (windowTranslateHom N W X Y n)

noncomputable def MagnitudeConjecture.CoveringSeparation.windowIdentityHomLinearEquiv {C : Type u} [CategoryTheory.Category.{v, u} C] {k : Type w} [Semiring k] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {G : Type w} [Group G] [MulAction G C] (N : Subgroup G) (W : Set C) (X Y : WindowCategory W) : (X ⟶ Y) ≃ₗ[k] windowTranslateHom N W X Y 1

The identity translated Hom summand is linearly equivalent to the Hom space of the full window subcategory.

theorem MagnitudeConjecture.CoveringSeparation.windowTranslateHom_orthogonal_of_pairwise_windowSeparated {C : Type u} [CategoryTheory.Category.{v, u} C] {G : Type w} [Group G] [MulAction G C] (N : Subgroup G) (W : Set C) (separated : ∀ {n₁ n₂ : G}, n₁ ∈ N → n₂ ∈ N → n₁ ≠ n₂ → ∀ {X Y : C}, X ∈ W → Y ∈ W → ¬homInteraction (n₁ • X) (n₂ • Y)) : CoveringHom.TranslateHomOrthogonal (windowTranslateHom N W)

Pairwise separation of subgroup translates for homInteraction gives the exact nonidentity translate-Hom orthogonality used by the functor-level Gabriel formula.