Residue maps for chosen indecomposables over an algebraically closed field

The finite tau-category data already records that every chosen indecomposable has a local endomorphism ring. Over an algebraically closed field, the local algebra residue construction supplies its unique scalar residue map. The categorical radical criterion identifies the kernel with the diagonal categorical radical.

noncomputable def MagnitudeConjecture.FiniteTauMatrix.algebraicallyClosedResidueMap {k : Type s} [Field k] [IsAlgClosed 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) (X : Ind) : (T.obj X ⟶ T.obj X) →ₗ[k] k

The scalar residue map on the endomorphism algebra of a chosen indecomposable.

theorem MagnitudeConjecture.FiniteTauMatrix.algebraicallyClosedResidueMap_surjective {k : Type s} [Field k] [IsAlgClosed 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) (X : Ind) : Function.Surjective ⇑(algebraicallyClosedResidueMap T X)

theorem MagnitudeConjecture.FiniteTauMatrix.mem_ker_algebraicallyClosedResidueMap_iff_not_isUnit {k : Type s} [Field k] [IsAlgClosed 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) (X : Ind) (f : T.obj X ⟶ T.obj X) : f ∈ (algebraicallyClosedResidueMap T X).ker ↔ ¬IsUnit (CategoryTheory.End.of f)

theorem MagnitudeConjecture.FiniteTauMatrix.radicalSubmodule_eq_ker_algebraicallyClosedResidueMap {k : Type s} [Field k] [IsAlgClosed 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) (X : Ind) : CategoryTheory.radicalSubmodule k (T.obj X) (T.obj X) = (algebraicallyClosedResidueMap T X).ker

The concrete scalar residue map has the categorical radical as kernel.

noncomputable def MagnitudeConjecture.FiniteTauMatrix.ResidueFieldData.ofIsAlgClosed {k : Type s} [Field k] [IsAlgClosed 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) : ResidueFieldData T

Algebraic closedness automatically supplies all diagonal residue-field data required by the Hom--mesh inverse theorem.

theorem MagnitudeConjecture.FiniteTauMatrix.HomMeshInverseData.ofIsAlgClosed {k : Type s} [Field k] [IsAlgClosed 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) : HomMeshInverseData T

Over an algebraically closed field, right-mesh monicity is now the only remaining input to the Hom--mesh inverse package.