Nilpotent categorical traces from the factorial obstruction #
The permutation action and scalar cycle-trace formula of an object
form a CycleTraceTower. Schrijver's factorial obstruction gives
nilpotent-trace vanishing from a single tensor level of dimension
less than n!, and hence from exponential endomorphism growth.
The Frobenius and trace-zeta route is retained in ObjectTower.
noncomputable def
RS.objectCycleTraceTower
{A : Type u}
[CategoryTheory.Category.{v, u} A]
[CategoryTheory.MonoidalCategory A]
[CategoryTheory.SymmetricCategory A]
[CategoryTheory.Preadditive A]
[CategoryTheory.Linear ℂ A]
[CategoryTheory.MonoidalPreadditive A]
[CategoryTheory.MonoidalLinear ℂ A]
[CategoryTheory.RigidCategory A]
(hu : HasScalarUnit A)
(X : A)
:
CycleTraceTower (fun (n : ℕ) => CategoryTheory.End (tensorPow A X n)) (CategoryTheory.End X)
The cycle-trace tower of an object, with no growth assumption.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
RS.factorial_le_finrank_of_nonzero_nilpotent_trace
{A : Type u}
[CategoryTheory.Category.{v, u} A]
[CategoryTheory.MonoidalCategory A]
[CategoryTheory.SymmetricCategory A]
[CategoryTheory.Preadditive A]
[CategoryTheory.Linear ℂ A]
[CategoryTheory.MonoidalPreadditive A]
[CategoryTheory.MonoidalLinear ℂ A]
[CategoryTheory.RigidCategory A]
(hu : HasScalarUnit A)
(X : A)
{g : CategoryTheory.End X}
(hg : IsNilpotent g)
(hτ : (scalarTrace hu X) g ≠ 0)
(n : ℕ)
[Module.Finite ℂ (CategoryTheory.End (tensorPow A X n))]
:
A nonzero nilpotent trace forces factorial dimension at every finite-dimensional tensor level.
theorem
RS.scalarTrace_eq_zero_of_finrank_lt_factorial
{A : Type u}
[CategoryTheory.Category.{v, u} A]
[CategoryTheory.MonoidalCategory A]
[CategoryTheory.SymmetricCategory A]
[CategoryTheory.Preadditive A]
[CategoryTheory.Linear ℂ A]
[CategoryTheory.MonoidalPreadditive A]
[CategoryTheory.MonoidalLinear ℂ A]
[CategoryTheory.RigidCategory A]
(hu : HasScalarUnit A)
(X : A)
{n : ℕ}
[Module.Finite ℂ (CategoryTheory.End (tensorPow A X n))]
(hbound : Module.finrank ℂ (CategoryTheory.End (tensorPow A X n)) < n.factorial)
{g : CategoryTheory.End X}
(hg : IsNilpotent g)
:
One tensor level of dimension less than its factorial suffices for nilpotent categorical traces to vanish.
theorem
RS.scalarTrace_eq_zero_of_isNilpotent_factorial
{A : Type u}
[CategoryTheory.Category.{v, u} A]
[CategoryTheory.MonoidalCategory A]
[CategoryTheory.SymmetricCategory A]
[CategoryTheory.Preadditive A]
[CategoryTheory.Linear ℂ A]
[CategoryTheory.MonoidalPreadditive A]
[CategoryTheory.MonoidalLinear ℂ A]
[CategoryTheory.RigidCategory A]
(hu : HasScalarUnit A)
(X : A)
[∀ (n : ℕ), Module.Finite ℂ (CategoryTheory.End (tensorPow A X n))]
(B : ℝ)
(hbound : ∀ (n : ℕ), ↑(Module.finrank ℂ (CategoryTheory.End (tensorPow A X n))) ≤ B ^ n)
{g : CategoryTheory.End X}
(hg : IsNilpotent g)
:
The factorial proof of nilpotent categorical trace vanishing under exponential endomorphism growth.