The power duality datum

The tensor powers of a dual pair of modules form a dual pair: the power pairing and the copairing power assemble into a ModDualityDatum at every level. The pairing's linearity is modPowPairing_linear; the copairing's linearity is proved here from the associativity of the descended action, since the copairing power is the action on the unit-stage element.

The zigzag laws for the power datum — the inheritance of the triangle identities up the powers — are the peel induction and live separately; once available, ZigzagNonzero applied to the power datum detects the nonvanishing of the copairing powers from the nonvanishing of the power modules.

theorem RS.act_on_point_linear {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) (hact : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.mul X) act = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator A A X).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A act) act)) (u : CategoryTheory.MonoidalCategoryStruct.tensorUnit D ⟶ X) : CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.mul (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor A).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A u) act)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor A).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A u) act))) act

Acting on a point is linear: for an associative action on a carrier, the orbit map of a global point is a module map from the regular module. Stated over an abstract carrier so that instantiations at definitional wrappers stay uniformly typed.

theorem RS.act_on_point_unit {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) (hone : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.one X) act = (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).hom) (u : CategoryTheory.MonoidalCategoryStruct.tensorUnit D ⟶ X) : CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.one (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor A).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A u) act)) = u

The orbit map returns the point at the unit: for a unital action, evaluating the orbit map of a global point at the monoid unit recovers the point.

theorem RS.powCopairA_unit {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 CategoryTheory.MonObj.one (powCopairA A M M' d n) = powUnitStage A M M' d n

The unit of the copairing power is the unit stage: the copair element of the power datum is the chain unit.

theorem RS.powCopairA_linear {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 CategoryTheory.MonObj.mul (powCopairA A M M' d n) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (powCopairA A M M' d n)) (actLeft A (modTensor A (modPowMod A M.X n) (modPowMod A M'.X n)))

The copairing power is linear: the copairing power is the action on the unit-stage element, so its linearity is the associativity of the descended action.

noncomputable def RS.powDualityDatum {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 : ℕ) : ModDualityDatum A (modPowMod A M.X n) (modPowMod A M'.X n)

The power duality datum: the tensor powers of a dual pair form a dual pair, with the power pairing and the copairing power.

Equations

• RS.powDualityDatum A M M' d n = { pair := RS.modPowPairing A M M' d n, copair := RS.powCopairA A M M' d n, pair_linear := ⋯, copair_linear := ⋯ }