Local residue of a shift-orbit endomorphism algebra

For an indecomposable object with trivial shift stabilizer, taking the ordinary degree-zero component of a finite-support shift-orbit endomorphism and then passing to the residue field is multiplicative. Products returning to degree zero through a nonzero shift factor through a nonisomorphic indecomposable and therefore have zero residue.

This is the local-algebra mechanism in Gabriel's assertion that a pushed endomorphism is nilpotent exactly when its identity component is nilpotent.

noncomputable def MagnitudeConjecture.CoveringHom.shiftOrbitResidueLinearMap {k : Type uK} [Field k] [IsAlgClosed 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] (X : C) [FiniteDimensional k (CategoryTheory.End X)] [IsLocalRing (CategoryTheory.End X)] : ShiftOrbitHom A X X →ₗ[k] k

The residue scalar of the ordinary degree-zero component of a shift-orbit endomorphism.

@[simp]

theorem MagnitudeConjecture.CoveringHom.shiftOrbitResidueLinearMap_of_ne {k : Type uK} [Field k] [IsAlgClosed 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] (X : C) [FiniteDimensional k (CategoryTheory.End X)] [IsLocalRing (CategoryTheory.End X)] {a : A} (ha : a ≠ 0) (f : ShiftHom X X a) : (shiftOrbitResidueLinearMap X) ((shiftOrbitOf X X a) f) = 0

@[simp]

theorem MagnitudeConjecture.CoveringHom.shiftOrbitResidueLinearMap_of_zero {k : Type uK} [Field k] [IsAlgClosed 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] (X : C) [FiniteDimensional k (CategoryTheory.End X)] [IsLocalRing (CategoryTheory.End X)] (f : ShiftHom X X 0) : (shiftOrbitResidueLinearMap X) ((shiftOrbitOf X X 0) f) = LocalAlgebraResidue.residueScalar k (CategoryTheory.End.of ((shiftHomZeroLinearEquiv X X).symm f))

theorem MagnitudeConjecture.CoveringHom.residueScalar_shiftHomComp'_eq_zero {k : Type uK} [Field k] [IsAlgClosed k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.IsIdempotentComplete C] {A : Type w} [AddGroup A] [CategoryTheory.HasShift C A] [∀ (a : A), (CategoryTheory.shiftFunctor C a).Additive] (X : C) [FiniteDimensional k (CategoryTheory.End X)] [IsLocalRing (CategoryTheory.End X)] (hX : CategoryTheory.Indecomposable X) (htrivial : ∀ (a : A), Nonempty (X ≅ (CategoryTheory.shiftFunctor C a).obj X) → a = 0) {a b : A} (ha : a ≠ 0) (hba : b + a = 0) (f : ShiftHom X X a) (g : ShiftHom X X b) : LocalAlgebraResidue.residueScalar k (CategoryTheory.End.of ((shiftHomZeroLinearEquiv X X).symm (shiftHomComp' hba f g))) = 0

A homogeneous product returning to degree zero through a nonzero shift has zero residue.

theorem MagnitudeConjecture.CoveringHom.shiftOrbitResidueLinearMap_comp_of_ne_of_add_eq_zero {k : Type uK} [Field k] [IsAlgClosed k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.IsIdempotentComplete C] {A : Type w} [AddGroup A] [CategoryTheory.HasShift C A] [∀ (a : A), (CategoryTheory.shiftFunctor C a).Additive] (X : C) [FiniteDimensional k (CategoryTheory.End X)] [IsLocalRing (CategoryTheory.End X)] (hX : CategoryTheory.Indecomposable X) (htrivial : ∀ (a : A), Nonempty (X ≅ (CategoryTheory.shiftFunctor C a).obj X) → a = 0) {a b : A} (ha : a ≠ 0) (hba : b + a = 0) (f : ShiftHom X X a) (g : ShiftHom X X b) : (shiftOrbitResidueLinearMap X) ((shiftOrbitOf X X (b + a)) (shiftHomComp f g)) = 0

The shift-orbit residue of a homogeneous product through a nonzero shift vanishes.

theorem MagnitudeConjecture.CoveringHom.shiftOrbitResidueLinearMap_comp {k : Type uK} [Field k] [IsAlgClosed k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.IsIdempotentComplete C] {A : Type w} [AddGroup A] [CategoryTheory.HasShift C A] [∀ (a : A), (CategoryTheory.shiftFunctor C a).Additive] (X : C) [FiniteDimensional k (CategoryTheory.End X)] [IsLocalRing (CategoryTheory.End X)] (hX : CategoryTheory.Indecomposable X) (htrivial : ∀ (a : A), Nonempty (X ≅ (CategoryTheory.shiftFunctor C a).obj X) → a = 0) (q r : ShiftOrbitHom A X X) : (shiftOrbitResidueLinearMap X) ((shiftOrbitCompHom q) r) = (shiftOrbitResidueLinearMap X) q * (shiftOrbitResidueLinearMap X) r

The degree-zero residue is multiplicative for shift-orbit convolution when the base object is indecomposable with trivial shift stabilizer.

theorem MagnitudeConjecture.CoveringHom.shiftOrbitResidueLinearMap_one {k : Type uK} [Field k] [IsAlgClosed 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] (X : C) [FiniteDimensional k (CategoryTheory.End X)] [IsLocalRing (CategoryTheory.End X)] : (shiftOrbitResidueLinearMap X) (shiftOrbitId X) = 1

The residue of the shift-orbit identity is one.

noncomputable def MagnitudeConjecture.CoveringHom.shiftOrbitResidueAlgHom {k : Type uK} [Field k] [IsAlgClosed k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.IsIdempotentComplete 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)] (X : C) [FiniteDimensional k (CategoryTheory.End X)] [IsLocalRing (CategoryTheory.End X)] (hX : CategoryTheory.Indecomposable X) (htrivial : ∀ (a : A), Nonempty (X ≅ (CategoryTheory.shiftFunctor C a).obj X) → a = 0) : CategoryTheory.End (have this := X; this) →ₐ[k] k

The degree-zero residue is a k-algebra homomorphism on the shift-orbit endomorphism ring.