The tensor product of duality data

Deligne's 1.15 tensor part: dual pairs tensor. The pairing of the tensor datum crosses the middle factors through the descended interchange and pairs coordinatewise into the regular module; the copairing unfolds the unit and inserts both copairings. The descended interchange exists because the interchange is linear in both factors.

noncomputable def RS.interchangeDesc {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] (X₁ X₂ Y₁ Y₂ : CategoryTheory.Mod D A) : modTensor A (modTensorMod A X₁ X₂) (modTensorMod A Y₁ Y₂) ⟶ modTensor A (modTensorMod A X₁ Y₁) (modTensorMod A X₂ Y₂)

The descended interchange: the interchange of module tensor products descends to the relative tensor of the bundles, because it is linear in both factors.

Equations

• RS.interchangeDesc A X₁ X₂ Y₁ Y₂ = RS.modTensorDesc A (RS.modTensorMod A X₁ X₂) (RS.modTensorMod A Y₁ Y₂) (RS.interchange A X₁ X₂ Y₁ Y₂) ⋯

@[simp]

theorem RS.modTensorπ_interchangeDesc {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] (X₁ X₂ Y₁ Y₂ : CategoryTheory.Mod D A) : CategoryTheory.CategoryStruct.comp (modTensorπ A (modTensorMod A X₁ X₂) (modTensorMod A Y₁ Y₂)) (interchangeDesc A X₁ X₂ Y₁ Y₂) = interchange A X₁ X₂ Y₁ Y₂

Defining equation of the descended interchange.

@[simp]

theorem RS.modTensorπ_interchangeDesc_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] (X₁ X₂ Y₁ Y₂ : CategoryTheory.Mod D A) {Z : D} (h : modTensor A (modTensorMod A X₁ Y₁) (modTensorMod A X₂ Y₂) ⟶ Z) : CategoryTheory.CategoryStruct.comp (modTensorπ A (modTensorMod A X₁ X₂) (modTensorMod A Y₁ Y₂)) (CategoryTheory.CategoryStruct.comp (interchangeDesc A X₁ X₂ Y₁ Y₂) h) = CategoryTheory.CategoryStruct.comp (interchange A X₁ X₂ Y₁ Y₂) h

Defining equation of the descended interchange.

theorem RS.interchangeDesc_act {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] (X₁ X₂ Y₁ Y₂ : CategoryTheory.Mod D A) : CategoryTheory.CategoryStruct.comp (modTensorAct A (modTensorMod A X₁ X₂) (modTensorMod A Y₁ Y₂)) (interchangeDesc A X₁ X₂ Y₁ Y₂) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (interchangeDesc A X₁ X₂ Y₁ Y₂)) (modTensorAct A (modTensorMod A X₁ Y₁) (modTensorMod A X₂ Y₂))

The descended interchange intertwines the actions.

theorem RS.interchangeDesc_act_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] (X₁ X₂ Y₁ Y₂ : CategoryTheory.Mod D A) {Z : D} (h : modTensor A (modTensorMod A X₁ Y₁) (modTensorMod A X₂ Y₂) ⟶ Z) : CategoryTheory.CategoryStruct.comp (modTensorAct A (modTensorMod A X₁ X₂) (modTensorMod A Y₁ Y₂)) (CategoryTheory.CategoryStruct.comp (interchangeDesc A X₁ X₂ Y₁ Y₂) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (interchangeDesc A X₁ X₂ Y₁ Y₂)) (CategoryTheory.CategoryStruct.comp (modTensorAct A (modTensorMod A X₁ Y₁) (modTensorMod A X₂ Y₂)) h)

The descended interchange intertwines the actions.

noncomputable def RS.regPairFold {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Limits.HasCoequalizers D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.IsCommMonObj A] : modTensor A (regularMod A) (regularMod A) ⟶ A

The fold of the doubled regular module onto the base.

Equations

• RS.regPairFold A = (RS.modTensorUnitLeft A (RS.regularMod A)).hom

noncomputable def RS.tensorPair {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₂ N₁' N₂' : CategoryTheory.Mod D A} (d₁ : ModDualityDatum A N₁ N₁') (d₂ : ModDualityDatum A N₂ N₂') : modTensor A (modTensorMod A N₁' N₂') (modTensorMod A N₁ N₂) ⟶ A

The tensor pairing: cross through the descended interchange, pair coordinatewise, and fold.

Equations

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

noncomputable def RS.regPairUnfold {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Limits.HasCoequalizers D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.IsCommMonObj A] : A ⟶ modTensor A (regularMod A) (regularMod A)

The unfolding of the base into the doubled regular module.

Equations

• RS.regPairUnfold A = (RS.modTensorUnitLeft A (RS.regularMod A)).inv

noncomputable def RS.tensorCopair {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₂ N₁' N₂' : CategoryTheory.Mod D A} (d₁ : ModDualityDatum A N₁ N₁') (d₂ : ModDualityDatum A N₂ N₂') : A ⟶ modTensor A (modTensorMod A N₁ N₂) (modTensorMod A N₁' N₂')

The tensor copairing: unfold the unit, insert both copairings, and regroup through the descended interchange.

Equations

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

theorem RS.regPairUnfold_act {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.CategoryStruct.comp CategoryTheory.MonObj.mul (regPairUnfold A) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (regPairUnfold A)) (modTensorAct A (regularMod A) (regularMod A))

The inverse of the doubled-unit fold intertwines the multiplication and the action.

theorem RS.tensorPair_linear {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₂ N₁' N₂' : CategoryTheory.Mod D A} (d₁ : ModDualityDatum A N₁ N₁') (d₂ : ModDualityDatum A N₂ N₂') : CategoryTheory.CategoryStruct.comp (modTensorAct A (modTensorMod A N₁' N₂') (modTensorMod A N₁ N₂)) (tensorPair A d₁ d₂) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (tensorPair A d₁ d₂)) CategoryTheory.MonObj.mul

The tensor pairing is linear.

theorem RS.tensorCopair_linear {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₂ N₁' N₂' : CategoryTheory.Mod D A} (d₁ : ModDualityDatum A N₁ N₁') (d₂ : ModDualityDatum A N₂ N₂') : CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.mul (tensorCopair A d₁ d₂) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (tensorCopair A d₁ d₂)) (modTensorAct A (modTensorMod A N₁ N₂) (modTensorMod A N₁' N₂'))

The tensor copairing is linear.

noncomputable def RS.tensorDatum {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₂ N₁' N₂' : CategoryTheory.Mod D A} (d₁ : ModDualityDatum A N₁ N₁') (d₂ : ModDualityDatum A N₂ N₂') : ModDualityDatum A (modTensorMod A N₁ N₂) (modTensorMod A N₁' N₂')

The tensor product of duality data (Deligne 1.15, tensor part): dual pairs tensor, with the crossed coordinatewise pairing and copairing.

Equations

• RS.tensorDatum A d₁ d₂ = { pair := RS.tensorPair A d₁ d₂, copair := RS.tensorCopair A d₁ d₂, pair_linear := ⋯, copair_linear := ⋯ }