The power pairing

For a Mod-internal duality datum on a pair of modules, the nested pairing of equal tensor powers: peel the innermost pair — the last factor of the M'-power against the first factor of the M-power — evaluate the datum, braid the scalar out, and multiply onto the pairing of the remaining powers. The pairing is defined at the raw tensor-power level by recursion on the arity; the descent obligations through the module-power and module-tensor coequalizers reduce, by the same recursion, to the datum's linearity and the commutativity of the monoid.

The datum's pairing at the raw tensor level

noncomputable def RS.pairRaw {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory 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.MonoidalCategoryStruct.tensorObj M'.X M.X ⟶ A

The datum's pairing evaluated on the raw tensor product.

Equations

• RS.pairRaw A M M' d = CategoryTheory.CategoryStruct.comp (RS.modTensorπ A M' M) d.pair

theorem RS.pairRaw_actLeft_fst {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory 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.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator A M'.X M.X).inv (CategoryTheory.MonoidalCategoryStruct.whiskerRight (actLeft A M'.X) M.X)) (pairRaw A M M' d) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (pairRaw A M M' d)) CategoryTheory.MonObj.mul

Raw linearity of the pairing in the M'-factor: acting on the first factor multiplies the scalar.

theorem RS.pairRaw_actLeft_fst_assoc {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory 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') {Z : D} (h : A ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator A M'.X M.X).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (actLeft A M'.X) M.X) (CategoryTheory.CategoryStruct.comp (pairRaw A M M' d) h)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (pairRaw A M M' d)) (CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.mul h)

Raw linearity of the pairing in the M'-factor: acting on the first factor multiplies the scalar.

theorem RS.pairRaw_slide {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory 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.whiskerRight (actRight A M'.X) M.X) (pairRaw A M M' d) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator M'.X A M.X).hom (CategoryTheory.MonoidalCategoryStruct.whiskerLeft M'.X (actLeft A M.X))) (pairRaw A M M' d)

The middle slide across the raw pairing: the braided right action on M' and the left action on M pair equally.

theorem RS.pairRaw_slide_assoc {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory 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') {Z : D} (h : A ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (actRight A M'.X) M.X) (CategoryTheory.CategoryStruct.comp (pairRaw A M M' d) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator M'.X A M.X).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft M'.X (actLeft A M.X)) (CategoryTheory.CategoryStruct.comp (pairRaw A M M' d) h))

The middle slide across the raw pairing: the braided right action on M' and the left action on M pair equally.

theorem RS.pairRaw_actRight_fst {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory 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.whiskerRight (actRight A M'.X) M.X) (pairRaw A M M' d) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (β_ M'.X A).hom M.X) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator A M'.X M.X).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (pairRaw A M M' d)) CategoryTheory.MonObj.mul))

Raw linearity through the braided right action: acting on the right of the M'-factor braids the scalar out to the left and multiplies.

theorem RS.pairRaw_actRight_fst_assoc {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory 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') {Z : D} (h : A ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (actRight A M'.X) M.X) (CategoryTheory.CategoryStruct.comp (pairRaw A M M' d) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (β_ M'.X A).hom M.X) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator A M'.X M.X).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (pairRaw A M M' d)) (CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.mul h)))

Raw linearity through the braided right action: acting on the right of the M'-factor braids the scalar out to the left and multiplies.

theorem RS.pairRaw_actLeft_snd {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory 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.whiskerLeft M'.X (actLeft A M.X)) (pairRaw A M M' d) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator M'.X A M.X).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (β_ M'.X A).hom M.X) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator A M'.X M.X).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (pairRaw A M M' d)) CategoryTheory.MonObj.mul)))

Raw linearity in the M-factor: acting on the left of the M-factor braids the scalar out to the left and multiplies.

theorem RS.pairRaw_actLeft_snd_assoc {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory 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') {Z : D} (h : A ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft M'.X (actLeft A M.X)) (CategoryTheory.CategoryStruct.comp (pairRaw A M M' d) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator M'.X A M.X).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (β_ M'.X A).hom M.X) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator A M'.X M.X).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (pairRaw A M M' d)) (CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.mul h))))

Raw linearity in the M-factor: acting on the left of the M-factor braids the scalar out to the left and multiplies.

The nested power pairing

noncomputable def RS.rawPair {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory 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.MonoidalCategoryStruct.tensorObj (tensorPow D M'.X n) (tensorPow D M.X n) ⟶ A

The nested power pairing at the raw tensor level, by recursion on the arity: at n + 1, peel the first factor of the M-power, pair it with the exposed last factor of the M'-power, braid the resulting scalar past the remaining M-power, and multiply it onto the pairing of the remaining powers.

Equations

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

theorem RS.rawPair_zero {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory 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') : rawPair A M M' d 0 = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit D)).hom CategoryTheory.MonObj.one

The base case of the power pairing.

theorem RS.rawPair_succ {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory 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 : ℕ) : rawPair A M M' d (n + 1) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (tensorPow D M'.X (n + 1)) (powPeel M.X n).hom) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator (tensorPow D M'.X n) M'.X (CategoryTheory.MonoidalCategoryStruct.tensorObj M.X (tensorPow D M.X n))).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (tensorPow D M'.X n) (CategoryTheory.MonoidalCategoryStruct.associator M'.X M.X (tensorPow D M.X n)).inv) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (tensorPow D M'.X n) (CategoryTheory.MonoidalCategoryStruct.whiskerRight (pairRaw A M M' d) (tensorPow D M.X n))) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (tensorPow D M'.X n) (β_ A (tensorPow D M.X n)).hom) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator (tensorPow D M'.X n) (tensorPow D M.X n) A).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (rawPair A M M' d n) A) CategoryTheory.MonObj.mul))))))

The recursion of the power pairing.

The generic pairing step

The recursion step of the power pairing, over an arbitrary continuation pairing: pair the exposed last M'-factor against the exposed head M-factor, braid the scalar past the remaining block, and fold it onto the continuation by multiplication. All extraction and naturality laws are proved at this generality, so that the inductions over the arity reduce to threading through the step.

noncomputable def RS.pairStep {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory 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') {Q R : D} (r : CategoryTheory.MonoidalCategoryStruct.tensorObj Q R ⟶ A) : CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj Q M'.X) (CategoryTheory.MonoidalCategoryStruct.tensorObj M.X R) ⟶ A

The generic recursion step of the power pairing.

Equations

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

theorem RS.rawPair_succ_step {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory 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 : ℕ) : rawPair A M M' d (n + 1) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (tensorPow D M'.X (n + 1)) (powPeel M.X n).hom) (pairStep A M M' d (rawPair A M M' d n))

The recursion of the power pairing through the generic step.

theorem RS.pairStep_precomp {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory 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') {Q' Q R : D} (f : Q' ⟶ Q) (r : CategoryTheory.MonoidalCategoryStruct.tensorObj Q R ⟶ A) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.whiskerRight f M'.X) (CategoryTheory.MonoidalCategoryStruct.tensorObj M.X R)) (pairStep A M M' d r) = pairStep A M M' d (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight f R) r)

Naturality of the step in the block variable.

theorem RS.pairStep_postcomp {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory 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') {Q R' R : D} (g : R' ⟶ R) (r : CategoryTheory.MonoidalCategoryStruct.tensorObj Q R ⟶ A) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (CategoryTheory.MonoidalCategoryStruct.tensorObj Q M'.X) (CategoryTheory.MonoidalCategoryStruct.whiskerLeft M.X g)) (pairStep A M M' d r) = pairStep A M M' d (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Q g) r)

Naturality of the step in the continuation variable.

Scalar extraction over a symmetric base

The descent obligations move an acted scalar across whole tensor blocks in both directions; the two routes agree only when the braiding is symmetric. The pairing calculus therefore runs over a symmetric base from here on — which is the generality of the Key Lemma itself. The section is fresh, so that the symmetric structure's braiding is the only braiding in scope.

theorem RS.concat_peel_head {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (X : D) (p q : ℕ) : CategoryTheory.CategoryStruct.comp (tensorPowConcat X (p + 1) q).hom (CategoryTheory.CategoryStruct.comp (powCast X ⋯) (powPeel X (p + q)).hom) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (powPeel X p).hom (tensorPow D X q)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X (tensorPow D X p) (tensorPow D X q)).hom (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (tensorPowConcat X p q).hom))

Concatenation against the head peel: concatenating onto a power with an exposed head factor and peeling the head of the result equals peeling the first block and concatenating the rest under the exposed factor.

theorem RS.braid_cross_pair {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] {S T Z : D} (C : D) (f : CategoryTheory.MonoidalCategoryStruct.tensorObj S T ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (β_ S C).hom T) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator C S T).hom (CategoryTheory.MonoidalCategoryStruct.whiskerLeft C f)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator S C T).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft S (β_ C T).hom) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator S T C).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight f C) (β_ Z C).hom)))

A strand crossing out to the left through an evaluated pairing may instead cross to the right and braid past the output.

theorem RS.pairRaw_actRight_out {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') : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (actRight A M'.X) M.X) (pairRaw A M M' d) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator M'.X A M.X).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft M'.X (β_ A M.X).hom) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator M'.X M.X A).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (pairRaw A M M' d) A) CategoryTheory.MonObj.mul)))

Scalar extraction at the pair: acting on the right of the M'-factor equals sliding the scalar rightwards past the M-factor, pairing, and multiplying from the right.

theorem RS.pairRaw_actRight_out_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] (M M' : CategoryTheory.Mod D A) (d : ModDualityDatum A M M') {Z : D} (h : A ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (actRight A M'.X) M.X) (CategoryTheory.CategoryStruct.comp (pairRaw A M M' d) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator M'.X A M.X).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft M'.X (β_ A M.X).hom) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator M'.X M.X A).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (pairRaw A M M' d) A) (CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.mul h))))

Scalar extraction at the pair: acting on the right of the M'-factor equals sliding the scalar rightwards past the M-factor, pairing, and multiplying from the right.

theorem RS.pairRaw_actLeft_out {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') : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft M'.X (actLeft A M.X)) (pairRaw A M M' d) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft M'.X (β_ A M.X).hom) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator M'.X M.X A).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (pairRaw A M M' d) A) CategoryTheory.MonObj.mul))

Scalar extraction at the pair, second slot: acting on the left of the M-factor equals sliding the scalar rightwards past the M-factor, pairing, and multiplying from the right.

theorem RS.pairRaw_actLeft_out_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] (M M' : CategoryTheory.Mod D A) (d : ModDualityDatum A M M') {Z : D} (h : A ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft M'.X (actLeft A M.X)) (CategoryTheory.CategoryStruct.comp (pairRaw A M M' d) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft M'.X (β_ A M.X).hom) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator M'.X M.X A).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (pairRaw A M M' d) A) (CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.mul h)))

Scalar extraction at the pair, second slot: acting on the left of the M-factor equals sliding the scalar rightwards past the M-factor, pairing, and multiplying from the right.

theorem RS.pairRaw_actRight_snd {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') : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft M'.X (actRight A M.X)) (pairRaw A M M' d) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator M'.X M.X A).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (pairRaw A M M' d) A) CategoryTheory.MonObj.mul)

Scalar extraction at the pair, second slot from the right: acting through the braided right action on the M-factor multiplies the pairing from the right, with no crossing at all.

theorem RS.pairRaw_actRight_snd_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] (M M' : CategoryTheory.Mod D A) (d : ModDualityDatum A M M') {Z : D} (h : A ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft M'.X (actRight A M.X)) (CategoryTheory.CategoryStruct.comp (pairRaw A M M' d) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator M'.X M.X A).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (pairRaw A M M' d) A) (CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.mul h))

Scalar extraction at the pair, second slot from the right: acting through the braided right action on the M-factor multiplies the pairing from the right, with no crossing at all.

theorem RS.rawPair_actRight_last {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 (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (tensorPow D M'.X n) (actRight A M'.X)) (tensorPow D M.X (n + 1))) (rawPair A M M' d (n + 1)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.associator (tensorPow D M'.X n) M'.X A).inv (tensorPow D M.X (n + 1))) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator (tensorPow D M'.X (n + 1)) A (tensorPow D M.X (n + 1))).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (tensorPow D M'.X (n + 1)) (β_ A (tensorPow D M.X (n + 1))).hom) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator (tensorPow D M'.X (n + 1)) (tensorPow D M.X (n + 1)) A).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (rawPair A M M' d (n + 1)) A) CategoryTheory.MonObj.mul))))

Scalar extraction at the last M'-factor: acting on the right of the exposed last factor of the M'-power equals braiding the scalar past the whole M-power and multiplying the pairing from the right.

theorem RS.pairStep_actRight {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') {Q R : D} (r : CategoryTheory.MonoidalCategoryStruct.tensorObj Q R ⟶ A) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Q (actRight A M'.X)) (CategoryTheory.MonoidalCategoryStruct.tensorObj M.X R)) (pairStep A M M' d r) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.associator Q M'.X A).inv (CategoryTheory.MonoidalCategoryStruct.tensorObj M.X R)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator (CategoryTheory.MonoidalCategoryStruct.tensorObj Q M'.X) A (CategoryTheory.MonoidalCategoryStruct.tensorObj M.X R)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (CategoryTheory.MonoidalCategoryStruct.tensorObj Q M'.X) (β_ A (CategoryTheory.MonoidalCategoryStruct.tensorObj M.X R)).hom) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator (CategoryTheory.MonoidalCategoryStruct.tensorObj Q M'.X) (CategoryTheory.MonoidalCategoryStruct.tensorObj M.X R) A).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (pairStep A M M' d r) A) CategoryTheory.MonObj.mul))))

Generic scalar extraction at the M'-slot of the step: acting through the braided right action on the exposed M'-factor equals braiding the scalar past the peeled block and multiplying the step from the right.

theorem RS.pairStep_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') {Q R : D} (r : CategoryTheory.MonoidalCategoryStruct.tensorObj Q R ⟶ A) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (CategoryTheory.MonoidalCategoryStruct.tensorObj Q M'.X) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator A M.X R).inv (CategoryTheory.MonoidalCategoryStruct.whiskerRight (actLeft A M.X) R))) (pairStep A M M' d r) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (CategoryTheory.MonoidalCategoryStruct.tensorObj Q M'.X) (β_ A (CategoryTheory.MonoidalCategoryStruct.tensorObj M.X R)).hom) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator (CategoryTheory.MonoidalCategoryStruct.tensorObj Q M'.X) (CategoryTheory.MonoidalCategoryStruct.tensorObj M.X R) A).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (pairStep A M M' d r) A) CategoryTheory.MonObj.mul))

Generic scalar extraction at the M-slot of the step: acting on the exposed head M-factor equals braiding the scalar past the peeled block and multiplying the step from the right.

theorem RS.actLeft_eq_braid_actRight {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] (A : D) [CategoryTheory.MonObj A] (X : D) [CategoryTheory.ModObj A X] : actLeft A X = CategoryTheory.CategoryStruct.comp (β_ A X).hom (actRight A X)

Over a symmetric base the left action is the braided right action after one crossing.

theorem RS.pairStep_actLeft_pair {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') {Q R : D} (r : CategoryTheory.MonoidalCategoryStruct.tensorObj Q R ⟶ A) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Q (actLeft A M'.X)) (CategoryTheory.MonoidalCategoryStruct.tensorObj M.X R)) (pairStep A M M' d r) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Q (β_ A M'.X).hom) (CategoryTheory.MonoidalCategoryStruct.tensorObj M.X R)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.associator Q M'.X A).inv (CategoryTheory.MonoidalCategoryStruct.tensorObj M.X R)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator (CategoryTheory.MonoidalCategoryStruct.tensorObj Q M'.X) A (CategoryTheory.MonoidalCategoryStruct.tensorObj M.X R)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (CategoryTheory.MonoidalCategoryStruct.tensorObj Q M'.X) (β_ A (CategoryTheory.MonoidalCategoryStruct.tensorObj M.X R)).hom) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator (CategoryTheory.MonoidalCategoryStruct.tensorObj Q M'.X) (CategoryTheory.MonoidalCategoryStruct.tensorObj M.X R) A).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (pairStep A M M' d r) A) CategoryTheory.MonObj.mul)))))

Generic scalar extraction at the M'-slot, for a scalar arriving from the left of the consumed factor.

theorem RS.pairStep_slide {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') {Q R : D} (r : CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj Q M'.X) R ⟶ A) (hr : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Q (actRight A M'.X)) R) r = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.associator Q M'.X A).inv R) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator (CategoryTheory.MonoidalCategoryStruct.tensorObj Q M'.X) A R).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (CategoryTheory.MonoidalCategoryStruct.tensorObj Q M'.X) (β_ A R).hom) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator (CategoryTheory.MonoidalCategoryStruct.tensorObj Q M'.X) R A).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight r A) CategoryTheory.MonObj.mul))))) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Q (winLegM A M'.X)) (CategoryTheory.MonoidalCategoryStruct.tensorObj M.X R)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.associator Q M'.X M'.X).inv (CategoryTheory.MonoidalCategoryStruct.tensorObj M.X R)) (pairStep A M M' d r)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Q (winLegN A M'.X)) (CategoryTheory.MonoidalCategoryStruct.tensorObj M.X R)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.associator Q M'.X M'.X).inv (CategoryTheory.MonoidalCategoryStruct.tensorObj M.X R)) (pairStep A M M' d r))

The top-slot slide law: for a continuation pairing that absorbs the braided right action on its last block factor — the extraction property of the power pairing — the two legs of the top slot window agree after the generic step.

theorem RS.rawPair_cast {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') {m n : ℕ} (h : m = n) : rawPair A M M' d m = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (powCast M'.X h) (tensorPow D M.X m)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (tensorPow D M'.X n) (powCast M.X h)) (rawPair A M M' d n))

Transport of the power pairing along an arity equality.

theorem RS.pairStep_slide_snd {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') {Q R : D} (r : CategoryTheory.MonoidalCategoryStruct.tensorObj Q R ⟶ A) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj Q M'.X) M'.X) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (winLegM A M.X) R) (CategoryTheory.MonoidalCategoryStruct.associator M.X M.X R).hom)) (pairStep A M M' d (pairStep A M M' d r)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj Q M'.X) M'.X) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (winLegN A M.X) R) (CategoryTheory.MonoidalCategoryStruct.associator M.X M.X R).hom)) (pairStep A M M' d (pairStep A M M' d r))

The head-slot slide law: the two legs of a slot window on the first two M-factors agree after the doubled generic step. The statement is closed — the continuation is arbitrary.

theorem RS.rawPair_rel_fst_top {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') (a : ℕ) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (modPowLegM A M'.X a 0) (tensorPow D M.X (a + 2))) (rawPair A M M' d (a + 2)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (modPowLegN A M'.X a 0) (tensorPow D M.X (a + 2))) (rawPair A M M' d (a + 2))

The top slot relation of the power pairing: at the slot touching the last two factors of the M'-power, the two legs pair equally.

theorem RS.rawPair_rel_fst {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') (a b : ℕ) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (modPowLegM A M'.X a b) (tensorPow D M.X (a + 2 + b))) (rawPair A M M' d (a + 2 + b)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (modPowLegN A M'.X a b) (tensorPow D M.X (a + 2 + b))) (rawPair A M M' d (a + 2 + b))

The first slot relations of the power pairing: at every slot of the M'-power, the two legs pair equally.

theorem RS.rawPair_rel_snd {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') (b a m : ℕ) (h : a + 2 + b = m) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (tensorPow D M'.X m) (CategoryTheory.CategoryStruct.comp (modPowLegM A M.X a b) (powCast M.X h))) (rawPair A M M' d m) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (tensorPow D M'.X m) (CategoryTheory.CategoryStruct.comp (modPowLegN A M.X a b) (powCast M.X h))) (rawPair A M M' d m)

The second slot relations of the power pairing: at every slot of the M-power, the two legs pair equally.

theorem RS.pairStep_ext {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') {Q R : D} (r : CategoryTheory.MonoidalCategoryStruct.tensorObj Q R ⟶ A) : pairStep A M M' d (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Q (β_ A R).hom) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator Q R A).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight r A) CategoryTheory.MonObj.mul))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (CategoryTheory.MonoidalCategoryStruct.tensorObj Q M'.X) (CategoryTheory.MonoidalCategoryStruct.whiskerLeft M.X (β_ A R).hom)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (CategoryTheory.MonoidalCategoryStruct.tensorObj Q M'.X) (CategoryTheory.MonoidalCategoryStruct.associator M.X R A).inv) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator (CategoryTheory.MonoidalCategoryStruct.tensorObj Q M'.X) (CategoryTheory.MonoidalCategoryStruct.tensorObj M.X R) A).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (pairStep A M M' d r) A) CategoryTheory.MonObj.mul)))

Extraction propagates through the step: the step over an extracted continuation is the extraction of the step, with the scalar crossing the continuation block.

theorem RS.rawPair_actTail {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.whiskerLeft (tensorPow D M'.X (n + 1)) (powTailAct A M.X n)) (rawPair A M M' d (n + 1)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (tensorPow D M'.X (n + 1)) (β_ A (tensorPow D M.X (n + 1))).hom) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator (tensorPow D M'.X (n + 1)) (tensorPow D M.X (n + 1)) A).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (rawPair A M M' d (n + 1)) A) CategoryTheory.MonObj.mul))

Scalar extraction at the tail of the M-power: the tail action on the M-power extracts as the scalar braiding past the whole power and multiplying the pairing from the right.

The descended pairing

The two-stage descent of the raw pairing through the module-power coequalizers, mirroring the descent of the raw multiplication: the slot relations assemble over the biproduct legs, the first stage descends the M'-power against the ambient M-power, and the second stage descends the M-power.

theorem RS.rawPair_rel_fst' {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') {m : ℕ} (a b : ℕ) (hab : a + 2 + b = m) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.CategoryStruct.comp (modPowLegM A M'.X a b) (powCast M'.X hab)) (tensorPow D M.X m)) (rawPair A M M' d m) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.CategoryStruct.comp (modPowLegN A M'.X a b) (powCast M'.X hab)) (tensorPow D M.X m)) (rawPair A M M' d m)

The first slot relations, in cast-carrying form.

noncomputable def RS.pairPowStage {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) [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.MonoidalPreadditive D] (d : ModDualityDatum A M M') (n : ℕ) : CategoryTheory.MonoidalCategoryStruct.tensorObj (modPow A M'.X n) (tensorPow D M.X n) ⟶ A

The first stage of the pairing descent: the raw pairing descends through the M'-power against the ambient M-power.

Equations

• RS.pairPowStage A M M' d n = RS.modPowWhiskerRightDesc A M'.X n (RS.tensorPow D M.X n) (RS.rawPair A M M' d n) ⋯

@[simp]

theorem RS.modPowπ_whiskerRight_pairPowStage {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) [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.MonoidalPreadditive D] (d : ModDualityDatum A M M') (n : ℕ) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (modPowπ A M'.X n) (tensorPow D M.X n)) (pairPowStage A M M' d n) = rawPair A M M' d n

Defining equation of the first stage.

@[simp]

theorem RS.modPowπ_whiskerRight_pairPowStage_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] (M M' : CategoryTheory.Mod D A) [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.MonoidalPreadditive D] (d : ModDualityDatum A M M') (n : ℕ) {Z : D} (h : A ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (modPowπ A M'.X n) (tensorPow D M.X n)) (CategoryTheory.CategoryStruct.comp (pairPowStage A M M' d n) h) = CategoryTheory.CategoryStruct.comp (rawPair A M M' d n) h

Defining equation of the first stage.

theorem RS.pairPowStage_cond {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) [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.MonoidalPreadditive D] (d : ModDualityDatum A M M') (n : ℕ) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (modPow A M'.X n) (modPowLegFst A M.X n)) (pairPowStage A M M' d n) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (modPow A M'.X n) (modPowLegSnd A M.X n)) (pairPowStage A M M' d n)

The first stage coequalizes the left-whiskered legs of the M-power.

noncomputable def RS.pairPow {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) [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.MonoidalPreadditive D] (d : ModDualityDatum A M M') (n : ℕ) : CategoryTheory.MonoidalCategoryStruct.tensorObj (modPow A M'.X n) (modPow A M.X n) ⟶ A

The descended power pairing on the module powers, in two stages.

Equations

• RS.pairPow A M M' d n = RS.modPowWhiskerLeftDesc A M.X (RS.modPow A M'.X n) n (RS.pairPowStage A M M' d n) ⋯

@[simp]

theorem RS.modPowπ_tensor_pairPow {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) [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.MonoidalPreadditive D] (d : ModDualityDatum A M M') (n : ℕ) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (modPowπ A M'.X n) (modPowπ A M.X n)) (pairPow A M M' d n) = rawPair A M M' d n

Defining equation of the descended pairing.

@[simp]

theorem RS.modPowπ_tensor_pairPow_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] (M M' : CategoryTheory.Mod D A) [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.MonoidalPreadditive D] (d : ModDualityDatum A M M') (n : ℕ) {Z : D} (h : A ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (modPowπ A M'.X n) (modPowπ A M.X n)) (CategoryTheory.CategoryStruct.comp (pairPow A M M' d n) h) = CategoryTheory.CategoryStruct.comp (rawPair A M M' d n) h

Defining equation of the descended pairing.

theorem RS.pairPow_middle_cond {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) [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.MonoidalPreadditive D] (d : ModDualityDatum A M M') (n : ℕ) : CategoryTheory.CategoryStruct.comp (modTensorLegM A (modPowMod A M'.X n) (modPowMod A M.X n)) (pairPow A M M' d (n + 1)) = CategoryTheory.CategoryStruct.comp (modTensorLegN A (modPowMod A M'.X n) (modPowMod A M.X n)) (pairPow A M M' d (n + 1))

The middle relation: the descended pairing coequalizes the module-tensor legs of the power bundles.

noncomputable def RS.modPowPairing {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) [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.MonoidalPreadditive D] (d : ModDualityDatum A M M') (n : ℕ) : modTensor A (modPowMod A M'.X n) (modPowMod A M.X n) ⟶ A

The Mod-internal power pairing: the descended pairing on the module tensor product of the power bundles.

Equations

• RS.modPowPairing A M M' d n = RS.modTensorDesc A (RS.modPowMod A M'.X n) (RS.modPowMod A M.X n) (RS.pairPow A M M' d (n + 1)) ⋯

@[simp]

theorem RS.modTensorπ_modPowPairing {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) [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.MonoidalPreadditive D] (d : ModDualityDatum A M M') (n : ℕ) : CategoryTheory.CategoryStruct.comp (modTensorπ A (modPowMod A M'.X n) (modPowMod A M.X n)) (modPowPairing A M M' d n) = pairPow A M M' d (n + 1)

Defining equation of the Mod-internal power pairing.

@[simp]

theorem RS.modTensorπ_modPowPairing_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] (M M' : CategoryTheory.Mod D A) [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.MonoidalPreadditive D] (d : ModDualityDatum A M M') (n : ℕ) {Z : D} (h : A ⟶ Z) : CategoryTheory.CategoryStruct.comp (modTensorπ A (modPowMod A M'.X n) (modPowMod A M.X n)) (CategoryTheory.CategoryStruct.comp (modPowPairing A M M' d n) h) = CategoryTheory.CategoryStruct.comp (pairPow A M M' d (n + 1)) h

Defining equation of the Mod-internal power pairing.

noncomputable def RS.symPowσMod {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.Limits.HasFiniteBiproducts D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Linear ℂ D] [CategoryTheory.MonoidalLinear ℂ D] {X : D} [CategoryTheory.ModObj A X] (n : ℕ) : symPowMod A X n ⟶ modPowMod A X n

The section of the symmetric power, as a morphism of modules.

Equations

• RS.symPowσMod A n = { hom := RS.symPowσ A X (n + 1), isModHom := ⋯ }

@[simp]

theorem RS.symPowσMod_hom {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.Limits.HasFiniteBiproducts D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Linear ℂ D] [CategoryTheory.MonoidalLinear ℂ D] {X : D} [CategoryTheory.ModObj A X] (n : ℕ) : (symPowσMod A n).hom = symPowσ A X (n + 1)

noncomputable def RS.symPowPairing {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) [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Linear ℂ D] [CategoryTheory.MonoidalLinear ℂ D] (d : ModDualityDatum A M M') (n : ℕ) : modTensor A (symPowMod A M'.X n) (symPowMod A M.X n) ⟶ A

The symmetric power pairing: the Mod-internal pairing on the symmetric powers, through the sections.

Equations

• RS.symPowPairing A M M' d n = CategoryTheory.CategoryStruct.comp (RS.modTensorMap A (RS.symPowσMod A n) (RS.symPowσMod A n)) (RS.modPowPairing A M M' d n)

@[simp]

theorem RS.modTensorπ_symPowPairing {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) [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Linear ℂ D] [CategoryTheory.MonoidalLinear ℂ D] (d : ModDualityDatum A M M') (n : ℕ) : CategoryTheory.CategoryStruct.comp (modTensorπ A (symPowMod A M'.X n) (symPowMod A M.X n)) (symPowPairing A M M' d n) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (symPowσ A M'.X (n + 1)) (symPowσ A M.X (n + 1))) (pairPow A M M' d (n + 1))

Defining equation of the symmetric power pairing.

@[simp]

theorem RS.modTensorπ_symPowPairing_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] (M M' : CategoryTheory.Mod D A) [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Linear ℂ D] [CategoryTheory.MonoidalLinear ℂ D] (d : ModDualityDatum A M M') (n : ℕ) {Z : D} (h : A ⟶ Z) : CategoryTheory.CategoryStruct.comp (modTensorπ A (symPowMod A M'.X n) (symPowMod A M.X n)) (CategoryTheory.CategoryStruct.comp (symPowPairing A M M' d n) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (symPowσ A M'.X (n + 1)) (symPowσ A M.X (n + 1))) (pairPow A M M' d (n + 1))) h

Defining equation of the symmetric power pairing.