Module-level inverses of the merge maps

The merge isomorphism of PowMerge.lean upgrades to the category of modules: the split intertwines the actions, so it bundles as a module map inverse to the bundled power multiplication powMulMod. From it, the two insertions of a single factor into a module power — at the front, through the braiding, and at the back — become isomorphisms of modules.

• powMulModInv: the split as a map of modules, with the roundtrips powMulMod_powMulModInv and powMulModInv_powMulMod.
• powFrontMod/powFrontModInv: the front insertion — the M-side leg of the chain transition powDelta — and its inverse, with roundtrips.
• powBackMod/powBackModInv: the back insertion and its inverse, with roundtrips.

The split as a module map

theorem RS.powSplit_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] (a b : ℕ) : CategoryTheory.CategoryStruct.comp (modPowAct A X (a + 1 + b)) (powSplit A X a b) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (powSplit A X a b)) (modTensorAct A (modPowMod A X a) (modPowMod A X b))

The split intertwines the module actions: the inverse of an equivariant isomorphism is equivariant, by cancelling the descended power multiplication on the right.

noncomputable def RS.powMulModInv {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 : ℕ) : modPowMod A X (a + 1 + b) ⟶ modTensorMod A (modPowMod A X a) (modPowMod A X b)

The module-level inverse of the merge: the split bundled as a map of modules.

Equations

• RS.powMulModInv A X a b = CategoryTheory.Mod.Hom.mk' (RS.powSplit A X a b) ⋯

@[simp]

theorem RS.powMulMod_powMulModInv {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 (powMulMod A X a b) (powMulModInv A X a b) = CategoryTheory.CategoryStruct.id (modTensorMod A (modPowMod A X a) (modPowMod A X b))

The bundled merge and its inverse compose to the identity on the module tensor product.

@[simp]

theorem RS.powMulMod_powMulModInv_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 : CategoryTheory.Mod D A} (h : modTensorMod A (modPowMod A X a) (modPowMod A X b) ⟶ Z) : CategoryTheory.CategoryStruct.comp (powMulMod A X a b) (CategoryTheory.CategoryStruct.comp (powMulModInv A X a b) h) = h

The bundled merge and its inverse compose to the identity on the module tensor product.

@[simp]

theorem RS.powMulModInv_powMulMod {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 (powMulModInv A X a b) (powMulMod A X a b) = CategoryTheory.CategoryStruct.id (modPowMod A X (a + 1 + b))

The bundled inverse and the merge compose to the identity on the module power.

@[simp]

theorem RS.powMulModInv_powMulMod_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 : CategoryTheory.Mod D A} (h : modPowMod A X (a + 1 + b) ⟶ Z) : CategoryTheory.CategoryStruct.comp (powMulModInv A X a b) (CategoryTheory.CategoryStruct.comp (powMulMod A X a b) h) = h

The bundled inverse and the merge compose to the identity on the module power.

Transport and braiding helpers at the module level

@[simp]

theorem RS.modPowCastMod_comp_id {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 : ℕ} (h : a + 1 = b + 1) (h' : b + 1 = a + 1) : CategoryTheory.CategoryStruct.comp (modPowCastMod A X h) (modPowCastMod A X h') = CategoryTheory.CategoryStruct.id (modPowMod A X a)

Two opposite arity transports of module powers cancel.

@[simp]

theorem RS.modPowCastMod_comp_id_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 : ℕ} (h : a + 1 = b + 1) (h' : b + 1 = a + 1) {Z : CategoryTheory.Mod D A} (h✝ : modPowMod A X a ⟶ Z) : CategoryTheory.CategoryStruct.comp (modPowCastMod A X h) (CategoryTheory.CategoryStruct.comp (modPowCastMod A X h') h✝) = h✝

Two opposite arity transports of module powers cancel.

@[simp]

theorem RS.modTensorSwapMod_modTensorSwapMod {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory 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] (P Q : CategoryTheory.Mod D A) : CategoryTheory.CategoryStruct.comp (modTensorSwapMod A P Q) (modTensorSwapMod A Q P) = CategoryTheory.CategoryStruct.id (modTensorMod A P Q)

The braiding of the module tensor product is an involution at the module level.

@[simp]

theorem RS.modTensorSwapMod_modTensorSwapMod_assoc {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory 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] (P Q : CategoryTheory.Mod D A) {Z : CategoryTheory.Mod D A} (h : modTensorMod A P Q ⟶ Z) : CategoryTheory.CategoryStruct.comp (modTensorSwapMod A P Q) (CategoryTheory.CategoryStruct.comp (modTensorSwapMod A Q P) h) = h

The braiding of the module tensor product is an involution at the module level.

The front insertion

noncomputable def RS.powFrontMod {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] (n : ℕ) : modTensorMod A (modPowMod A X n) (modPowMod A X 0) ⟶ modPowMod A X (n + 1)

The front insertion: merge a fresh factor onto the front of a module power, through the braiding. This is the M-side leg of the chain transition powDelta.

Equations

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

noncomputable def RS.powFrontModInv {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] (n : ℕ) : modPowMod A X (n + 1) ⟶ modTensorMod A (modPowMod A X n) (modPowMod A X 0)

The inverse of the front insertion.

Equations

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

@[simp]

theorem RS.powFrontMod_powFrontModInv {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] (n : ℕ) : CategoryTheory.CategoryStruct.comp (powFrontMod A X n) (powFrontModInv A X n) = CategoryTheory.CategoryStruct.id (modTensorMod A (modPowMod A X n) (modPowMod A X 0))

The front insertion and its inverse compose to the identity on the module tensor product.

@[simp]

theorem RS.powFrontMod_powFrontModInv_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] (n : ℕ) {Z : CategoryTheory.Mod D A} (h : modTensorMod A (modPowMod A X n) (modPowMod A X 0) ⟶ Z) : CategoryTheory.CategoryStruct.comp (powFrontMod A X n) (CategoryTheory.CategoryStruct.comp (powFrontModInv A X n) h) = h

The front insertion and its inverse compose to the identity on the module tensor product.

@[simp]

theorem RS.powFrontModInv_powFrontMod {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] (n : ℕ) : CategoryTheory.CategoryStruct.comp (powFrontModInv A X n) (powFrontMod A X n) = CategoryTheory.CategoryStruct.id (modPowMod A X (n + 1))

The inverse of the front insertion and the front insertion compose to the identity on the module power.

@[simp]

theorem RS.powFrontModInv_powFrontMod_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] (n : ℕ) {Z : CategoryTheory.Mod D A} (h : modPowMod A X (n + 1) ⟶ Z) : CategoryTheory.CategoryStruct.comp (powFrontModInv A X n) (CategoryTheory.CategoryStruct.comp (powFrontMod A X n) h) = h

The inverse of the front insertion and the front insertion compose to the identity on the module power.

The back insertion

noncomputable def RS.powBackMod {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] (n : ℕ) : modTensorMod A (modPowMod A X n) (modPowMod A X 0) ⟶ modPowMod A X (n + 1)

The back insertion: merge a fresh factor onto the back of a module power — the bundled merge with a singleton right block.

Equations

• RS.powBackMod A X n = RS.powMulMod A X n 0

noncomputable def RS.powBackModInv {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] (n : ℕ) : modPowMod A X (n + 1) ⟶ modTensorMod A (modPowMod A X n) (modPowMod A X 0)

The inverse of the back insertion.

Equations

• RS.powBackModInv A X n = RS.powMulModInv A X n 0

@[simp]

theorem RS.powBackMod_powBackModInv {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] (n : ℕ) : CategoryTheory.CategoryStruct.comp (powBackMod A X n) (powBackModInv A X n) = CategoryTheory.CategoryStruct.id (modTensorMod A (modPowMod A X n) (modPowMod A X 0))

The back insertion and its inverse compose to the identity on the module tensor product.

@[simp]

theorem RS.powBackMod_powBackModInv_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] (n : ℕ) {Z : CategoryTheory.Mod D A} (h : modTensorMod A (modPowMod A X n) (modPowMod A X 0) ⟶ Z) : CategoryTheory.CategoryStruct.comp (powBackMod A X n) (CategoryTheory.CategoryStruct.comp (powBackModInv A X n) h) = h

The back insertion and its inverse compose to the identity on the module tensor product.

@[simp]

theorem RS.powBackModInv_powBackMod {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] (n : ℕ) : CategoryTheory.CategoryStruct.comp (powBackModInv A X n) (powBackMod A X n) = CategoryTheory.CategoryStruct.id (modPowMod A X (n + 1))

The inverse of the back insertion and the back insertion compose to the identity on the module power.

@[simp]

theorem RS.powBackModInv_powBackMod_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] (n : ℕ) {Z : CategoryTheory.Mod D A} (h : modPowMod A X (n + 1) ⟶ Z) : CategoryTheory.CategoryStruct.comp (powBackModInv A X n) (CategoryTheory.CategoryStruct.comp (powBackMod A X n) h) = h

The inverse of the back insertion and the back insertion compose to the identity on the module power.