The successor power datum #
The step of the power induction: the copairing power at the successor stage is the tensor copairing of the stage datum and the bottom datum, pushed along the transition legs. The orbit extension principle reduces the comparison to the unit elements, where the chain recursion is definitional.
theorem
RS.act_on_point_eq
{D : Type u}
[CategoryTheory.Category.{v, u} D]
[CategoryTheory.MonoidalCategory D]
(A : D)
[CategoryTheory.MonObj A]
{X : D}
(act : CategoryTheory.MonoidalCategoryStruct.tensorObj A X ⟶ X)
(f : A ⟶ X)
(hf :
CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.mul f = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A f) act)
:
The orbit extension principle: a linear map out of the base is the orbit map of its unit element.
theorem
RS.powDelta_actLeft
{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)]
[∀ (Z : D),
CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair
(CategoryTheory.MonoidalCategory.tensorRight Z)]
(A : D)
[CategoryTheory.MonObj A]
[CategoryTheory.IsCommMonObj A]
(M M' : CategoryTheory.Mod D A)
(d : ModDualityDatum A M M')
(n : ℕ)
:
CategoryTheory.CategoryStruct.comp (modTensorAct A (modPowMod A M.X n) (modPowMod A M'.X n)) (powDelta A M M' d n) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (powDelta A M M' d n))
(modTensorAct A (modPowMod A M.X (n + 1)) (modPowMod A M'.X (n + 1)))
The transition is linear: the power chain transition intertwines the descended actions of adjacent stages.
theorem
RS.powCopairA_succ_tensor
{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)]
[∀ (Z : D),
CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair
(CategoryTheory.MonoidalCategory.tensorRight Z)]
(A : D)
[CategoryTheory.MonObj A]
[CategoryTheory.IsCommMonObj A]
(M M' : CategoryTheory.Mod D A)
(d : ModDualityDatum A M M')
(n : ℕ)
:
powCopairA A M M' d (n + 1) = CategoryTheory.CategoryStruct.comp (tensorCopair A (powDualityDatum A M M' d n) (powDualityDatum A M M' d 0))
(modTensorMap A
(CategoryTheory.CategoryStruct.comp (modTensorSwapMod A (modPowMod A M.X n) (modPowMod A M.X 0))
(CategoryTheory.CategoryStruct.comp (powMulMod A M.X 0 n) (modPowCastMod A M.X ⋯)))
(powMulMod A M'.X n 0))
The successor copairing power is the tensor copairing pushed along the transition legs (Deligne 1.15, copair side of the power step).