Finite-support summands of pull-up/push-down

An idempotent on the explicit direct sum of pairwise nonisomorphic indecomposable translates is the identity if every diagonal component is an isomorphism. The proof restricts each individual direct-sum element to its finite support and applies the finite Krull--Schmidt matrix theorem.

theorem MagnitudeConjecture.CoveringHom.instHasFiniteBiproductsFunctorModuleCat_magnitudeConjecture {k : Type uK} [CommRing k] {C : Type u} [CategoryTheory.Category.{v, u} C] : CategoryTheory.Limits.HasFiniteBiproducts (CategoryTheory.Functor C (ModuleCat k))

@[reducible, inline]

abbrev MagnitudeConjecture.CoveringHom.orbitPullupPushdownFiniteIndex {A : Type w} (s : Finset A) : Type

A small finite index type enumerating a finite subset of the deck group.

noncomputable def MagnitudeConjecture.CoveringHom.orbitPullupPushdownFiniteLabel {A : Type w} (s : Finset A) (i : orbitPullupPushdownFiniteIndex s) : A

The deck-group label at one index of the chosen finite enumeration.

theorem MagnitudeConjecture.CoveringHom.orbitPullupPushdownFiniteLabel_mem {A : Type w} (s : Finset A) (i : orbitPullupPushdownFiniteIndex s) : orbitPullupPushdownFiniteLabel s i ∈ s

theorem MagnitudeConjecture.CoveringHom.orbitPullupPushdownFiniteLabel_injective {A : Type w} (s : Finset A) : Function.Injective (orbitPullupPushdownFiniteLabel s)

@[reducible, inline]

noncomputable abbrev MagnitudeConjecture.CoveringHom.orbitPullupPushdownFiniteTranslate {k : Type uK} [CommRing k] {C : Type u} [CategoryTheory.Category.{v, u} C] {A : Type w} [AddGroup A] [CategoryTheory.HasShift C A] (M : CategoryTheory.Functor C (ModuleCat k)) (s : Finset A) : CategoryTheory.Functor C (ModuleCat k)

The finite biproduct of translates indexed by a finite subset of the deck group.

noncomputable def MagnitudeConjecture.CoveringHom.orbitPullupPushdownFiniteInclude {k : Type uK} [CommRing k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {A : Type w} [AddGroup A] [CategoryTheory.HasShift C A] [∀ (a : A), (CategoryTheory.shiftFunctor C a).Additive] [∀ (a : A), CategoryTheory.Functor.Linear k (CategoryTheory.shiftFunctor C a)] (M : CategoryTheory.Functor C (ModuleCat k)) [M.Additive] [CategoryTheory.Functor.Linear k M] (s : Finset A) : orbitPullupPushdownFiniteTranslate M s ⟶ orbitPullupPushdown M

Include a finite biproduct of translates in the full direct sum.

noncomputable def MagnitudeConjecture.CoveringHom.orbitPullupPushdownFiniteProject {k : Type uK} [CommRing k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {A : Type w} [AddGroup A] [CategoryTheory.HasShift C A] [∀ (a : A), (CategoryTheory.shiftFunctor C a).Additive] [∀ (a : A), CategoryTheory.Functor.Linear k (CategoryTheory.shiftFunctor C a)] (M : CategoryTheory.Functor C (ModuleCat k)) [M.Additive] [CategoryTheory.Functor.Linear k M] (s : Finset A) : orbitPullupPushdown M ⟶ orbitPullupPushdownFiniteTranslate M s

Project the full direct sum onto a finite biproduct of translates.

noncomputable def MagnitudeConjecture.CoveringHom.orbitPullupPushdownFiniteRestriction {k : Type uK} [CommRing k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {A : Type w} [AddGroup A] [CategoryTheory.HasShift C A] [∀ (a : A), (CategoryTheory.shiftFunctor C a).Additive] [∀ (a : A), CategoryTheory.Functor.Linear k (CategoryTheory.shiftFunctor C a)] (M : CategoryTheory.Functor C (ModuleCat k)) [M.Additive] [CategoryTheory.Functor.Linear k M] (s : Finset A) (p : orbitPullupPushdown M ⟶ orbitPullupPushdown M) : orbitPullupPushdownFiniteTranslate M s ⟶ orbitPullupPushdownFiniteTranslate M s

The finite square matrix obtained by restricting an endomorphism of the full translate sum to a finite set of rows and columns.

theorem MagnitudeConjecture.CoveringHom.orbitPullupPushdownFiniteRestriction_component {k : Type uK} [CommRing k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {A : Type w} [AddGroup A] [CategoryTheory.HasShift C A] [∀ (a : A), (CategoryTheory.shiftFunctor C a).Additive] [∀ (a : A), CategoryTheory.Functor.Linear k (CategoryTheory.shiftFunctor C a)] (M : CategoryTheory.Functor C (ModuleCat k)) [M.Additive] [CategoryTheory.Functor.Linear k M] (s : Finset A) (p : orbitPullupPushdown M ⟶ orbitPullupPushdown M) (b c : orbitPullupPushdownFiniteIndex s) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.ι (fun (i : orbitPullupPushdownFiniteIndex s) => orbitPullupPushdownTranslate M (orbitPullupPushdownFiniteLabel s i)) b) (CategoryTheory.CategoryStruct.comp (orbitPullupPushdownFiniteRestriction M s p) (CategoryTheory.Limits.biproduct.π (fun (i : orbitPullupPushdownFiniteIndex s) => orbitPullupPushdownTranslate M (orbitPullupPushdownFiniteLabel s i)) c)) = CategoryTheory.CategoryStruct.comp (orbitPullupPushdownTranslateLof M (orbitPullupPushdownFiniteLabel s b)) (CategoryTheory.CategoryStruct.comp p (orbitPullupPushdownTranslateComponent M (orbitPullupPushdownFiniteLabel s c)))

theorem MagnitudeConjecture.CoveringHom.orbitPullupPushdownFiniteRestriction_component_assoc {k : Type uK} [CommRing k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {A : Type w} [AddGroup A] [CategoryTheory.HasShift C A] [∀ (a : A), (CategoryTheory.shiftFunctor C a).Additive] [∀ (a : A), CategoryTheory.Functor.Linear k (CategoryTheory.shiftFunctor C a)] (M : CategoryTheory.Functor C (ModuleCat k)) [M.Additive] [CategoryTheory.Functor.Linear k M] (s : Finset A) (p : orbitPullupPushdown M ⟶ orbitPullupPushdown M) (b c : orbitPullupPushdownFiniteIndex s) {Z : CategoryTheory.Functor C (ModuleCat k)} (h : orbitPullupPushdownTranslate M (orbitPullupPushdownFiniteLabel s c) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.ι (fun (i : orbitPullupPushdownFiniteIndex s) => orbitPullupPushdownTranslate M (orbitPullupPushdownFiniteLabel s i)) b) (CategoryTheory.CategoryStruct.comp (orbitPullupPushdownFiniteRestriction M s p) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.π (fun (i : orbitPullupPushdownFiniteIndex s) => orbitPullupPushdownTranslate M (orbitPullupPushdownFiniteLabel s i)) c) h)) = CategoryTheory.CategoryStruct.comp (orbitPullupPushdownTranslateLof M (orbitPullupPushdownFiniteLabel s b)) (CategoryTheory.CategoryStruct.comp p (CategoryTheory.CategoryStruct.comp (orbitPullupPushdownTranslateComponent M (orbitPullupPushdownFiniteLabel s c)) h))

theorem MagnitudeConjecture.CoveringHom.orbitPullupPushdownFiniteRestriction_isIso {k : Type uK} [CommRing k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {A : Type w} [AddGroup A] [CategoryTheory.HasShift C A] [∀ (a : A), (CategoryTheory.shiftFunctor C a).Additive] [∀ (a : A), CategoryTheory.Functor.Linear k (CategoryTheory.shiftFunctor C a)] (M : CategoryTheory.Functor C (ModuleCat k)) [M.Additive] [CategoryTheory.Functor.Linear k M] (s : Finset A) (p : orbitPullupPushdown M ⟶ orbitPullupPushdown M) (hindecomp : ∀ (b : A), CategoryTheory.Indecomposable (orbitPullupPushdownTranslate M b)) (hlocal : ∀ (b : A), IsLocalRing (CategoryTheory.End (orbitPullupPushdownTranslate M b))) (hpair : ∀ (b c : A), b ≠ c → ¬Nonempty (orbitPullupPushdownTranslate M b ≅ orbitPullupPushdownTranslate M c)) (hdiag : ∀ (b : A), CategoryTheory.IsIso (CategoryTheory.CategoryStruct.comp (orbitPullupPushdownTranslateLof M b) (CategoryTheory.CategoryStruct.comp p (orbitPullupPushdownTranslateComponent M b)))) : CategoryTheory.IsIso (orbitPullupPushdownFiniteRestriction M s p)

The finite restriction has invertible diagonal, hence is invertible.

theorem MagnitudeConjecture.CoveringHom.orbitPullupPushdownFiniteProject_include_apply_support {k : Type uK} [CommRing k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {A : Type w} [AddGroup A] [CategoryTheory.HasShift C A] [∀ (a : A), (CategoryTheory.shiftFunctor C a).Additive] [∀ (a : A), CategoryTheory.Functor.Linear k (CategoryTheory.shiftFunctor C a)] (M : CategoryTheory.Functor C (ModuleCat k)) [M.Additive] [CategoryTheory.Functor.Linear k M] (s : Finset A) (X : C) (x : orbitPushdownValue M X) (hx : ∀ b ∉ s, x b = 0) : (ModuleCat.Hom.hom ((CategoryTheory.CategoryStruct.comp (orbitPullupPushdownFiniteProject M s) (orbitPullupPushdownFiniteInclude M s)).app X)) x = x

Projecting an element onto the finite biproduct indexed by its support and then including it again recovers the element.

theorem MagnitudeConjecture.CoveringHom.orbitPullupPushdown_idempotent_eq_id_of_diagonal_isIso {k : Type uK} [CommRing k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {A : Type w} [AddGroup A] [CategoryTheory.HasShift C A] [∀ (a : A), (CategoryTheory.shiftFunctor C a).Additive] [∀ (a : A), CategoryTheory.Functor.Linear k (CategoryTheory.shiftFunctor C a)] (M : CategoryTheory.Functor C (ModuleCat k)) [M.Additive] [CategoryTheory.Functor.Linear k M] (p : orbitPullupPushdown M ⟶ orbitPullupPushdown M) (hp : CategoryTheory.CategoryStruct.comp p p = p) (hindecomp : ∀ (b : A), CategoryTheory.Indecomposable (orbitPullupPushdownTranslate M b)) (hlocal : ∀ (b : A), IsLocalRing (CategoryTheory.End (orbitPullupPushdownTranslate M b))) (hpair : ∀ (b c : A), b ≠ c → ¬Nonempty (orbitPullupPushdownTranslate M b ≅ orbitPullupPushdownTranslate M c)) (hdiag : ∀ (b : A), CategoryTheory.IsIso (CategoryTheory.CategoryStruct.comp (orbitPullupPushdownTranslateLof M b) (CategoryTheory.CategoryStruct.comp p (orbitPullupPushdownTranslateComponent M b)))) : p = CategoryTheory.CategoryStruct.id (orbitPullupPushdown M)

An idempotent on the explicit translate direct sum is the identity when all its diagonal components are invertible.

theorem MagnitudeConjecture.CoveringHom.orbitPullupPushdown_isIso_of_retraction_of_diagonal_isIso {k : Type uK} [CommRing k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {A : Type w} [AddGroup A] [CategoryTheory.HasShift C A] [∀ (a : A), (CategoryTheory.shiftFunctor C a).Additive] [∀ (a : A), CategoryTheory.Functor.Linear k (CategoryTheory.shiftFunctor C a)] (M : CategoryTheory.Functor C (ModuleCat k)) [M.Additive] [CategoryTheory.Functor.Linear k M] {L : CategoryTheory.Functor C (ModuleCat k)} (j : L ⟶ orbitPullupPushdown M) (r : orbitPullupPushdown M ⟶ L) (hjr : CategoryTheory.CategoryStruct.comp j r = CategoryTheory.CategoryStruct.id L) (hindecomp : ∀ (b : A), CategoryTheory.Indecomposable (orbitPullupPushdownTranslate M b)) (hlocal : ∀ (b : A), IsLocalRing (CategoryTheory.End (orbitPullupPushdownTranslate M b))) (hpair : ∀ (b c : A), b ≠ c → ¬Nonempty (orbitPullupPushdownTranslate M b ≅ orbitPullupPushdownTranslate M c)) (hdiag : ∀ (b : A), CategoryTheory.IsIso (CategoryTheory.CategoryStruct.comp (orbitPullupPushdownTranslateLof M b) (CategoryTheory.CategoryStruct.comp r (CategoryTheory.CategoryStruct.comp j (orbitPullupPushdownTranslateComponent M b))))) : CategoryTheory.IsIso j

A retract of the translate direct sum is the whole direct sum when the associated projector has invertible diagonal components.

theorem MagnitudeConjecture.CoveringHom.orbitPullupPushdown_one_retract_inclusion_isIso_of_invariant_diagonal {k : Type uK} [CommRing k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {A : Type w} [AddGroup A] [CategoryTheory.HasShift C A] [∀ (a : A), (CategoryTheory.shiftFunctor C a).Additive] [∀ (a : A), CategoryTheory.Functor.Linear k (CategoryTheory.shiftFunctor C a)] (M : CategoryTheory.Functor C (ModuleCat k)) [M.Additive] [CategoryTheory.Functor.Linear k M] {L Q : CategoryTheory.Functor C (ModuleCat k)} (j : L ⟶ orbitPullupPushdown M) (r : orbitPullupPushdown M ⟶ L) (hjr : CategoryTheory.CategoryStruct.comp j r = CategoryTheory.CategoryStruct.id L) (j' : Q ⟶ orbitPullupPushdown M) (r' : orbitPullupPushdown M ⟶ Q) (hj'r' : CategoryTheory.CategoryStruct.comp j' r' = CategoryTheory.CategoryStruct.id Q) (htotal : CategoryTheory.CategoryStruct.comp r j + CategoryTheory.CategoryStruct.comp r' j' = CategoryTheory.CategoryStruct.id (orbitPullupPushdown M)) (hindecomp : ∀ (b : A), CategoryTheory.Indecomposable (orbitPullupPushdownTranslate M b)) (hlocal : ∀ (b : A), IsLocalRing (CategoryTheory.End (orbitPullupPushdownTranslate M b))) (hpair : ∀ (b c : A), b ≠ c → ¬Nonempty (orbitPullupPushdownTranslate M b ≅ orbitPullupPushdownTranslate M c)) (hinvariant : ∀ (a b : A), CategoryTheory.IsIso (CategoryTheory.CategoryStruct.comp (orbitPullupPushdownTranslateLof M b) (CategoryTheory.CategoryStruct.comp r (CategoryTheory.CategoryStruct.comp j (orbitPullupPushdownTranslateComponent M b)))) ↔ CategoryTheory.IsIso (CategoryTheory.CategoryStruct.comp (orbitPullupPushdownTranslateLof M (a + b)) (CategoryTheory.CategoryStruct.comp r (CategoryTheory.CategoryStruct.comp j (orbitPullupPushdownTranslateComponent M (a + b)))))) : CategoryTheory.IsIso j ∨ CategoryTheory.IsIso j'

Explicit-retraction form of the invariant-summand theorem. This form is stable under applying a functor because it retains the chosen complementary projectors rather than asking IsSplitMono to choose new retractions.