The three-letter multi-tensor against the nested binary tensor

The comparison of the wide presentation of the multi-tensor of a three-element list with the left-nested binary module tensor product of ModTensor.lean.

• triple_decomp: a three-element list has exactly two adjacent slots.
• tripleResolve/tripleResolveInv: the resolution of the three-element fold onto the plain triple tensor, absorbing the unit seed of the fold.
• tripleLegFst_resolve, tripleLegSnd_resolve, and the inverse forms: the slot legs of the wide relation pair against the resolutions, with the window morphism quantified.
• modMultiTripleHom: the forward descent through the wide coequalizer, landing on the cover of the inverse associator of ModAssoc.lean; its slot conditions are the whiskered binary balance and the cover condition of the inverse associator.
• tripleInvCover, tripleInvMid, modMultiTripleInv: the backward double descent through the outer and inner binary coequalizers, mapping onto the wide projection.
• modMultiTriple: the packaged isomorphism modMulti A [X, Y, Z] ≅ modTensor A (modTensorMod A X Y) Z, with defining equations against the projections in both directions.

The resolution of the three-element fold

theorem RS.triple_decomp {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] {X Y Z M N : CategoryTheory.Mod D A} {pre post : List (CategoryTheory.Mod D A)} (h : [X, Y, Z] = pre ++ M :: N :: post) : pre = [] ∧ X = M ∧ Y = N ∧ post = [Z] ∨ pre = [X] ∧ Y = M ∧ Z = N ∧ post = []

The two decompositions of a three-element list: the slot at the head and the slot at the tail.

def RS.tripleResolve {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] (X Y Z : CategoryTheory.Mod D A) : modList A [X, Y, Z] ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj X.X (CategoryTheory.MonoidalCategoryStruct.tensorObj Y.X Z.X)

The resolution of the three-element fold onto the plain triple tensor: absorb the unit seed. A bridge morphism with a modList-typed source, so that statements through it stay type-correct at low transparency.

Equations

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

def RS.tripleResolveInv {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] (X Y Z : CategoryTheory.Mod D A) : CategoryTheory.MonoidalCategoryStruct.tensorObj X.X (CategoryTheory.MonoidalCategoryStruct.tensorObj Y.X Z.X) ⟶ modList A [X, Y, Z]

The inverse resolution: reinstate the unit seed.

Equations

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

@[simp]

theorem RS.tripleResolve_inv {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] (X Y Z : CategoryTheory.Mod D A) : CategoryTheory.CategoryStruct.comp (tripleResolve A X Y Z) (tripleResolveInv A X Y Z) = CategoryTheory.CategoryStruct.id (modList A [X, Y, Z])

@[simp]

theorem RS.tripleResolve_inv_assoc {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] (X Y Z : CategoryTheory.Mod D A) {Z✝ : D} (h : modList A [X, Y, Z] ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (tripleResolve A X Y Z) (CategoryTheory.CategoryStruct.comp (tripleResolveInv A X Y Z) h) = h

@[simp]

theorem RS.tripleResolveInv_resolve {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] (X Y Z : CategoryTheory.Mod D A) : CategoryTheory.CategoryStruct.comp (tripleResolveInv A X Y Z) (tripleResolve A X Y Z) = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj X.X (CategoryTheory.MonoidalCategoryStruct.tensorObj Y.X Z.X))

@[simp]

theorem RS.tripleResolveInv_resolve_assoc {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] (X Y Z : CategoryTheory.Mod D A) {Z✝ : D} (h : CategoryTheory.MonoidalCategoryStruct.tensorObj X.X (CategoryTheory.MonoidalCategoryStruct.tensorObj Y.X Z.X) ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (tripleResolveInv A X Y Z) (CategoryTheory.CategoryStruct.comp (tripleResolve A X Y Z) h) = h

def RS.tripleSeedFst {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] (X Y Z : CategoryTheory.Mod D A) : modMultiMid A [] X Y [Z] ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj X.X A) Y.X) Z.X

The window seed of the head slot: absorb the unit seed of the suffix fold, retyped at modMultiMid.

Equations

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

def RS.tripleSeedFstInv {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] (X Y Z : CategoryTheory.Mod D A) : CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj X.X A) Y.X) Z.X ⟶ modMultiMid A [] X Y [Z]

The inverse window seed of the head slot.

Equations

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

theorem RS.tripleLegFst_resolve {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] (X Y Z : CategoryTheory.Mod D A) (w : CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj X.X A) Y.X ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj X.X Y.X) (h : [] ++ [X, Y, Z] = [X, Y, Z]) : CategoryTheory.CategoryStruct.comp (modMultiLegOf A X Y [Z] w []) (CategoryTheory.CategoryStruct.comp (modListCast A h) (tripleResolve A X Y Z)) = CategoryTheory.CategoryStruct.comp (tripleSeedFst A X Y Z) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight w Z.X) (CategoryTheory.MonoidalCategoryStruct.associator X.X Y.X Z.X).hom)

The head-slot leg against the resolution: the unit seed is absorbed, the window morphism and the reassociation remain.

theorem RS.tripleLegFst_resolve_assoc {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] (X Y Z : CategoryTheory.Mod D A) (w : CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj X.X A) Y.X ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj X.X Y.X) (h : [] ++ [X, Y, Z] = [X, Y, Z]) {Z✝ : D} (h✝ : CategoryTheory.MonoidalCategoryStruct.tensorObj X.X (CategoryTheory.MonoidalCategoryStruct.tensorObj Y.X Z.X) ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (modMultiLegOf A X Y [Z] w []) (CategoryTheory.CategoryStruct.comp (modListCast A h) (CategoryTheory.CategoryStruct.comp (tripleResolve A X Y Z) h✝)) = CategoryTheory.CategoryStruct.comp (tripleSeedFst A X Y Z) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight w Z.X) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X.X Y.X Z.X).hom h✝))

The head-slot leg against the resolution: the unit seed is absorbed, the window morphism and the reassociation remain.

theorem RS.tripleLegFst_resolveInv {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] (X Y Z : CategoryTheory.Mod D A) (w : CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj X.X A) Y.X ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj X.X Y.X) (h : [] ++ [X, Y, Z] = [X, Y, Z]) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight w Z.X) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X.X Y.X Z.X).hom (tripleResolveInv A X Y Z)) = CategoryTheory.CategoryStruct.comp (tripleSeedFstInv A X Y Z) (CategoryTheory.CategoryStruct.comp (modMultiLegOf A X Y [Z] w []) (modListCast A h))

A window morphism against the inverse resolution, in head-slot leg form.

theorem RS.tripleLegFst_resolveInv_assoc {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] (X Y Z : CategoryTheory.Mod D A) (w : CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj X.X A) Y.X ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj X.X Y.X) (h : [] ++ [X, Y, Z] = [X, Y, Z]) {Z✝ : D} (h✝ : modList A [X, Y, Z] ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight w Z.X) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X.X Y.X Z.X).hom (CategoryTheory.CategoryStruct.comp (tripleResolveInv A X Y Z) h✝)) = CategoryTheory.CategoryStruct.comp (tripleSeedFstInv A X Y Z) (CategoryTheory.CategoryStruct.comp (modMultiLegOf A X Y [Z] w []) (CategoryTheory.CategoryStruct.comp (modListCast A h) h✝))

A window morphism against the inverse resolution, in head-slot leg form.

def RS.tripleSeedSnd {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] (X Y Z : CategoryTheory.Mod D A) : modMultiMid A [X] Y Z [] ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj X.X (CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj Y.X A) Z.X)

The window seed of the tail slot: the whiskered pair seed, retyped at modMultiMid over the head prefix.

Equations

• RS.tripleSeedSnd A X Y Z = CategoryTheory.MonoidalCategoryStruct.whiskerLeft X.X (RS.pairSeed A Y Z)

def RS.tripleSeedSndInv {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] (X Y Z : CategoryTheory.Mod D A) : CategoryTheory.MonoidalCategoryStruct.tensorObj X.X (CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj Y.X A) Z.X) ⟶ modMultiMid A [X] Y Z []

The inverse window seed of the tail slot.

Equations

• RS.tripleSeedSndInv A X Y Z = CategoryTheory.MonoidalCategoryStruct.whiskerLeft X.X (RS.pairSeedInv A Y Z)

theorem RS.tripleLegSnd_resolve {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] (X Y Z : CategoryTheory.Mod D A) (w : CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj Y.X A) Z.X ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj Y.X Z.X) (h : [X] ++ [Y, Z] = [X, Y, Z]) : CategoryTheory.CategoryStruct.comp (modMultiLegOf A Y Z [] w [X]) (CategoryTheory.CategoryStruct.comp (modListCast A h) (tripleResolve A X Y Z)) = CategoryTheory.CategoryStruct.comp (tripleSeedSnd A X Y Z) (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X.X w)

The tail-slot leg against the resolution: under the head factor the leg is the pair leg, and the pair resolution applies.

theorem RS.tripleLegSnd_resolve_assoc {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] (X Y Z : CategoryTheory.Mod D A) (w : CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj Y.X A) Z.X ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj Y.X Z.X) (h : [X] ++ [Y, Z] = [X, Y, Z]) {Z✝ : D} (h✝ : CategoryTheory.MonoidalCategoryStruct.tensorObj X.X (CategoryTheory.MonoidalCategoryStruct.tensorObj Y.X Z.X) ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (modMultiLegOf A Y Z [] w [X]) (CategoryTheory.CategoryStruct.comp (modListCast A h) (CategoryTheory.CategoryStruct.comp (tripleResolve A X Y Z) h✝)) = CategoryTheory.CategoryStruct.comp (tripleSeedSnd A X Y Z) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X.X w) h✝)

The tail-slot leg against the resolution: under the head factor the leg is the pair leg, and the pair resolution applies.

theorem RS.tripleLegSnd_resolveInv {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] (X Y Z : CategoryTheory.Mod D A) (w : CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj Y.X A) Z.X ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj Y.X Z.X) (h : [X] ++ [Y, Z] = [X, Y, Z]) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X.X w) (tripleResolveInv A X Y Z) = CategoryTheory.CategoryStruct.comp (tripleSeedSndInv A X Y Z) (CategoryTheory.CategoryStruct.comp (modMultiLegOf A Y Z [] w [X]) (modListCast A h))

A window morphism against the inverse resolution, in tail-slot leg form.

theorem RS.tripleLegSnd_resolveInv_assoc {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] (X Y Z : CategoryTheory.Mod D A) (w : CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj Y.X A) Z.X ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj Y.X Z.X) (h : [X] ++ [Y, Z] = [X, Y, Z]) {Z✝ : D} (h✝ : modList A [X, Y, Z] ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X.X w) (CategoryTheory.CategoryStruct.comp (tripleResolveInv A X Y Z) h✝) = CategoryTheory.CategoryStruct.comp (tripleSeedSndInv A X Y Z) (CategoryTheory.CategoryStruct.comp (modMultiLegOf A Y Z [] w [X]) (CategoryTheory.CategoryStruct.comp (modListCast A h) h✝))

A window morphism against the inverse resolution, in tail-slot leg form.

The comparison isomorphism

theorem RS.tripleWindowFst_cond {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Limits.HasCoequalizers D] [∀ (V : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft V)] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.IsCommMonObj A] (X Y Z : CategoryTheory.Mod D A) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (modTensorLegM A X Y) Z.X) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X.X Y.X Z.X).hom (modTensorAssocInvCover A X Y Z)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (modTensorLegN A X Y) Z.X) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X.X Y.X Z.X).hom (modTensorAssocInvCover A X Y Z))

The head window against the inverse-associator cover: the two binary legs agree after the cover, by the inner balance whiskered by Z.

noncomputable def RS.modMultiTripleHom {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] [∀ (V : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft V)] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.IsCommMonObj A] (X Y Z : CategoryTheory.Mod D A) : modMulti A [X, Y, Z] ⟶ modTensor A (modTensorMod A X Y) Z

The forward comparison: the wide projection descends onto the cover of the inverse associator. The head slot condition is the whiskered binary balance, the tail slot condition is the cover condition of the inverse associator.

Equations

• RS.modMultiTripleHom A X Y Z = RS.modMultiDesc A (CategoryTheory.CategoryStruct.comp (RS.tripleResolve A X Y Z) (RS.modTensorAssocInvCover A X Y Z)) ⋯

@[simp]

theorem RS.modMultiπ_tripleHom {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] [∀ (V : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft V)] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.IsCommMonObj A] (X Y Z : CategoryTheory.Mod D A) : CategoryTheory.CategoryStruct.comp (modMultiπ A [X, Y, Z]) (modMultiTripleHom A X Y Z) = CategoryTheory.CategoryStruct.comp (tripleResolve A X Y Z) (modTensorAssocInvCover A X Y Z)

Defining equation of the forward comparison.

@[simp]

theorem RS.modMultiπ_tripleHom_assoc {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] [∀ (V : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft V)] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.IsCommMonObj A] (X Y Z : CategoryTheory.Mod D A) {Z✝ : D} (h : modTensor A (modTensorMod A X Y) Z ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (modMultiπ A [X, Y, Z]) (CategoryTheory.CategoryStruct.comp (modMultiTripleHom A X Y Z) h) = CategoryTheory.CategoryStruct.comp (tripleResolve A X Y Z) (CategoryTheory.CategoryStruct.comp (modTensorAssocInvCover A X Y Z) h)

Defining equation of the forward comparison.

theorem RS.modMultiπ_tripleHom_π {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] [∀ (V : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft V)] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.IsCommMonObj A] (X Y Z : CategoryTheory.Mod D A) : CategoryTheory.CategoryStruct.comp (modMultiπ A [X, Y, Z]) (modMultiTripleHom A X Y Z) = CategoryTheory.CategoryStruct.comp (tripleResolve A X Y Z) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X.X Y.X Z.X).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (modTensorπ A X Y) Z.X) (modTensorπ A (modTensorMod A X Y) Z)))

Defining equation of the forward comparison, with the cover spelled out on the projections of the nested binary tensor.

theorem RS.modMultiπ_tripleHom_π_assoc {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] [∀ (V : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft V)] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.IsCommMonObj A] (X Y Z : CategoryTheory.Mod D A) {Z✝ : D} (h : modTensor A (modTensorMod A X Y) Z ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (modMultiπ A [X, Y, Z]) (CategoryTheory.CategoryStruct.comp (modMultiTripleHom A X Y Z) h) = CategoryTheory.CategoryStruct.comp (tripleResolve A X Y Z) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X.X Y.X Z.X).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (modTensorπ A X Y) Z.X) (modTensorπ A (modTensorMod A X Y) Z)) h))

Defining equation of the forward comparison, with the cover spelled out on the projections of the nested binary tensor.

noncomputable def RS.tripleInvCover {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] (A : D) [CategoryTheory.MonObj A] (X Y Z : CategoryTheory.Mod D A) : CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj X.X Y.X) Z.X ⟶ modMulti A [X, Y, Z]

The cover of the backward comparison: reassociate, reinstate the unit seed, and project onto the multi-tensor.

Equations

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

theorem RS.tripleInvCover_cond {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] (A : D) [CategoryTheory.MonObj A] (X Y Z : CategoryTheory.Mod D A) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (modTensorLegM A X Y) Z.X) (tripleInvCover A X Y Z) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (modTensorLegN A X Y) Z.X) (tripleInvCover A X Y Z)

The cover of the backward comparison coequalizes the whiskered inner balance: the head slot relation of the wide pair.

theorem RS.tripleResolveInv_snd_rel {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] (A : D) [CategoryTheory.MonObj A] (X Y Z : CategoryTheory.Mod D A) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X.X (CategoryTheory.MonoidalCategoryStruct.whiskerRight (actRight A Y.X) Z.X)) (CategoryTheory.CategoryStruct.comp (tripleResolveInv A X Y Z) (modMultiπ A [X, Y, Z])) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X.X (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator Y.X A Z.X).hom (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Y.X (actLeft A Z.X)))) (CategoryTheory.CategoryStruct.comp (tripleResolveInv A X Y Z) (modMultiπ A [X, Y, Z]))

The tail slot relation after the inverse resolution, spelled at the braided right action: the bridge between the outer balance of the nested binary tensor and the wide relation pair.

theorem RS.tripleResolveInv_snd_rel_assoc {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] (A : D) [CategoryTheory.MonObj A] (X Y Z : CategoryTheory.Mod D A) {Z✝ : D} (h : modMulti A [X, Y, Z] ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X.X (CategoryTheory.MonoidalCategoryStruct.whiskerRight (actRight A Y.X) Z.X)) (CategoryTheory.CategoryStruct.comp (tripleResolveInv A X Y Z) (CategoryTheory.CategoryStruct.comp (modMultiπ A [X, Y, Z]) h)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X.X (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator Y.X A Z.X).hom (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Y.X (actLeft A Z.X)))) (CategoryTheory.CategoryStruct.comp (tripleResolveInv A X Y Z) (CategoryTheory.CategoryStruct.comp (modMultiπ A [X, Y, Z]) h))

The tail slot relation after the inverse resolution, spelled at the braided right action: the bridge between the outer balance of the nested binary tensor and the wide relation pair.

noncomputable def RS.tripleInvMid {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] [∀ (V : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorRight V)] (A : D) [CategoryTheory.MonObj A] (X Y Z : CategoryTheory.Mod D A) : CategoryTheory.MonoidalCategoryStruct.tensorObj (modTensor A X Y) Z.X ⟶ modMulti A [X, Y, Z]

The half-descended backward comparison, on the cover of the outer coequalizer of the nested binary tensor.

Equations

• RS.tripleInvMid A X Y Z = RS.modTensorWhiskerRDesc A X Y Z.X (RS.tripleInvCover A X Y Z) ⋯

@[simp]

theorem RS.whiskerRight_modTensorπ_tripleInvMid {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] [∀ (V : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorRight V)] (A : D) [CategoryTheory.MonObj A] (X Y Z : CategoryTheory.Mod D A) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (modTensorπ A X Y) Z.X) (tripleInvMid A X Y Z) = tripleInvCover A X Y Z

Defining equation of the half-descended backward comparison.

@[simp]

theorem RS.whiskerRight_modTensorπ_tripleInvMid_assoc {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] [∀ (V : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorRight V)] (A : D) [CategoryTheory.MonObj A] (X Y Z : CategoryTheory.Mod D A) {Z✝ : D} (h : modMulti A [X, Y, Z] ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (modTensorπ A X Y) Z.X) (CategoryTheory.CategoryStruct.comp (tripleInvMid A X Y Z) h) = CategoryTheory.CategoryStruct.comp (tripleInvCover A X Y Z) h

Defining equation of the half-descended backward comparison.

theorem RS.tripleInvMid_cond {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] [∀ (V : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft V)] [∀ (V : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorRight V)] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.IsCommMonObj A] (X Y Z : CategoryTheory.Mod D A) : CategoryTheory.CategoryStruct.comp (modTensorLegM A (modTensorMod A X Y) Z) (tripleInvMid A X Y Z) = CategoryTheory.CategoryStruct.comp (modTensorLegN A (modTensorMod A X Y) Z) (tripleInvMid A X Y Z)

The half-descended backward comparison coequalizes the outer balance: the monoid sliding between the (X, Y)-block and Z slides into the tail slot of the wide relation pair.

noncomputable def RS.modMultiTripleInv {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] [∀ (V : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft V)] [∀ (V : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorRight V)] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.IsCommMonObj A] (X Y Z : CategoryTheory.Mod D A) : modTensor A (modTensorMod A X Y) Z ⟶ modMulti A [X, Y, Z]

The backward comparison: the nested binary tensor descends onto the multi-tensor, by double descent through the outer and inner coequalizers.

Equations

• RS.modMultiTripleInv A X Y Z = RS.modTensorDesc A (RS.modTensorMod A X Y) Z (RS.tripleInvMid A X Y Z) ⋯

@[simp]

theorem RS.modTensorπ_tripleInv {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] [∀ (V : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft V)] [∀ (V : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorRight V)] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.IsCommMonObj A] (X Y Z : CategoryTheory.Mod D A) : CategoryTheory.CategoryStruct.comp (modTensorπ A (modTensorMod A X Y) Z) (modMultiTripleInv A X Y Z) = tripleInvMid A X Y Z

Defining equation of the backward comparison against the outer projection.

@[simp]

theorem RS.modTensorπ_tripleInv_assoc {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] [∀ (V : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft V)] [∀ (V : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorRight V)] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.IsCommMonObj A] (X Y Z : CategoryTheory.Mod D A) {Z✝ : D} (h : modMulti A [X, Y, Z] ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (modTensorπ A (modTensorMod A X Y) Z) (CategoryTheory.CategoryStruct.comp (modMultiTripleInv A X Y Z) h) = CategoryTheory.CategoryStruct.comp (tripleInvMid A X Y Z) h

Defining equation of the backward comparison against the outer projection.

theorem RS.whiskerRight_modTensorπ_tripleInv {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] [∀ (V : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft V)] [∀ (V : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorRight V)] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.IsCommMonObj A] (X Y Z : CategoryTheory.Mod D A) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (modTensorπ A X Y) Z.X) (CategoryTheory.CategoryStruct.comp (modTensorπ A (modTensorMod A X Y) Z) (modMultiTripleInv A X Y Z)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X.X Y.X Z.X).hom (CategoryTheory.CategoryStruct.comp (tripleResolveInv A X Y Z) (modMultiπ A [X, Y, Z]))

Defining equation of the backward comparison against both projections: reassociate, reinstate the unit seed, and project.

theorem RS.whiskerRight_modTensorπ_tripleInv_assoc {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] [∀ (V : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft V)] [∀ (V : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorRight V)] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.IsCommMonObj A] (X Y Z : CategoryTheory.Mod D A) {Z✝ : D} (h : modMulti A [X, Y, Z] ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (modTensorπ A X Y) Z.X) (CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (modTensorπ A (modTensorMod A X Y) Z) (modMultiTripleInv A X Y Z)) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X.X Y.X Z.X).hom (CategoryTheory.CategoryStruct.comp (tripleResolveInv A X Y Z) (CategoryTheory.CategoryStruct.comp (modMultiπ A [X, Y, Z]) h))

Defining equation of the backward comparison against both projections: reassociate, reinstate the unit seed, and project.

@[simp]

theorem RS.modMultiTripleHom_tripleInv {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] [∀ (V : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft V)] [∀ (V : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorRight V)] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.IsCommMonObj A] (X Y Z : CategoryTheory.Mod D A) : CategoryTheory.CategoryStruct.comp (modMultiTripleHom A X Y Z) (modMultiTripleInv A X Y Z) = CategoryTheory.CategoryStruct.id (modMulti A [X, Y, Z])

The forward comparison retracts the backward comparison.

@[simp]

theorem RS.modMultiTripleHom_tripleInv_assoc {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] [∀ (V : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft V)] [∀ (V : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorRight V)] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.IsCommMonObj A] (X Y Z : CategoryTheory.Mod D A) {Z✝ : D} (h : modMulti A [X, Y, Z] ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (modMultiTripleHom A X Y Z) (CategoryTheory.CategoryStruct.comp (modMultiTripleInv A X Y Z) h) = h

The forward comparison retracts the backward comparison.

@[simp]

theorem RS.modMultiTripleInv_tripleHom {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] [∀ (V : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft V)] [∀ (V : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorRight V)] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.IsCommMonObj A] (X Y Z : CategoryTheory.Mod D A) : CategoryTheory.CategoryStruct.comp (modMultiTripleInv A X Y Z) (modMultiTripleHom A X Y Z) = CategoryTheory.CategoryStruct.id (modTensor A (modTensorMod A X Y) Z)

The backward comparison retracts the forward comparison.

@[simp]

theorem RS.modMultiTripleInv_tripleHom_assoc {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] [∀ (V : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft V)] [∀ (V : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorRight V)] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.IsCommMonObj A] (X Y Z : CategoryTheory.Mod D A) {Z✝ : D} (h : modTensor A (modTensorMod A X Y) Z ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (modMultiTripleInv A X Y Z) (CategoryTheory.CategoryStruct.comp (modMultiTripleHom A X Y Z) h) = h

The backward comparison retracts the forward comparison.

noncomputable def RS.modMultiTriple {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] [∀ (V : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft V)] [∀ (V : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorRight V)] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.IsCommMonObj A] (X Y Z : CategoryTheory.Mod D A) : modMulti A [X, Y, Z] ≅ modTensor A (modTensorMod A X Y) Z

The three-letter multi-tensor is the nested binary tensor: the one-step wide presentation of modMulti A [X, Y, Z] and the left-nested binary module tensor product coequalize the same relations.

Equations

• RS.modMultiTriple A X Y Z = { hom := RS.modMultiTripleHom A X Y Z, inv := RS.modMultiTripleInv A X Y Z, hom_inv_id := ⋯, inv_hom_id := ⋯ }