The triangle scalar of the power chain

The copairing powers of a duality datum retract against the nested power pairing: under the scalar zigzag, the pairing evaluates every chain unit to the unit of the base. This is the nonvanishing engine of the Key Lemma's chain.

theorem RS.modTensorMap_swap {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Limits.HasCoequalizers D] (A : D) [CategoryTheory.MonObj A] {P P' Q Q' : CategoryTheory.Mod D A} (f : P ⟶ P') (g : Q ⟶ Q') : CategoryTheory.CategoryStruct.comp (modTensorMap A f g) (modTensorSwap A P' Q') = CategoryTheory.CategoryStruct.comp (modTensorSwap A P Q) (modTensorMap A g f)

The braiding of the module tensor product is natural.

theorem RS.modPowOne_pairPow {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] (M M' : CategoryTheory.Mod D A) (d : ModDualityDatum A M M') : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (modPowOne A M'.X).inv (modPowOne A M.X).inv) (pairPow A M M' d 1) = pairRaw A M M' d

The nested pairing at arity one is the pairing, through the singleton isomorphisms.

theorem RS.toZero_modPowPairing {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] (M M' : CategoryTheory.Mod D A) (d : ModDualityDatum A M M') : CategoryTheory.CategoryStruct.comp (modTensorMap A (toModPowModZero A M') (toModPowModZero A M)) (modPowPairing A M M' d 0) = d.pair

The Mod-internal power pairing at arity zero is the datum's pairing, through the singleton stages.

theorem RS.powSeed_pairing {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] (M M' : CategoryTheory.Mod D A) (d : ModDualityDatum A M M') (hzig : CategoryTheory.CategoryStruct.comp d.copair (CategoryTheory.CategoryStruct.comp (modTensorSwap A M M') d.pair) = CategoryTheory.CategoryStruct.id A) : CategoryTheory.CategoryStruct.comp (powSeed A M M' d) (CategoryTheory.CategoryStruct.comp (modTensorSwap A (modPowMod A M.X 0) (modPowMod A M'.X 0)) (modPowPairing A M M' d 0)) = CategoryTheory.MonObj.one

The seed retracts against the pairing: under the scalar zigzag, the bottom chain unit evaluates to the unit of the base.

instance RS.epi_modPowπ {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] (n : ℕ) : CategoryTheory.Epi (modPowπ A X n)

The module-power projection is an epimorphism.

instance RS.epi_modPowπ_tensorHom {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] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Z)] (A : D) [CategoryTheory.MonObj A] (X : D) [CategoryTheory.ModObj A X] (Y : D) [CategoryTheory.ModObj A Y] (m n : ℕ) : CategoryTheory.Epi (CategoryTheory.MonoidalCategoryStruct.tensorHom (modPowπ A X m) (modPowπ A Y n))

The tensor product of two module-power projections is an epimorphism.

instance RS.epi_modPowπ_tensorHom_whiskerRight {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] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Z)] (A : D) [CategoryTheory.MonObj A] (X : D) [CategoryTheory.ModObj A X] (Y : D) [CategoryTheory.ModObj A Y] (m n : ℕ) (W : D) : CategoryTheory.Epi (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.tensorHom (modPowπ A X m) (modPowπ A Y n)) W)

A tensor pair of power projections whiskered on the right is an epimorphism.

instance RS.epi_modPowπ_tensorHom_tensorHom {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] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Z)] (A : D) [CategoryTheory.MonObj A] (X : D) [CategoryTheory.ModObj A X] (Y : D) [CategoryTheory.ModObj A Y] (Z' W' : D) [CategoryTheory.ModObj A Z'] [CategoryTheory.ModObj A W'] (a b c e : ℕ) : CategoryTheory.Epi (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.MonoidalCategoryStruct.tensorHom (modPowπ A X a) (modPowπ A Y b)) (CategoryTheory.MonoidalCategoryStruct.tensorHom (modPowπ A Z' c) (modPowπ A W' e)))

A tensor square of power projection pairs is an epimorphism.

instance RS.epi_whiskerLeft_modPowπ_whiskerRight' {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] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Z)] (A : D) [CategoryTheory.MonObj A] (X : D) [CategoryTheory.ModObj A X] (n : ℕ) (Q W : D) : CategoryTheory.Epi (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Q (modPowπ A X n)) W)

A left-whiskered power projection whiskered on the right is an epimorphism.

theorem RS.tensorHom_π_interchange_map {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)] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorRight Z)] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.IsCommMonObj A] (N₁ N₂ P₁ P₂ : CategoryTheory.Mod D A) {Q R : CategoryTheory.Mod D A} (f : modTensorMod A N₁ P₁ ⟶ Q) (g : modTensorMod A N₂ P₂ ⟶ R) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (modTensorπ A N₁ N₂) (modTensorπ A P₁ P₂)) (CategoryTheory.CategoryStruct.comp (interchange A N₁ N₂ P₁ P₂) (modTensorMap A f g)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorμ N₁.X N₂.X P₁.X P₂.X) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.CategoryStruct.comp (modTensorπ A N₁ P₁) f.hom) (CategoryTheory.CategoryStruct.comp (modTensorπ A N₂ P₂) g.hom)) (modTensorπ A Q R))

The interchange followed by a functorial map computes under the stage projections: the raw crossing feeds the two module maps.

theorem RS.tensorHom_π_interchange_map_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)] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorRight Z)] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.IsCommMonObj A] (N₁ N₂ P₁ P₂ : CategoryTheory.Mod D A) {Q R : CategoryTheory.Mod D A} (f : modTensorMod A N₁ P₁ ⟶ Q) (g : modTensorMod A N₂ P₂ ⟶ R) {Z : D} (h : modTensor A Q R ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (modTensorπ A N₁ N₂) (modTensorπ A P₁ P₂)) (CategoryTheory.CategoryStruct.comp (interchange A N₁ N₂ P₁ P₂) (CategoryTheory.CategoryStruct.comp (modTensorMap A f g) h)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorμ N₁.X N₂.X P₁.X P₂.X) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.CategoryStruct.comp (modTensorπ A N₁ P₁) f.hom) (CategoryTheory.CategoryStruct.comp (modTensorπ A N₂ P₂) g.hom)) (CategoryTheory.CategoryStruct.comp (modTensorπ A Q R) h))

The interchange followed by a functorial map computes under the stage projections: the raw crossing feeds the two module maps.

theorem RS.powDeltaCore_pairing {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 (interchange A (modPowMod A M.X n) (modPowMod A M'.X n) (modPowMod A M.X 0) (modPowMod A M'.X 0)) (CategoryTheory.CategoryStruct.comp (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)) (CategoryTheory.CategoryStruct.comp (modTensorSwap A (modPowMod A M.X (n + 1)) (modPowMod A M'.X (n + 1))) (modPowPairing A M M' d (n + 1)))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.CategoryStruct.comp (modTensorSwap A (modPowMod A M.X n) (modPowMod A M'.X n)) (modPowPairing A M M' d n)) (CategoryTheory.CategoryStruct.comp (modTensorSwap A (modPowMod A M.X 0) (modPowMod A M'.X 0)) (modPowPairing A M M' d 0))) CategoryTheory.MonObj.mul

Multiplicativity of the pairing against the transition core: the interchange followed by the aligned multiplications and the pairing of the joined stage evaluates as the product of the stage pairings.

theorem RS.powDelta_pairing {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') (hzig : CategoryTheory.CategoryStruct.comp d.copair (CategoryTheory.CategoryStruct.comp (modTensorSwap A M M') d.pair) = CategoryTheory.CategoryStruct.id A) (n : ℕ) : CategoryTheory.CategoryStruct.comp (powDelta A M M' d n) (CategoryTheory.CategoryStruct.comp (modTensorSwap A (modPowMod A M.X (n + 1)) (modPowMod A M'.X (n + 1))) (modPowPairing A M M' d (n + 1))) = CategoryTheory.CategoryStruct.comp (modTensorSwap A (modPowMod A M.X n) (modPowMod A M'.X n)) (modPowPairing A M M' d n)

The transition retracts against the pairing: under the scalar zigzag, one insertion peels off against one zigzag.

theorem RS.powUnitStage_pairing {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') (hzig : CategoryTheory.CategoryStruct.comp d.copair (CategoryTheory.CategoryStruct.comp (modTensorSwap A M M') d.pair) = CategoryTheory.CategoryStruct.id A) (n : ℕ) : CategoryTheory.CategoryStruct.comp (powUnitStage A M M' d n) (CategoryTheory.CategoryStruct.comp (modTensorSwap A (modPowMod A M.X n) (modPowMod A M'.X n)) (modPowPairing A M M' d n)) = CategoryTheory.MonObj.one

The chain units retract against the pairing: every copairing power evaluates to the unit of the base.

theorem RS.rawPair_actHead {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] (M M' : CategoryTheory.Mod D A) (d : ModDualityDatum A M M') (n : ℕ) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (powTailAct A M'.X n) (tensorPow D M.X (n + 1))) (rawPair A M M' d (n + 1)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator A (tensorPow D M'.X (n + 1)) (tensorPow D M.X (n + 1))).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (rawPair A M M' d (n + 1))) CategoryTheory.MonObj.mul)

Scalar extraction at the head of the M'-power: the tail action on the M'-power extracts as the scalar multiplying the pairing from the left.

theorem RS.pairPow_actHead {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] (M M' : CategoryTheory.Mod D A) (d : ModDualityDatum A M M') (n : ℕ) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (modPowAct A M'.X n) (modPow A M.X (n + 1))) (pairPow A M M' d (n + 1)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator A (modPow A M'.X (n + 1)) (modPow A M.X (n + 1))).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (pairPow A M M' d (n + 1))) CategoryTheory.MonObj.mul)

The head action extracts through the descended pairing.

theorem RS.modPowPairing_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)] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.IsCommMonObj A] (M M' : CategoryTheory.Mod D A) (d : ModDualityDatum A M M') (n : ℕ) : CategoryTheory.CategoryStruct.comp (actLeft A (modTensor A (modPowMod A M'.X n) (modPowMod A M.X n))) (modPowPairing A M M' d n) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (modPowPairing A M M' d n)) CategoryTheory.MonObj.mul

The power pairing is linear: it is a map of modules into the regular module.