The power copairing

The mirror of the power pairing: the copairing side of a Mod-internal duality datum. The copairing lands in the quotient modTensor A M M', so there is no raw section; every primitive lives at the descended level. The file provides the copairing unit copairUnit — the seed of the chain units of the Key Lemma — with its linearity laws, the braiding modTensorSwap of the module tensor product with its defining equation, involution and module-linearity, and the zigzag scalar zig together with the retraction law: under the zigzag identity of the datum the scalar is the unit of the base. The retraction is the nonvanishing engine of the Key Lemma's chain: a vanishing chain unit forces the unit of the base to vanish.

The copairing unit

noncomputable def RS.copairUnit {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.tensorUnit D ⟶ modTensor A M M'

The copairing unit: the copairing of the datum evaluated at the unit of the base. The seed of the chain units of the Key Lemma.

Equations

• RS.copairUnit A M M' d = CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.one d.copair

theorem RS.copair_act {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.MonObj.mul d.copair = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A d.copair) (modTensorAct A M M')

Linearity of the copairing, phrased at the descended action: multiplying before the copairing is acting after it.

theorem RS.copair_act_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 : modTensor A M M' ⟶ Z) : CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.mul (CategoryTheory.CategoryStruct.comp d.copair h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A d.copair) (CategoryTheory.CategoryStruct.comp (modTensorAct A M M') h)

Linearity of the copairing, phrased at the descended action: multiplying before the copairing is acting after it.

theorem RS.copair_braid_act {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 d.copair A) (CategoryTheory.CategoryStruct.comp (β_ (modTensor A M M') A).hom (modTensorAct A M M')) = CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.mul d.copair

Linearity through the braided right action: the copairing carries right multiplication to the braided right action on the module tensor product.

theorem RS.copair_braid_act_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 : modTensor A M M' ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight d.copair A) (CategoryTheory.CategoryStruct.comp (β_ (modTensor A M M') A).hom (CategoryTheory.CategoryStruct.comp (modTensorAct A M M') h)) = CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.mul (CategoryTheory.CategoryStruct.comp d.copair h)

Linearity through the braided right action: the copairing carries right multiplication to the braided right action on the module tensor product.

theorem RS.copairUnit_act {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 A (copairUnit A M M' d)) (modTensorAct A M M') = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor A).hom d.copair

The action on the copairing unit collapses onto the copairing: the copairing unit is a relative invariant of the module tensor product.

theorem RS.copairUnit_act_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 : modTensor A M M' ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (copairUnit A M M' d)) (CategoryTheory.CategoryStruct.comp (modTensorAct A M M') h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor A).hom (CategoryTheory.CategoryStruct.comp d.copair h)

The action on the copairing unit collapses onto the copairing: the copairing unit is a relative invariant of the module tensor product.

The braiding of the module tensor product

The copairing is consumed against the pairing through the braiding of the module tensor product: the braiding of the underlying factors descends through the coequalizers, the relation carried across by the window exchange of ModCross. The exchange swaps the two legs, so the two-sided descent needs the symmetric base — the generality of the Key Lemma itself.

noncomputable def RS.modTensorSwap {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Limits.HasCoequalizers D] (A : D) [CategoryTheory.MonObj A] (M N : CategoryTheory.Mod D A) : modTensor A M N ⟶ modTensor A N M

The braiding of the module tensor product: the braiding of the underlying factors descends through the coequalizers, the relation carried across by the window exchange.

Equations

• RS.modTensorSwap A M N = RS.modTensorDesc A M N (CategoryTheory.CategoryStruct.comp (β_ M.X N.X).hom (RS.modTensorπ A N M)) ⋯

@[simp]

theorem RS.modTensorπ_swap {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Limits.HasCoequalizers D] (A : D) [CategoryTheory.MonObj A] (M N : CategoryTheory.Mod D A) : CategoryTheory.CategoryStruct.comp (modTensorπ A M N) (modTensorSwap A M N) = CategoryTheory.CategoryStruct.comp (β_ M.X N.X).hom (modTensorπ A N M)

Defining equation of the braiding of the module tensor product: on the projection it is the braiding of the factors.

@[simp]

theorem RS.modTensorπ_swap_assoc {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Limits.HasCoequalizers D] (A : D) [CategoryTheory.MonObj A] (M N : CategoryTheory.Mod D A) {Z : D} (h : modTensor A N M ⟶ Z) : CategoryTheory.CategoryStruct.comp (modTensorπ A M N) (CategoryTheory.CategoryStruct.comp (modTensorSwap A M N) h) = CategoryTheory.CategoryStruct.comp (β_ M.X N.X).hom (CategoryTheory.CategoryStruct.comp (modTensorπ A N M) h)

Defining equation of the braiding of the module tensor product: on the projection it is the braiding of the factors.

@[simp]

theorem RS.modTensorSwap_modTensorSwap {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Limits.HasCoequalizers D] (A : D) [CategoryTheory.MonObj A] (M N : CategoryTheory.Mod D A) : CategoryTheory.CategoryStruct.comp (modTensorSwap A M N) (modTensorSwap A N M) = CategoryTheory.CategoryStruct.id (modTensor A M N)

The braiding of the module tensor product is an involution.

@[simp]

theorem RS.modTensorSwap_modTensorSwap_assoc {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Limits.HasCoequalizers D] (A : D) [CategoryTheory.MonObj A] (M N : CategoryTheory.Mod D A) {Z : D} (h : modTensor A M N ⟶ Z) : CategoryTheory.CategoryStruct.comp (modTensorSwap A M N) (CategoryTheory.CategoryStruct.comp (modTensorSwap A N M) h) = h

The braiding of the module tensor product is an involution.

theorem RS.modTensorAct_swap {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Limits.HasCoequalizers D] (A : D) [CategoryTheory.MonObj A] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Z)] [CategoryTheory.IsCommMonObj A] (M N : CategoryTheory.Mod D A) : CategoryTheory.CategoryStruct.comp (modTensorAct A M N) (modTensorSwap A M N) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (modTensorSwap A M N)) (modTensorAct A N M)

The braiding of the module tensor product is a module map: it intertwines the descended actions.

theorem RS.modTensorAct_swap_assoc {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Limits.HasCoequalizers D] (A : D) [CategoryTheory.MonObj A] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Z)] [CategoryTheory.IsCommMonObj A] (M N : CategoryTheory.Mod D A) {Z : D} (h : modTensor A N M ⟶ Z) : CategoryTheory.CategoryStruct.comp (modTensorAct A M N) (CategoryTheory.CategoryStruct.comp (modTensorSwap A M N) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (modTensorSwap A M N)) (CategoryTheory.CategoryStruct.comp (modTensorAct A N M) h)

The braiding of the module tensor product is a module map: it intertwines the descended actions.

The zigzag scalar and the retraction law

The composite of the copairing with the pairing through the braiding of the module tensor product. The zigzag identity of the datum — Deligne's (1.15.1) duality — is taken as a hypothesis; it is not derivable from the bare datum.

noncomputable def RS.zig {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Limits.HasCoequalizers D] (A : D) [CategoryTheory.MonObj A] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Z)] [CategoryTheory.IsCommMonObj A] (M M' : CategoryTheory.Mod D A) (d : ModDualityDatum A M M') : CategoryTheory.MonoidalCategoryStruct.tensorUnit D ⟶ A

The zigzag scalar of a duality datum: the copairing unit, braided across the module tensor product and consumed by the pairing.

Equations

• RS.zig A M M' d = CategoryTheory.CategoryStruct.comp (RS.copairUnit A M M' d) (CategoryTheory.CategoryStruct.comp (RS.modTensorSwap A M M') d.pair)

theorem RS.zig_eq_unit {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Limits.HasCoequalizers D] (A : D) [CategoryTheory.MonObj A] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Z)] [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) : zig A M M' d = CategoryTheory.MonObj.one

The retraction law: under the zigzag identity of the datum, the zigzag scalar is the unit of the base.