The envelope and its regularity

The envelope of the skein category is the Karoubi completion of the matrix envelope of its Karoubi completion: idempotent-complete by construction, with finite biproducts, and with semisimple endomorphism algebras via the corner-trace argument one level up. Von Neumann regularity of every morphism follows from semisimplicity of the biproduct endomorphism algebra, and kernels are the splittings of the regular idempotents.

Regularity in semisimple rings

theorem RS.exists_mul_mul_self {A : Type u} [Ring A] [IsSemisimpleRing A] (a : A) : ∃ (b : A), a * b * a = a

Semisimple rings are von Neumann regular.

The envelope

@[reducible]

def RS.Env {R : ℕ} (f : EdgeRankParameter R) : Type 1

The envelope: the Karoubi completion of the matrix envelope of the Karoubi completion of the skein category — Kar(Add(Kar(𝒞_f))) where the accompanying paper's Cauchy completion 𝒟_f (§3.4) is Kar(Add(𝒞_f)).

The two agree up to equivalence, both being Cauchy completions of 𝒞_f, and the inner Karoubi carries its weight in the proofs: an atom is the image of an atomic idempotent of a skein endomorphism algebra, so atoms exist only where idempotents split, and the nilpotent-trace argument for the matrix envelope reads the atomic decomposition of each matrix entry (AtomicIdempotents.lean, AtomDichotomy.lean, NilpotentMatTrace.lean). The outer Karoubi is still needed: the additive envelope of an idempotent-complete category need not be idempotent-complete.

Equations

• RS.Env f = CategoryTheory.Idempotents.Karoubi (CategoryTheory.Mat_ (CategoryTheory.Idempotents.Karoubi (RS.SkeinObj f)))

Semisimplicity of envelope endomorphism algebras

noncomputable def RS.envTrace {R : ℕ} (f : EdgeRankParameter R) (E : Env f) : CategoryTheory.End E →ₗ[ℂ] ℂ

The envelope corner trace.

Equations

• RS.envTrace f E = { toFun := fun (x : CategoryTheory.End E) => (RS.matTrace f E.X) x.f, map_add' := ⋯, map_smul' := ⋯ }

theorem RS.envEnd_isSemisimpleRing {R : ℕ} (f : EdgeRankParameter R) (E : Env f) : IsSemisimpleRing (CategoryTheory.End E)

Semisimplicity of envelope endomorphism algebras.

Regularity of envelope morphisms

theorem RS.env_hom_regular {R : ℕ} (f : EdgeRankParameter R) {M N : Env f} (u : M ⟶ N) : ∃ (g : N ⟶ M), CategoryTheory.CategoryStruct.comp u (CategoryTheory.CategoryStruct.comp g u) = u

Every envelope morphism is von Neumann regular.

Kernels

theorem RS.env_hasKernels {R : ℕ} (f : EdgeRankParameter R) : CategoryTheory.Limits.HasKernels (Env f)

Kernels exist in the envelope.

Cokernels

theorem RS.env_hasCokernels {R : ℕ} (f : EdgeRankParameter R) : CategoryTheory.Limits.HasCokernels (Env f)

Cokernels exist in the envelope.

Monomorphisms and epimorphisms split

theorem RS.env_mono_split {R : ℕ} (f : EdgeRankParameter R) {M N : Env f} (m : M ⟶ N) [CategoryTheory.Mono m] : ∃ (r : N ⟶ M), CategoryTheory.CategoryStruct.comp m r = CategoryTheory.CategoryStruct.id M

Monomorphisms split.

theorem RS.env_epi_split {R : ℕ} (f : EdgeRankParameter R) {M N : Env f} (e : M ⟶ N) [CategoryTheory.Epi e] : ∃ (s : N ⟶ M), CategoryTheory.CategoryStruct.comp s e = CategoryTheory.CategoryStruct.id N

Epimorphisms split.

Normality and the abelian structure

@[instance_reducible]

noncomputable def RS.envNormalMono {R : ℕ} (f : EdgeRankParameter R) {M N : Env f} (m : M ⟶ N) [CategoryTheory.Mono m] : CategoryTheory.NormalMono m

Every mono is a kernel.

Equations

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

@[instance_reducible]

noncomputable def RS.envNormalEpi {R : ℕ} (f : EdgeRankParameter R) {M N : Env f} (e : M ⟶ N) [CategoryTheory.Epi e] : CategoryTheory.NormalEpi e

Every epi is a cokernel.

Equations

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

@[reducible]

noncomputable def RS.envAbelian {R : ℕ} (f : EdgeRankParameter R) : CategoryTheory.Abelian (Env f)

The envelope is abelian, from the factorial trace obstruction and the connection pairing.

Equations

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