Iso builders for the twisted power induction

Functoriality of the relative tensor and of the left twist on isomorphisms: the two transport devices consumed by the k-fold twisted power identification.

noncomputable def RS.tensorLeftModMapIso {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] (A : D) [CategoryTheory.MonObj A] {V V' : D} (e : V ≅ V') {M N : CategoryTheory.Mod D A} (f : M ≅ N) : tensorLeftMod A V M ≅ tensorLeftMod A V' N

The double twist transport: object and module isomorphisms together.

Equations

• RS.tensorLeftModMapIso A e f = RS.tensorLeftModContextIso A e M ≪≫ RS.tensorLeftModWhiskerIso A V' f

noncomputable def RS.modPowModZeroIso {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] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] (M : CategoryTheory.Mod D A) : modPowMod A M.X 0 ≅ M

The bottom power module is the module.

Equations

• RS.modPowModZeroIso A M = { hom := RS.fromModPowModZero A M, inv := RS.toModPowModZero A M, hom_inv_id := ⋯, inv_hom_id := ⋯ }

noncomputable def RS.powMergeModIso {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] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] (X : D) [CategoryTheory.ModObj A X] (k : ℕ) : modTensorMod A (modPowMod A X k) (modPowMod A X 0) ≅ modPowMod A X (k + 1)

The merge of adjacent power modules, as a module isomorphism.

Equations

• RS.powMergeModIso A X k = { hom := RS.powMulMod A X k 0, inv := RS.powMulModInv A X k 0, hom_inv_id := ⋯, inv_hom_id := ⋯ }

@[irreducible]

noncomputable def RS.twistPowModIso {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] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] (V : D) (R : CategoryTheory.Mod D A) (k : ℕ) : modPowMod A (tensorLeftMod A V R).X k ≅ tensorLeftMod A (tensorPow D V (k + 1)) (modPowMod A R.X k)

The twisted power identification: the relative powers of a twisted module are the twist of the powers by the tensor powers of the twisting object.

Equations

• One or more equations did not get rendered due to their size.
• RS.twistPowModIso A V R 0 = RS.modPowModZeroIso A (RS.tensorLeftMod A V R) ≪≫ RS.tensorLeftModMapIso A (CategoryTheory.MonoidalCategoryStruct.leftUnitor V).symm (RS.modPowModZeroIso A R).symm