The Hom-dichotomy between atoms

An atom of the Karoubi envelope is an object whose endomorphisms are the scalar line of a nonzero identity. Between atoms, the mixed-trace nondegeneracy forces the dichotomy: every nonzero morphism composes with a partner to a nonzero scalar, hence is an isomorphism. This is the engine turning the atomic idempotent decomposition into a semisimple-category structure.

structure RS.IsAtom {R : ℕ} (f : EdgeRankParameter R) (S : CategoryTheory.Idempotents.Karoubi (SkeinObj f)) : Prop

An atom: the endomorphisms are scalars, and the identity is nonzero.

• scalar (x : CategoryTheory.End S) : ∃ (c : ℂ), x = c • CategoryTheory.CategoryStruct.id S
• id_ne_zero : CategoryTheory.CategoryStruct.id S ≠ 0

theorem RS.atom_iso_of_ne_zero {R : ℕ} (f : EdgeRankParameter R) {S T : CategoryTheory.Idempotents.Karoubi (SkeinObj f)} (hS : IsAtom f S) (hT : IsAtom f T) {φ : S ⟶ T} (hφ : φ ≠ 0) : ∃ (ψ : T ⟶ S), CategoryTheory.CategoryStruct.comp φ ψ = CategoryTheory.CategoryStruct.id S ∧ CategoryTheory.CategoryStruct.comp ψ φ = CategoryTheory.CategoryStruct.id T

The dichotomy: a nonzero morphism between atoms is an isomorphism.

Atoms from atomic idempotents

@[reducible]

noncomputable def RS.cutBy {R : ℕ} (f : EdgeRankParameter R) (X : CategoryTheory.Idempotents.Karoubi (SkeinObj f)) {eK : CategoryTheory.End X} (he : IsIdempotentElem eK) : CategoryTheory.Idempotents.Karoubi (SkeinObj f)

The Karoubi object cut out of X by an idempotent of its endomorphism algebra.

Equations

• RS.cutBy f X he = { X := X.X, p := eK.f, idem := ⋯ }

theorem RS.isAtom_cutBy {R : ℕ} (f : EdgeRankParameter R) (X : CategoryTheory.Idempotents.Karoubi (SkeinObj f)) {eK : CategoryTheory.End X} (he : IsAtomicIdempotent eK) : IsAtom f (cutBy f X ⋯)

The object cut out by an atomic idempotent is an atom.