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 MBDVendor.Magnitude.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 : QSE.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 MBDVendor.Magnitude.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 : QSE.Iyama.FiniteRightTauCategoryData C Ind) (X : Ind) : Function.Surjective ⇑(algebraicallyClosedResidueMap T X)

theorem MBDVendor.Magnitude.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 : QSE.Iyama.FiniteRightTauCategoryData C Ind) (X : Ind) (f : T.obj X ⟶ T.obj X) : f ∈ (algebraicallyClosedResidueMap T X).ker ↔ ¬IsUnit (CategoryTheory.End.of f)

theorem MBDVendor.Magnitude.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 : QSE.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 MBDVendor.Magnitude.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 : QSE.Iyama.FiniteRightTauCategoryData C Ind) : ResidueFieldData T

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

theorem MBDVendor.Magnitude.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 : QSE.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.