Residue-field discharge for the Hom--mesh recurrence

This file reduces the residue-dimension equation to a concrete residue map on each chosen indecomposable endomorphism ring. The off-diagonal assertion is proved from the finite Krull--Schmidt skeleton itself: a morphism between two distinct skeletal indecomposables cannot be split monic and is therefore categorically radical.

The remaining module-theoretic input is a surjective linear residue map End(X) -> k whose kernel is the categorical radical. Rank-nullity then gives codimension one on the diagonal.

theorem MagnitudeConjecture.FiniteTauMatrix.isIso_of_isSplitMono_obj_obj {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.IsIdempotentComplete C] {Ind : Type w} [Fintype Ind] (T : QuotientSubmoduleEquidistribution.Iyama.FiniteRightTauCategoryData C Ind) {p q : Ind} (f : T.obj p ⟶ T.obj q) [CategoryTheory.IsSplitMono f] : CategoryTheory.IsIso f

A split monomorphism between two chosen indecomposable representatives is an isomorphism.

theorem MagnitudeConjecture.FiniteTauMatrix.isRadicalMorphism_obj_obj_of_ne {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.IsIdempotentComplete C] {Ind : Type w} [Fintype Ind] (T : QuotientSubmoduleEquidistribution.Iyama.FiniteRightTauCategoryData C Ind) {X Y : Ind} (hXY : X ≠ Y) (f : T.obj X ⟶ T.obj Y) : QuotientSubmoduleEquidistribution.CategoricalRadical.IsRadicalMorphism f

Every morphism between two distinct chosen skeletal indecomposables is categorically radical.

structure MagnitudeConjecture.FiniteTauMatrix.ResidueFieldData {k : Type s} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.IsIdempotentComplete C] [CategoryTheory.Linear k C] {Ind : Type w} [Fintype Ind] (T : QuotientSubmoduleEquidistribution.Iyama.FiniteRightTauCategoryData C Ind) : Type (max (max s v) w)

Concrete residue-field data on the chosen indecomposable endomorphism rings. In the module-category specialization this is obtained from the finite-dimensional local endomorphism algebra over an algebraically closed field.

• residueMap (X : Ind) : (T.obj X ⟶ T.obj X) →ₗ[k] k
• residueMap_surjective (X : Ind) : Function.Surjective ⇑(self.residueMap X)
• radical_eq_ker (X : Ind) : CategoryTheory.radicalSubmodule k (T.obj X) (T.obj X) = (self.residueMap X).ker

theorem MagnitudeConjecture.FiniteTauMatrix.radical_finrank_add_one_eq_end {k : Type s} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.IsIdempotentComplete C] [CategoryTheory.Linear k C] [∀ (X Y : C), FiniteDimensional k (X ⟶ Y)] {Ind : Type w} [Fintype Ind] (T : QuotientSubmoduleEquidistribution.Iyama.FiniteRightTauCategoryData C Ind) (R : ResidueFieldData T) (X : Ind) : Module.finrank k ↥(CategoryTheory.radicalSubmodule k (T.obj X) (T.obj X)) + 1 = Module.finrank k (T.obj X ⟶ T.obj X)

theorem MagnitudeConjecture.FiniteTauMatrix.radicalFinrank_add_delta {k : Type s} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.IsIdempotentComplete C] [CategoryTheory.Linear k C] [∀ (X Y : C), FiniteDimensional k (X ⟶ Y)] {Ind : Type w} [Fintype Ind] [DecidableEq Ind] (T : QuotientSubmoduleEquidistribution.Iyama.FiniteRightTauCategoryData C Ind) (R : ResidueFieldData T) (X Y : Ind) : (Module.finrank k ↥(CategoryTheory.radicalSubmodule k (T.obj X) (T.obj Y)) + if X = Y then 1 else 0) = Module.finrank k (T.obj X ⟶ T.obj Y)

The residue maps imply the exact diagonal/off-diagonal dimension formula used by the Hom--mesh inverse theorem.

theorem MagnitudeConjecture.FiniteTauMatrix.HomMeshInverseData.ofResidue {k : Type s} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.IsIdempotentComplete C] [CategoryTheory.Linear k C] [∀ (X Y : C), FiniteDimensional k (X ⟶ Y)] {Ind : Type w} [Fintype Ind] [DecidableEq Ind] (T : QuotientSubmoduleEquidistribution.Iyama.FiniteTauCategoryData C Ind) (rightMono : ∀ (Y : Ind), CategoryTheory.Mono (T.rightMesh (T.obj Y)).f) (R : ResidueFieldData T.toFiniteRightTauCategoryData) : HomMeshInverseData T

Strictness together with concrete residue maps constructs all hypotheses of the Hom--mesh inverse theorem.