The nilpotent leg of the matrix-envelope trace

Nilpotent endomorphisms of matrix-envelope objects have vanishing diagonal trace. The argument stays inside the original endomorphism algebra: the atomic idempotent decompositions of each entry algebra split the trace into atom-level diagonal entries; the scalar matrix extracted through chosen iso-class representatives multiplies like the endomorphism (idempotent insertion), is supported on class blocks (the dichotomy), and inherits nilpotency — so each class block has vanishing complex trace, and the diagonal trace is the class-weighted sum of those.

Trace splitting along a complete orthogonal family

theorem RS.karoubiTrace_split {R : ℕ} (f : EdgeRankParameter R) {X : CategoryTheory.Idempotents.Karoubi (SkeinObj f)} {ι : Type} [Fintype ι] (e : ι → CategoryTheory.End X) (hco : CompleteOrthogonalIdempotents e) (x : CategoryTheory.End X) : (HomSpace.traceMap f.val X.X.arity) x.f = ∑ a : ι, (HomSpace.traceMap f.val X.X.arity) (CategoryTheory.CategoryStruct.comp (e a).f (CategoryTheory.CategoryStruct.comp x.f (e a).f))

The trace splits along a complete orthogonal idempotent family: tr x = ∑ₐ tr (eₐ x eₐ).

Atom resolutions

structure RS.AtomResolution {R : ℕ} (f : EdgeRankParameter R) (M : CategoryTheory.Mat_ (CategoryTheory.Idempotents.Karoubi (SkeinObj f))) : Type 1

A choice of atomic idempotent decompositions for every entry of a matrix-envelope object.

• idx : M.ι → Type

  The atom index of each entry.

• fin (i : M.ι) : Fintype (self.idx i)

  Finiteness.

• e (i : M.ι) : self.idx i → CategoryTheory.End (M.X i)

  The idempotent families.

• complete (i : M.ι) : CompleteOrthogonalIdempotents (self.e i)

  Complete orthogonality.

• atomic (i : M.ι) (a : self.idx i) : IsAtomicIdempotent (self.e i a)

  Atomicity.

noncomputable def RS.atomResolution {R : ℕ} (f : EdgeRankParameter R) (M : CategoryTheory.Mat_ (CategoryTheory.Idempotents.Karoubi (SkeinObj f))) : AtomResolution f M

Atom resolutions exist.

Equations

• One or more equations did not get rendered due to their size.

theorem RS.matTrace_resolution {R : ℕ} (f : EdgeRankParameter R) {M : CategoryTheory.Mat_ (CategoryTheory.Idempotents.Karoubi (SkeinObj f))} (A : AtomResolution f M) (φ : CategoryTheory.End M) : (matTrace f M) φ = ∑ i : M.ι, ∑ a : A.idx i, (HomSpace.traceMap f.val (M.X i).X.arity) (CategoryTheory.CategoryStruct.comp (A.e i a).f (CategoryTheory.CategoryStruct.comp (φ i i).f (A.e i a).f))

The diagonal trace refined along an atom resolution.

The atoms of a resolution

@[reducible]

def RS.AtomResolution.κ {R : ℕ} {f : EdgeRankParameter R} {M : CategoryTheory.Mat_ (CategoryTheory.Idempotents.Karoubi (SkeinObj f))} (A : AtomResolution f M) : Type

The total atom index.

Equations

• A.κ = ((i : M.ι) × A.idx i)

@[reducible]

noncomputable def RS.AtomResolution.S {R : ℕ} {f : EdgeRankParameter R} {M : CategoryTheory.Mat_ (CategoryTheory.Idempotents.Karoubi (SkeinObj f))} (A : AtomResolution f M) (p : A.κ) : CategoryTheory.Idempotents.Karoubi (SkeinObj f)

The atom at a total index.

Equations

• A.S p = RS.cutBy f (M.X p.fst) ⋯

theorem RS.AtomResolution.isAtom_S {R : ℕ} {f : EdgeRankParameter R} {M : CategoryTheory.Mat_ (CategoryTheory.Idempotents.Karoubi (SkeinObj f))} (A : AtomResolution f M) (p : A.κ) : IsAtom f (A.S p)

The atoms are atoms.

Scalar extraction on atoms

noncomputable def RS.atomScalar {R : ℕ} {f : EdgeRankParameter R} {S : CategoryTheory.Idempotents.Karoubi (SkeinObj f)} (hS : IsAtom f S) (x : CategoryTheory.End S) : ℂ

The scalar of an atom endomorphism.

Equations

• RS.atomScalar hS x = Classical.choose ⋯

theorem RS.atomScalar_spec {R : ℕ} {f : EdgeRankParameter R} {S : CategoryTheory.Idempotents.Karoubi (SkeinObj f)} (hS : IsAtom f S) (x : CategoryTheory.End S) : x = atomScalar hS x • CategoryTheory.CategoryStruct.id S

The extracted scalar does what it says: the endomorphism is that multiple of the identity.

theorem RS.atomScalar_unique {R : ℕ} {f : EdgeRankParameter R} {S : CategoryTheory.Idempotents.Karoubi (SkeinObj f)} (hS : IsAtom f S) {x : CategoryTheory.End S} {c : ℂ} (h : x = c • CategoryTheory.CategoryStruct.id S) : atomScalar hS x = c

The scalar is unique — an atom's identity is nonzero.

theorem RS.atomScalar_add {R : ℕ} {f : EdgeRankParameter R} {S : CategoryTheory.Idempotents.Karoubi (SkeinObj f)} (hS : IsAtom f S) (x y : CategoryTheory.End S) : atomScalar hS (x + y) = atomScalar hS x + atomScalar hS y

Extraction is additive.

theorem RS.atomScalar_comp {R : ℕ} {f : EdgeRankParameter R} {S : CategoryTheory.Idempotents.Karoubi (SkeinObj f)} (hS : IsAtom f S) (x y : CategoryTheory.End S) : atomScalar hS (CategoryTheory.CategoryStruct.comp x y) = atomScalar hS x * atomScalar hS y

Extraction is multiplicative: composition of atom endomorphisms is multiplication of scalars. This is what lets the scalar matrix inherit nilpotency.

The class structure

noncomputable def RS.AtomResolution.rel {R : ℕ} {f : EdgeRankParameter R} {M : CategoryTheory.Mat_ (CategoryTheory.Idempotents.Karoubi (SkeinObj f))} (A : AtomResolution f M) (p q : A.κ) : Prop

Atoms are related when isomorphic.

Equations

• A.rel p q = Nonempty (A.S p ≅ A.S q)

theorem RS.AtomResolution.rel_refl {R : ℕ} {f : EdgeRankParameter R} {M : CategoryTheory.Mat_ (CategoryTheory.Idempotents.Karoubi (SkeinObj f))} (A : AtomResolution f M) (p : A.κ) : A.rel p p

Isomorphism of atoms is reflexive.

theorem RS.AtomResolution.rel_symm {R : ℕ} {f : EdgeRankParameter R} {M : CategoryTheory.Mat_ (CategoryTheory.Idempotents.Karoubi (SkeinObj f))} (A : AtomResolution f M) {p q : A.κ} (h : A.rel p q) : A.rel q p

It is symmetric.

theorem RS.AtomResolution.rel_trans {R : ℕ} {f : EdgeRankParameter R} {M : CategoryTheory.Mat_ (CategoryTheory.Idempotents.Karoubi (SkeinObj f))} (A : AtomResolution f M) {p q r : A.κ} (h : A.rel p q) (h' : A.rel q r) : A.rel p r

It is transitive.

@[instance_reducible]

noncomputable instance RS.AtomResolution.relDec {R : ℕ} {f : EdgeRankParameter R} {M : CategoryTheory.Mat_ (CategoryTheory.Idempotents.Karoubi (SkeinObj f))} (A : AtomResolution f M) (p q : A.κ) : Decidable (A.rel p q)

A fixed decidability instance, so all filters elaborate uniformly.

Equations

• A.relDec p q = Classical.dec (A.rel p q)

Representatives and chosen isomorphisms

noncomputable def RS.AtomResolution.rep {R : ℕ} {f : EdgeRankParameter R} {M : CategoryTheory.Mat_ (CategoryTheory.Idempotents.Karoubi (SkeinObj f))} (A : AtomResolution f M) (p : A.κ) : A.κ

The class representative: the enumeration-minimal related index.

Equations

• A.rep p = (Fintype.equivFin A.κ).symm ((Finset.image ⇑(Fintype.equivFin A.κ) {q : A.κ | A.rel p q}).min' ⋯)

theorem RS.AtomResolution.rel_rep {R : ℕ} {f : EdgeRankParameter R} {M : CategoryTheory.Mat_ (CategoryTheory.Idempotents.Karoubi (SkeinObj f))} (A : AtomResolution f M) (p : A.κ) : A.rel p (A.rep p)

An atom is isomorphic to its class representative.

theorem RS.AtomResolution.rep_eq_of_rel {R : ℕ} {f : EdgeRankParameter R} {M : CategoryTheory.Mat_ (CategoryTheory.Idempotents.Karoubi (SkeinObj f))} (A : AtomResolution f M) {p q : A.κ} (h : A.rel p q) : A.rep p = A.rep q

Isomorphic atoms have the same representative.

noncomputable def RS.AtomResolution.w {R : ℕ} {f : EdgeRankParameter R} {M : CategoryTheory.Mat_ (CategoryTheory.Idempotents.Karoubi (SkeinObj f))} (A : AtomResolution f M) (p : A.κ) : A.S (A.rep p) ≅ A.S p

The chosen isomorphism from the representative atom.

Equations

• A.w p = Nonempty.some ⋯

The matrix elements

noncomputable def RS.AtomResolution.t {R : ℕ} {f : EdgeRankParameter R} {M : CategoryTheory.Mat_ (CategoryTheory.Idempotents.Karoubi (SkeinObj f))} (A : AtomResolution f M) (φ : CategoryTheory.End M) (p q : A.κ) : A.S p ⟶ A.S q

The matrix element of an endomorphism at a pair of atoms.

Equations

• A.t φ p q = { f := CategoryTheory.CategoryStruct.comp (A.e p.fst p.snd).f (CategoryTheory.CategoryStruct.comp (φ p.fst q.fst).f (A.e q.fst q.snd).f), comm := ⋯ }

theorem RS.AtomResolution.t_f {R : ℕ} {f : EdgeRankParameter R} {M : CategoryTheory.Mat_ (CategoryTheory.Idempotents.Karoubi (SkeinObj f))} (A : AtomResolution f M) (φ : CategoryTheory.End M) (p q : A.κ) : (A.t φ p q).f = CategoryTheory.CategoryStruct.comp (A.e p.fst p.snd).f (CategoryTheory.CategoryStruct.comp (φ p.fst q.fst).f (A.e q.fst q.snd).f)

The matrix element's underlying morphism: the entry cut down by the two atoms' idempotents.

theorem RS.AtomResolution.t_eq_zero {R : ℕ} {f : EdgeRankParameter R} {M : CategoryTheory.Mat_ (CategoryTheory.Idempotents.Karoubi (SkeinObj f))} (A : AtomResolution f M) (φ : CategoryTheory.End M) {p q : A.κ} (h : ¬A.rel p q) : A.t φ p q = 0

Cross-class matrix elements vanish (the dichotomy).

theorem RS.AtomResolution.t_comp {R : ℕ} {f : EdgeRankParameter R} {M : CategoryTheory.Mat_ (CategoryTheory.Idempotents.Karoubi (SkeinObj f))} (A : AtomResolution f M) (φ ψ : CategoryTheory.End M) (p r : A.κ) : A.t (CategoryTheory.CategoryStruct.comp φ ψ) p r = ∑ q : A.κ, CategoryTheory.CategoryStruct.comp (A.t φ p q) (A.t ψ q r)

Multiplicativity of the matrix elements: idempotent insertion turns the composite's elements into the matrix product of elements.

The scalar matrix

theorem RS.atomScalar_eqToHom_conj {R : ℕ} {f : EdgeRankParameter R} {S T : CategoryTheory.Idempotents.Karoubi (SkeinObj f)} (h : S = T) (hS : IsAtom f S) (hT : IsAtom f T) (z : CategoryTheory.End T) : atomScalar hS (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom h) (CategoryTheory.CategoryStruct.comp z (CategoryTheory.eqToHom ⋯))) = atomScalar hT z

Scalars are invariant under object-equality transport.

noncomputable def RS.AtomResolution.B {R : ℕ} {f : EdgeRankParameter R} {M : CategoryTheory.Mat_ (CategoryTheory.Idempotents.Karoubi (SkeinObj f))} (A : AtomResolution f M) (φ : CategoryTheory.End M) : Matrix A.κ A.κ ℂ

The scalar matrix of an endomorphism over the atoms.

Equations

• One or more equations did not get rendered due to their size.

theorem RS.AtomResolution.B_apply_of_ne {R : ℕ} {f : EdgeRankParameter R} {M : CategoryTheory.Mat_ (CategoryTheory.Idempotents.Karoubi (SkeinObj f))} (A : AtomResolution f M) (φ : CategoryTheory.End M) {p q : A.κ} (h : ¬A.rep p = A.rep q) : A.B φ p q = 0

The dichotomy: the scalar matrix vanishes off the class blocks, there being no isomorphism to transport along.

theorem RS.AtomResolution.B_zero {R : ℕ} {f : EdgeRankParameter R} {M : CategoryTheory.Mat_ (CategoryTheory.Idempotents.Karoubi (SkeinObj f))} (A : AtomResolution f M) : A.B 0 = 0

The scalar matrix of the zero endomorphism is zero.

theorem RS.AtomResolution.B_comp {R : ℕ} {f : EdgeRankParameter R} {M : CategoryTheory.Mat_ (CategoryTheory.Idempotents.Karoubi (SkeinObj f))} (A : AtomResolution f M) (φ ψ : CategoryTheory.End M) : A.B (CategoryTheory.CategoryStruct.comp φ ψ) = A.B φ * A.B ψ

Multiplicativity of the scalar matrix.

@[instance_reducible]

noncomputable instance RS.AtomResolution.kappaDec {R : ℕ} {f : EdgeRankParameter R} {M : CategoryTheory.Mat_ (CategoryTheory.Idempotents.Karoubi (SkeinObj f))} (A : AtomResolution f M) : DecidableEq A.κ

The total atom index has decidable equality, classically.

Equations

• A.kappaDec = Classical.decEq A.κ

theorem RS.AtomResolution.B_pow {R : ℕ} {f : EdgeRankParameter R} {M : CategoryTheory.Mat_ (CategoryTheory.Idempotents.Karoubi (SkeinObj f))} (A : AtomResolution f M) (φ : CategoryTheory.End M) (k : ℕ) : A.B (φ ^ (k + 1)) = A.B φ ^ (k + 1)

Powers transport to matrix powers.

theorem RS.AtomResolution.trace_t_diag {R : ℕ} {f : EdgeRankParameter R} {M : CategoryTheory.Mat_ (CategoryTheory.Idempotents.Karoubi (SkeinObj f))} (A : AtomResolution f M) (φ : CategoryTheory.End M) (p : A.κ) : (HomSpace.traceMap f.val (M.X p.fst).X.arity) (A.t φ p p).f = A.B φ p p * (HomSpace.traceMap f.val (M.X (A.rep p).fst).X.arity) (CategoryTheory.CategoryStruct.id (A.S (A.rep p))).f

The diagonal scalar recovers the diagonal trace entry, up to the class weight.

Class-block restriction

theorem RS.AtomResolution.B_support {R : ℕ} {f : EdgeRankParameter R} {M : CategoryTheory.Mat_ (CategoryTheory.Idempotents.Karoubi (SkeinObj f))} (A : AtomResolution f M) (φ : CategoryTheory.End M) {p q : A.κ} (h : A.B φ p q ≠ 0) : A.rep p = A.rep q

The scalar matrix is supported on class blocks.

noncomputable def RS.AtomResolution.restrict {R : ℕ} {f : EdgeRankParameter R} {M : CategoryTheory.Mat_ (CategoryTheory.Idempotents.Karoubi (SkeinObj f))} (A : AtomResolution f M) (c : A.κ) (X : Matrix A.κ A.κ ℂ) : Matrix { p : A.κ // A.rep p = c } { p : A.κ // A.rep p = c } ℂ

The class-block restriction of a matrix.

Equations

• A.restrict c X p q = X ↑p ↑q

theorem RS.AtomResolution.support_mul {R : ℕ} {f : EdgeRankParameter R} {M : CategoryTheory.Mat_ (CategoryTheory.Idempotents.Karoubi (SkeinObj f))} (A : AtomResolution f M) (X Y : Matrix A.κ A.κ ℂ) (hX : ∀ (p q : A.κ), X p q ≠ 0 → A.rep p = A.rep q) (hY : ∀ (p q : A.κ), Y p q ≠ 0 → A.rep p = A.rep q) (p q : A.κ) : (X * Y) p q ≠ 0 → A.rep p = A.rep q

Products preserve block support.

theorem RS.AtomResolution.restrict_mul {R : ℕ} {f : EdgeRankParameter R} {M : CategoryTheory.Mat_ (CategoryTheory.Idempotents.Karoubi (SkeinObj f))} (A : AtomResolution f M) (c : A.κ) (X Y : Matrix A.κ A.κ ℂ) (hX : ∀ (p q : A.κ), X p q ≠ 0 → A.rep p = A.rep q) : A.restrict c (X * Y) = A.restrict c X * A.restrict c Y

Restriction respects products of block-supported matrices.

theorem RS.AtomResolution.support_pow {R : ℕ} {f : EdgeRankParameter R} {M : CategoryTheory.Mat_ (CategoryTheory.Idempotents.Karoubi (SkeinObj f))} (A : AtomResolution f M) (X : Matrix A.κ A.κ ℂ) (hX : ∀ (p q : A.κ), X p q ≠ 0 → A.rep p = A.rep q) (k : ℕ) (p q : A.κ) : (X ^ (k + 1)) p q ≠ 0 → A.rep p = A.rep q

Powers preserve block support.

theorem RS.AtomResolution.restrict_pow {R : ℕ} {f : EdgeRankParameter R} {M : CategoryTheory.Mat_ (CategoryTheory.Idempotents.Karoubi (SkeinObj f))} (A : AtomResolution f M) (c : A.κ) (X : Matrix A.κ A.κ ℂ) (hX : ∀ (p q : A.κ), X p q ≠ 0 → A.rep p = A.rep q) (k : ℕ) : A.restrict c (X ^ (k + 1)) = A.restrict c X ^ (k + 1)

Restriction respects powers of block-supported matrices.

The nilpotent leg

noncomputable def RS.AtomResolution.δ {R : ℕ} {f : EdgeRankParameter R} {M : CategoryTheory.Mat_ (CategoryTheory.Idempotents.Karoubi (SkeinObj f))} (A : AtomResolution f M) (c : A.κ) : ℂ

The class weight: the closure trace of an atom identity.

Equations

• A.δ c = (RS.HomSpace.traceMap f.val (M.X c.fst).X.arity) (CategoryTheory.CategoryStruct.id (A.S c)).f

theorem RS.matTrace_eq_zero_of_isNilpotent' {R : ℕ} {f : EdgeRankParameter R} {M : CategoryTheory.Mat_ (CategoryTheory.Idempotents.Karoubi (SkeinObj f))} {φ : CategoryTheory.End M} (hφ : IsNilpotent φ) : (matTrace f M) φ = 0

The nilpotent leg: nilpotent matrix-envelope endomorphisms have vanishing diagonal trace.