The merge isomorphism for module powers

The relative tensor product of two module powers is the module power of the summed arity: the descended power multiplication powMulDesc of PowChain.lean is an isomorphism modTensor A (modPowMod A X a) (modPowMod A X b) ≅ modPow A X (a + 1 + b + 1), with inverse powSplit descended from the inverse of the concatenation of ambient tensor powers.

• headMod: the head insertion X ⊗ X^⊗b ⟶ modPow A X (b + 1); through modPowMul with the singleton power it is a module map for the action on the head factor (headMod_act) — the slide of the monoid from the head to the tail of a module power, packaged through the multiplication rather than proved slot by slot.
• powSplit: the inverse direction, descended through the wide coequalizer. Each slot relation of the big power either lands inside one half, where the corresponding half projection absorbs it (powSplit_cond_left/powSplit_cond_right), or at the boundary between the halves, where it becomes the coequalizer relation of the module tensor product itself (powSplit_cond_bound).
• powMergeIso: the packaged isomorphism, with powMulDesc as the forward direction and powSplit as the inverse.

Structural shuffles of the boundary window

Both boundary computations move a window map across the split of the ambient power into two halves. The shuffles are stated at general objects, so that no tensor-power arity enters the rewriting.

theorem RS.split_shuffle_fst {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] {P Q R S B : D} (u : Q ⟶ R) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.whiskerLeft P (CategoryTheory.MonoidalCategoryStruct.whiskerRight u S)) B) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.associator P R S).inv B) (CategoryTheory.MonoidalCategoryStruct.associator (CategoryTheory.MonoidalCategoryStruct.tensorObj P R) S B).hom) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator P (CategoryTheory.MonoidalCategoryStruct.tensorObj Q S) B).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft P (CategoryTheory.MonoidalCategoryStruct.associator Q S B).hom) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator P Q (CategoryTheory.MonoidalCategoryStruct.tensorObj S B)).inv (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.whiskerLeft P u) (CategoryTheory.MonoidalCategoryStruct.tensorObj S B))))

The left-window shuffle: a window map acting on the first two window factors passes to the left half of the split.

theorem RS.whiskerRight_tensorHom {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] {P₁ P₂ Q₂ R S : D} (f : P₁ ⟶ P₂) (g : P₂ ⟶ S) (h : R ⟶ Q₂) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight f R) (CategoryTheory.MonoidalCategoryStruct.tensorHom g h) = CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.CategoryStruct.comp f g) h

A whisker absorbed into the left factor of a tensor of morphisms.

theorem RS.whiskerRight_tensorHom_whiskerRight {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] {P₁ P₂ S T R Q₂ : D} (f : P₁ ⟶ P₂) (g : P₂ ⟶ S) (k : S ⟶ T) (h : R ⟶ Q₂) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight f R) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom g h) (CategoryTheory.MonoidalCategoryStruct.whiskerRight k Q₂)) = CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp g k)) h

Two whiskers absorbed into the left factor of a tensor of morphisms.

theorem RS.whiskerLeft_comp_tensorHom {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] {P Q₁ R₁ R₂ S : D} (f : R₁ ⟶ R₂) (g : P ⟶ Q₁) (h : R₂ ⟶ S) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft P f) (CategoryTheory.MonoidalCategoryStruct.tensorHom g h) = CategoryTheory.MonoidalCategoryStruct.tensorHom g (CategoryTheory.CategoryStruct.comp f h)

A left whisker absorbed into the right factor of a tensor of morphisms.

theorem RS.split_shuffle_snd {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] {P Y G S B : D} (v : CategoryTheory.MonoidalCategoryStruct.tensorObj G S ⟶ S) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.whiskerLeft P (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator Y G S).hom (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Y v))) B) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.associator P Y S).inv B) (CategoryTheory.MonoidalCategoryStruct.associator (CategoryTheory.MonoidalCategoryStruct.tensorObj P Y) S B).hom) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator P (CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj Y G) S) B).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft P (CategoryTheory.MonoidalCategoryStruct.associator (CategoryTheory.MonoidalCategoryStruct.tensorObj Y G) S B).hom) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator P (CategoryTheory.MonoidalCategoryStruct.tensorObj Y G) (CategoryTheory.MonoidalCategoryStruct.tensorObj S B)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.associator P Y G).inv (CategoryTheory.MonoidalCategoryStruct.tensorObj S B)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator (CategoryTheory.MonoidalCategoryStruct.tensorObj P Y) G (CategoryTheory.MonoidalCategoryStruct.tensorObj S B)).hom (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (CategoryTheory.MonoidalCategoryStruct.tensorObj P Y) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator G S B).inv (CategoryTheory.MonoidalCategoryStruct.whiskerRight v B)))))))

The right-window shuffle: a window map acting on the last two window factors passes to the head of the right half of the split.

The head insertion

The split of the big power exposes the right half with its head factor peeled: the map into the module power of the right half is the peeling inverse followed by the projection. Through the multiplication with the singleton power this insertion is a module map for the action on the head factor — the slide of the monoid from the head to the tail of a module power, obtained from modPowMul_actLeft rather than slot by slot.

noncomputable def RS.toPowOne {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (X : D) : X ⟶ tensorPow D X 1

The left unitor inverse, retyped so that its target is stated through the singleton tensor power — this keeps every statement about it type-correct at low transparency.

Equations

• RS.toPowOne X = (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).inv

theorem RS.powPeel_inv_concat {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (X : D) (b : ℕ) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (toPowOne X) (tensorPow D X b)) (CategoryTheory.CategoryStruct.comp (tensorPowConcat X 1 b).hom (powCast X ⋯)) = (powPeel X b).inv

The peeling inverse is the concatenation with a singleton block, up to the unitor and an arity transport.

theorem RS.powPeel_inv_concat_assoc {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (X : D) (b : ℕ) {Z : D} (h : tensorPow D X (b + 1) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (toPowOne X) (tensorPow D X b)) (CategoryTheory.CategoryStruct.comp (tensorPowConcat X 1 b).hom (CategoryTheory.CategoryStruct.comp (powCast X ⋯) h)) = CategoryTheory.CategoryStruct.comp (powPeel X b).inv h

The peeling inverse is the concatenation with a singleton block, up to the unitor and an arity transport.

noncomputable def RS.headMod {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 : D) [CategoryTheory.ModObj A X] (b : ℕ) : CategoryTheory.MonoidalCategoryStruct.tensorObj X (tensorPow D X b) ⟶ modPow A X (b + 1)

The head insertion of a factor into a module power: peel the head off the target power and project.

Equations

• RS.headMod A X b = CategoryTheory.CategoryStruct.comp (RS.powPeel X b).inv (RS.modPowπ A X (b + 1))

theorem RS.headMod_eq_mul {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Z)] (A : D) [CategoryTheory.MonObj A] (X : D) [CategoryTheory.ModObj A X] (b : ℕ) : headMod A X b = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (modPowOne A X).inv (modPowπ A X b)) (CategoryTheory.CategoryStruct.comp (modPowMul A X 1 b) (modPowCast A X ⋯))

The head insertion is the multiplication with the singleton power, up to the singleton isomorphism and an arity transport.

theorem RS.headMod_act {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Z)] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.IsCommMonObj A] (X : D) [CategoryTheory.ModObj A X] (b : ℕ) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (headMod A X b)) (modPowAct A X b) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator A X (tensorPow D X b)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (actLeft A X) (tensorPow D X b)) (headMod A X b))

The head insertion is a module map: the monoid acting on the head factor descends to the module-power action. At positive arity this is modPowMul_actLeft with a singleton left block — the slide of the monoid across the whole power, packaged through the multiplication.

The tail of the left half

The braided right action of the monoid on the left half of the split is, after the projection, the boundary window's action on the last factor of the left half.

theorem RS.braidPast_hom_swap {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] (U V T : D) : CategoryTheory.CategoryStruct.comp (braidPast U V T).hom (braidPast V U T).hom = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj U (CategoryTheory.MonoidalCategoryStruct.tensorObj V T))

In a symmetric category, carrying past a context inverts to carrying back past it.

theorem RS.braiding_actAcross {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] (A : D) [CategoryTheory.MonObj A] (X : D) [CategoryTheory.ModObj A X] (P : D) : CategoryTheory.CategoryStruct.comp (β_ (CategoryTheory.MonoidalCategoryStruct.tensorObj P X) A).hom (actAcross A P X) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator P X A).hom (CategoryTheory.MonoidalCategoryStruct.whiskerLeft P (actRight A X))

Braiding the monoid over a context pair: the braided right action through the last factor of a pair is the braiding of the factor alone, then the action — the monoid never crosses the context.

noncomputable def RS.powActRight {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Z)] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.IsCommMonObj A] (X : D) [CategoryTheory.ModObj A X] (a : ℕ) : CategoryTheory.MonoidalCategoryStruct.tensorObj (modPow A X (a + 1)) A ⟶ modPow A X (a + 1)

The braided right action of the module power, typed at the plain power — this keeps every statement about it type-correct at low transparency.

Equations

• RS.powActRight A X a = RS.actRight A (RS.modPowMod A X a).X

noncomputable def RS.boundAssoc {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A X : D) (a : ℕ) : CategoryTheory.MonoidalCategoryStruct.tensorObj (tensorPow D X a) (CategoryTheory.MonoidalCategoryStruct.tensorObj X A) ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj (tensorPow D X (a + 1)) A

The boundary reassociation, retyped so that its target is stated through the grown tensor power.

Equations

• RS.boundAssoc A X a = (CategoryTheory.MonoidalCategoryStruct.associator (RS.tensorPow D X a) X A).inv

theorem RS.modPowπ_actRight {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Z)] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.IsCommMonObj A] (X : D) [CategoryTheory.ModObj A X] (a : ℕ) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (modPowπ A X (a + 1)) A) (powActRight A X a) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator (tensorPow D X a) X A).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (tensorPow D X a) (actRight A X)) (modPowπ A X (a + 1)))

The braided right action of the left half after the projection: on the ambient power it is the boundary window's right action on the last factor.

The boundary bridge of the concatenation

noncomputable def RS.powDetach {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (X : D) (p q : ℕ) : CategoryTheory.MonoidalCategoryStruct.tensorObj (tensorPow D X (p + 1)) (tensorPow D X q) ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj (tensorPow D X p) (CategoryTheory.MonoidalCategoryStruct.tensorObj X (tensorPow D X q))

Detach the top factor of the first block onto the second. The associator, retyped so that its source is stated through the tensor power — the inverse bridge to powAttach.

Equations

• RS.powDetach X p q = (CategoryTheory.MonoidalCategoryStruct.associator (RS.tensorPow D X p) X (RS.tensorPow D X q)).hom

theorem RS.concat_split_bound {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (X : D) (a b : ℕ) : CategoryTheory.CategoryStruct.comp (tensorPowConcat X (a + 1 + 1) b).hom (CategoryTheory.CategoryStruct.comp (powCast X ⋯) (tensorPowConcat X (a + 1) (b + 1)).inv) = CategoryTheory.CategoryStruct.comp (powDetach X (a + 1) b) (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (tensorPow D X (a + 1)) (powPeel X b).inv)

The boundary split of the concatenation: undoing the split concatenation after the glued one detaches the exposed window factor onto the right half and peels it back in.

The boundary slot

The slot relation straddling the two halves of the split becomes, after both projections, the coequalizer relation of the module tensor product: the boundary bridge carries the relation object onto (modPow ⊗ A) ⊗ modPow, the braided right action of the left half absorbs the M-leg, and the head insertion of the right half absorbs the N-leg.

noncomputable def RS.boundBridge {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 : D) [CategoryTheory.ModObj A X] (a b : ℕ) : modPowMid A X a b ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj (modPow A X (a + 1)) A) (modPow A X (b + 1))

The boundary bridge: reassociate the window across the split and project both halves, keeping the monoid between them.

Equations

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

theorem RS.boundBridge_legM {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Z)] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.IsCommMonObj A] (X : D) [CategoryTheory.ModObj A X] (a b : ℕ) : CategoryTheory.CategoryStruct.comp (modPowLegM A X a b) (CategoryTheory.CategoryStruct.comp (powCast X ⋯) (CategoryTheory.CategoryStruct.comp (tensorPowConcat X (a + 1) (b + 1)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (modPowπ A X (a + 1)) (modPowπ A X (b + 1))) (modTensorπ A (modPowMod A X a) (modPowMod A X b))))) = CategoryTheory.CategoryStruct.comp (boundBridge A X a b) (CategoryTheory.CategoryStruct.comp (modTensorLegM A (modPowMod A X a) (modPowMod A X b)) (modTensorπ A (modPowMod A X a) (modPowMod A X b)))

The M-leg of the boundary slot factors through the boundary bridge and the first module-tensor leg.

theorem RS.boundBridge_legN {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Z)] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.IsCommMonObj A] (X : D) [CategoryTheory.ModObj A X] (a b : ℕ) : CategoryTheory.CategoryStruct.comp (modPowLegN A X a b) (CategoryTheory.CategoryStruct.comp (powCast X ⋯) (CategoryTheory.CategoryStruct.comp (tensorPowConcat X (a + 1) (b + 1)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (modPowπ A X (a + 1)) (modPowπ A X (b + 1))) (modTensorπ A (modPowMod A X a) (modPowMod A X b))))) = CategoryTheory.CategoryStruct.comp (boundBridge A X a b) (CategoryTheory.CategoryStruct.comp (modTensorLegN A (modPowMod A X a) (modPowMod A X b)) (modTensorπ A (modPowMod A X a) (modPowMod A X b)))

The N-leg of the boundary slot factors through the boundary bridge and the second module-tensor leg.

theorem RS.powSplit_cond_bound {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Z)] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.IsCommMonObj A] (X : D) [CategoryTheory.ModObj A X] (a b : ℕ) : CategoryTheory.CategoryStruct.comp (modPowLegM A X a b) (CategoryTheory.CategoryStruct.comp (powCast X ⋯) (CategoryTheory.CategoryStruct.comp (tensorPowConcat X (a + 1) (b + 1)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (modPowπ A X (a + 1)) (modPowπ A X (b + 1))) (modTensorπ A (modPowMod A X a) (modPowMod A X b))))) = CategoryTheory.CategoryStruct.comp (modPowLegN A X a b) (CategoryTheory.CategoryStruct.comp (powCast X ⋯) (CategoryTheory.CategoryStruct.comp (tensorPowConcat X (a + 1) (b + 1)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (modPowπ A X (a + 1)) (modPowπ A X (b + 1))) (modTensorπ A (modPowMod A X a) (modPowMod A X b)))))

The boundary slot condition: the slot relation straddling the two halves is absorbed by the split, through the coequalizer relation of the module tensor product.

The interior slots

A slot relation lying inside one half of the split embeds across the concatenation into that half and is absorbed by the half's own projection.

noncomputable def RS.midConcatFstIso {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A X : D) (s t n : ℕ) : CategoryTheory.MonoidalCategoryStruct.tensorObj (modPowMid A X s t) (tensorPow D X n) ≅ modPowMid A X s (t + n)

The bridge of midConcatFst, as an isomorphism.

Equations

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

noncomputable def RS.midConcatSndIso {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A X : D) (m s t : ℕ) : CategoryTheory.MonoidalCategoryStruct.tensorObj (tensorPow D X m) (modPowMid A X s t) ≅ modPowMid A X (m + s) t

The bridge of midConcatSnd, as an isomorphism.

Equations

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

theorem RS.powSplit_cond_left {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Z)] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.IsCommMonObj A] (X : D) [CategoryTheory.ModObj A X] (a b s t' : ℕ) (hL : s + 2 + t' = a + 1) : CategoryTheory.CategoryStruct.comp (modPowLegM A X s (t' + (b + 1))) (CategoryTheory.CategoryStruct.comp (powCast X ⋯) (CategoryTheory.CategoryStruct.comp (tensorPowConcat X (a + 1) (b + 1)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (modPowπ A X (a + 1)) (modPowπ A X (b + 1))) (modTensorπ A (modPowMod A X a) (modPowMod A X b))))) = CategoryTheory.CategoryStruct.comp (modPowLegN A X s (t' + (b + 1))) (CategoryTheory.CategoryStruct.comp (powCast X ⋯) (CategoryTheory.CategoryStruct.comp (tensorPowConcat X (a + 1) (b + 1)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (modPowπ A X (a + 1)) (modPowπ A X (b + 1))) (modTensorπ A (modPowMod A X a) (modPowMod A X b)))))

The in-left slot condition: a slot relation of the left half is absorbed by the left projection.

theorem RS.powSplit_cond_right {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Z)] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.IsCommMonObj A] (X : D) [CategoryTheory.ModObj A X] (a b s' t : ℕ) (hR : s' + 2 + t = b + 1) : CategoryTheory.CategoryStruct.comp (modPowLegM A X (a + 1 + s') t) (CategoryTheory.CategoryStruct.comp (powCast X ⋯) (CategoryTheory.CategoryStruct.comp (tensorPowConcat X (a + 1) (b + 1)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (modPowπ A X (a + 1)) (modPowπ A X (b + 1))) (modTensorπ A (modPowMod A X a) (modPowMod A X b))))) = CategoryTheory.CategoryStruct.comp (modPowLegN A X (a + 1 + s') t) (CategoryTheory.CategoryStruct.comp (powCast X ⋯) (CategoryTheory.CategoryStruct.comp (tensorPowConcat X (a + 1) (b + 1)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (modPowπ A X (a + 1)) (modPowπ A X (b + 1))) (modTensorπ A (modPowMod A X a) (modPowMod A X b)))))

The in-right slot condition: a slot relation of the right half is absorbed by the right projection.

The split and the merge isomorphism

theorem RS.powSplit_cond {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Z)] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.IsCommMonObj A] (X : D) [CategoryTheory.ModObj A X] (a b s t : ℕ) (hst : s + 2 + t = a + 1 + b + 1) : CategoryTheory.CategoryStruct.comp (modPowLegM A X s t) (CategoryTheory.CategoryStruct.comp (powCast X hst) (CategoryTheory.CategoryStruct.comp (tensorPowConcat X (a + 1) (b + 1)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (modPowπ A X (a + 1)) (modPowπ A X (b + 1))) (modTensorπ A (modPowMod A X a) (modPowMod A X b))))) = CategoryTheory.CategoryStruct.comp (modPowLegN A X s t) (CategoryTheory.CategoryStruct.comp (powCast X hst) (CategoryTheory.CategoryStruct.comp (tensorPowConcat X (a + 1) (b + 1)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (modPowπ A X (a + 1)) (modPowπ A X (b + 1))) (modTensorπ A (modPowMod A X a) (modPowMod A X b)))))

The wide-coequalizer condition of the split: every slot relation of the big power is absorbed by the split — inside the left half, at the boundary, or inside the right half.

noncomputable def RS.powSplit {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Z)] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.IsCommMonObj A] (X : D) [CategoryTheory.ModObj A X] (a b : ℕ) : modPow A X (a + 1 + b + 1) ⟶ modTensor A (modPowMod A X a) (modPowMod A X b)

The split of a module power: the inverse of the concatenation descends through the wide coequalizer onto the module tensor product of the two halves.

Equations

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

@[simp]

theorem RS.modPowπ_powSplit {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Z)] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.IsCommMonObj A] (X : D) [CategoryTheory.ModObj A X] (a b : ℕ) : CategoryTheory.CategoryStruct.comp (modPowπ A X (a + 1 + b + 1)) (powSplit A X a b) = CategoryTheory.CategoryStruct.comp (tensorPowConcat X (a + 1) (b + 1)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (modPowπ A X (a + 1)) (modPowπ A X (b + 1))) (modTensorπ A (modPowMod A X a) (modPowMod A X b)))

Defining equation of the split.

@[simp]

theorem RS.modPowπ_powSplit_assoc {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Z)] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.IsCommMonObj A] (X : D) [CategoryTheory.ModObj A X] (a b : ℕ) {Z : D} (h : modTensor A (modPowMod A X a) (modPowMod A X b) ⟶ Z) : CategoryTheory.CategoryStruct.comp (modPowπ A X (a + 1 + b + 1)) (CategoryTheory.CategoryStruct.comp (powSplit A X a b) h) = CategoryTheory.CategoryStruct.comp (tensorPowConcat X (a + 1) (b + 1)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (modPowπ A X (a + 1)) (modPowπ A X (b + 1))) (modTensorπ A (modPowMod A X a) (modPowMod A X b))) h)

Defining equation of the split.

@[simp]

theorem RS.powSplit_powMulDesc {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Z)] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.IsCommMonObj A] (X : D) [CategoryTheory.ModObj A X] (a b : ℕ) : CategoryTheory.CategoryStruct.comp (powSplit A X a b) (powMulDesc A X a b) = CategoryTheory.CategoryStruct.id (modPow A X (a + 1 + b + 1))

The split is a section of the descended power multiplication.

@[simp]

theorem RS.powSplit_powMulDesc_assoc {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Z)] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.IsCommMonObj A] (X : D) [CategoryTheory.ModObj A X] (a b : ℕ) {Z : D} (h : modPow A X (a + 1 + b + 1) ⟶ Z) : CategoryTheory.CategoryStruct.comp (powSplit A X a b) (CategoryTheory.CategoryStruct.comp (powMulDesc A X a b) h) = h

The split is a section of the descended power multiplication.

@[simp]

theorem RS.powMulDesc_powSplit {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Z)] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.IsCommMonObj A] (X : D) [CategoryTheory.ModObj A X] (a b : ℕ) : CategoryTheory.CategoryStruct.comp (powMulDesc A X a b) (powSplit A X a b) = CategoryTheory.CategoryStruct.id (modTensor A (modPowMod A X a) (modPowMod A X b))

The split is a retraction of the descended power multiplication.

@[simp]

theorem RS.powMulDesc_powSplit_assoc {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Z)] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.IsCommMonObj A] (X : D) [CategoryTheory.ModObj A X] (a b : ℕ) {Z : D} (h : modTensor A (modPowMod A X a) (modPowMod A X b) ⟶ Z) : CategoryTheory.CategoryStruct.comp (powMulDesc A X a b) (CategoryTheory.CategoryStruct.comp (powSplit A X a b) h) = h

The split is a retraction of the descended power multiplication.

noncomputable def RS.powMergeIso {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Z)] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.IsCommMonObj A] (X : D) [CategoryTheory.ModObj A X] (a b : ℕ) : modTensor A (modPowMod A X a) (modPowMod A X b) ≅ modPow A X (a + 1 + b + 1)

The merge isomorphism: the relative tensor product of two module powers is the module power of the summed arity, with the descended power multiplication as the forward direction and the split as its inverse.

Equations

• RS.powMergeIso A X a b = { hom := RS.powMulDesc A X a b, inv := RS.powSplit A X a b, hom_inv_id := ⋯, inv_hom_id := ⋯ }