The strand generator of the envelope

The embedded strand objects of the envelope and their tensor calculus: the n-strand envelope object is the n-th tensor power of the single strand, up to canonical isomorphism. This is the spine of the Deligne generator and moderate-growth fields.

Object-level equalities in Karoubi envelopes

theorem RS.karoubi_obj_ext {D : Type u} [CategoryTheory.Category.{v, u} D] {X : D} {p q : X ⟶ X} (h : p = q) {hp : CategoryTheory.CategoryStruct.comp p p = p} {hq : CategoryTheory.CategoryStruct.comp q q = q} : { X := X, p := p, idem := hp } = { X := X, p := q, idem := hq }

Karoubi objects with equal idempotents are equal.

The embedded strands

noncomputable def RS.strandK {R : ℕ} (f : EdgeRankParameter R) (n : ℕ) : CategoryTheory.Idempotents.Karoubi (SkeinObj f)

The embedded n-strand object of the corner category.

Equations

• RS.strandK f n = (CategoryTheory.Idempotents.toKaroubi (RS.SkeinObj f)).obj { arity := n }

noncomputable def RS.envStrand {R : ℕ} (f : EdgeRankParameter R) (n : ℕ) : Env f

The embedded n-strand object of the envelope.

Equations

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

theorem RS.strandK_tensor {R : ℕ} (f : EdgeRankParameter R) (a b : ℕ) : CategoryTheory.MonoidalCategoryStruct.tensorObj (strandK f a) (strandK f b) = strandK f (a + b)

Strand corner objects multiply arities.

The matrix embedding is tensor-compatible

noncomputable def RS.matEmbTensorHom {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalCategory D] (x y : D) : CategoryTheory.MonoidalCategoryStruct.tensorObj ((CategoryTheory.Mat_.embedding D).obj x) ((CategoryTheory.Mat_.embedding D).obj y) ⟶ (CategoryTheory.Mat_.embedding D).obj (CategoryTheory.MonoidalCategoryStruct.tensorObj x y)

The diagonal comparison from the tensor of embeddings to the embedding of the tensor.

Equations

• RS.matEmbTensorHom x y x✝¹ x✝ = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj x y)

noncomputable def RS.matEmbTensorInv {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalCategory D] (x y : D) : (CategoryTheory.Mat_.embedding D).obj (CategoryTheory.MonoidalCategoryStruct.tensorObj x y) ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj ((CategoryTheory.Mat_.embedding D).obj x) ((CategoryTheory.Mat_.embedding D).obj y)

The diagonal comparison from the embedding of the tensor to the tensor of embeddings.

Equations

• RS.matEmbTensorInv x y x✝¹ x✝ = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj x y)

noncomputable def RS.matEmbTensorIso {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalCategory D] (x y : D) : CategoryTheory.MonoidalCategoryStruct.tensorObj ((CategoryTheory.Mat_.embedding D).obj x) ((CategoryTheory.Mat_.embedding D).obj y) ≅ (CategoryTheory.Mat_.embedding D).obj (CategoryTheory.MonoidalCategoryStruct.tensorObj x y)

The diagonal isomorphism between the tensor of embeddings and the embedding of the tensor.

Equations

• RS.matEmbTensorIso x y = { hom := RS.matEmbTensorHom x y, inv := RS.matEmbTensorInv x y, hom_inv_id := ⋯, inv_hom_id := ⋯ }

The Karoubi embedding is tensor-compatible

theorem RS.toKaroubi_tensor {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A B : D) : CategoryTheory.MonoidalCategoryStruct.tensorObj ((CategoryTheory.Idempotents.toKaroubi D).obj A) ((CategoryTheory.Idempotents.toKaroubi D).obj B) = (CategoryTheory.Idempotents.toKaroubi D).obj (CategoryTheory.MonoidalCategoryStruct.tensorObj A B)

The embedding into the Karoubi envelope carries tensor to tensor, on the nose.

The strand tensor calculus in the envelope

noncomputable def RS.envStrandTensorIso {R : ℕ} (f : EdgeRankParameter R) (a b : ℕ) : CategoryTheory.MonoidalCategoryStruct.tensorObj (envStrand f a) (envStrand f b) ≅ envStrand f (a + b)

The strand objects of the envelope multiply arities.

Equations

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

theorem RS.envStrand_zero {R : ℕ} (f : EdgeRankParameter R) : envStrand f 0 = CategoryTheory.MonoidalCategoryStruct.tensorUnit (Env f)

The zero strand of the envelope is the unit.

noncomputable def RS.envStrandPowIso {R : ℕ} (f : EdgeRankParameter R) (n : ℕ) : tensorPow (Env f) (envStrand f 1) n ≅ envStrand f n

The strand power isomorphism: the n-th tensor power of the single strand is the n-strand object.

Equations

• RS.envStrandPowIso f 0 = CategoryTheory.eqToIso ⋯
• RS.envStrandPowIso f n.succ = CategoryTheory.MonoidalCategory.tensorIso (RS.envStrandPowIso f n) (CategoryTheory.Iso.refl (RS.envStrand f 1)) ≪≫ RS.envStrandTensorIso f n 1

Retracts through the layers

noncomputable def RS.envAmbientSec {R : ℕ} (f : EdgeRankParameter R) (E : Env f) : E ⟶ (CategoryTheory.Idempotents.toKaroubi (CategoryTheory.Mat_ (CategoryTheory.Idempotents.Karoubi (SkeinObj f)))).obj E.X

The ambient section: an envelope object into the full matrix object it corners.

Equations

• RS.envAmbientSec f E = { f := E.p, comm := ⋯ }

noncomputable def RS.envAmbientRet {R : ℕ} (f : EdgeRankParameter R) (E : Env f) : (CategoryTheory.Idempotents.toKaroubi (CategoryTheory.Mat_ (CategoryTheory.Idempotents.Karoubi (SkeinObj f)))).obj E.X ⟶ E

The ambient retraction.

Equations

• RS.envAmbientRet f E = { f := E.p, comm := ⋯ }

theorem RS.envAmbientSec_ret {R : ℕ} (f : EdgeRankParameter R) (E : Env f) : CategoryTheory.CategoryStruct.comp (envAmbientSec f E) (envAmbientRet f E) = CategoryTheory.CategoryStruct.id E

The envelope object is a retract of its ambient object.

noncomputable def RS.cornerSecK {R : ℕ} (f : EdgeRankParameter R) (x : CategoryTheory.Idempotents.Karoubi (SkeinObj f)) : x ⟶ strandK f x.X.arity

The corner section: a skein corner into its full strand.

Equations

• RS.cornerSecK f x = { f := x.p, comm := ⋯ }

noncomputable def RS.cornerRetK {R : ℕ} (f : EdgeRankParameter R) (x : CategoryTheory.Idempotents.Karoubi (SkeinObj f)) : strandK f x.X.arity ⟶ x

The corner retraction.

Equations

• RS.cornerRetK f x = { f := x.p, comm := ⋯ }

theorem RS.cornerSecK_ret {R : ℕ} (f : EdgeRankParameter R) (x : CategoryTheory.Idempotents.Karoubi (SkeinObj f)) : CategoryTheory.CategoryStruct.comp (cornerSecK f x) (cornerRetK f x) = CategoryTheory.CategoryStruct.id x

A Karoubi object is a retract of its corner in the envelope.

noncomputable def RS.envEmb {R : ℕ} (f : EdgeRankParameter R) (x : CategoryTheory.Idempotents.Karoubi (SkeinObj f)) : Env f

The embedded corner object of the envelope.

Equations

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

noncomputable def RS.envEmbSec {R : ℕ} (f : EdgeRankParameter R) (x : CategoryTheory.Idempotents.Karoubi (SkeinObj f)) : envEmb f x ⟶ envStrand f x.X.arity

The embedded corner section into its strand object.

Equations

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

noncomputable def RS.envEmbRet {R : ℕ} (f : EdgeRankParameter R) (x : CategoryTheory.Idempotents.Karoubi (SkeinObj f)) : envStrand f x.X.arity ⟶ envEmb f x

The embedded corner retraction.

Equations

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

theorem RS.envEmbSec_ret {R : ℕ} (f : EdgeRankParameter R) (x : CategoryTheory.Idempotents.Karoubi (SkeinObj f)) : CategoryTheory.CategoryStruct.comp (envEmbSec f x) (envEmbRet f x) = CategoryTheory.CategoryStruct.id (envEmb f x)

And the embedding of a Karoubi object is a retract of it — the three sections that make the strand generator work.

The biproduct decomposition of a matrix object

noncomputable def RS.envMatDecomp {R : ℕ} (f : EdgeRankParameter R) (A : CategoryTheory.Mat_ (CategoryTheory.Idempotents.Karoubi (SkeinObj f))) : (CategoryTheory.Idempotents.toKaroubi (CategoryTheory.Mat_ (CategoryTheory.Idempotents.Karoubi (SkeinObj f)))).obj A ≅ ⨁ fun (i : A.ι) => envEmb f (A.X i)

A matrix object of the envelope is the biproduct of its embedded entries.

Equations

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

The generator field

theorem RS.env_strandRetract {R : ℕ} (f : EdgeRankParameter R) : RetractGeneratedBy (Env f) (envStrand f 1)

The strand generates the envelope: every object is a retract of a finite biproduct of tensor powers of the single strand.