Documentation

LeanPool.RegtsSevenster.RS.Classical.Deligne.PairMul

The interchange of module tensor products #

The pair-multiplication device of the Key Lemma's chain algebra: over a symmetric base, the tensor product of two module tensor products interchanges into the module tensor product of the crossed pairs. The chain transitions and the stage products of the splitting algebra factor through it.

source
def RS.rawInterchange {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] (A : D) [CategoryTheory.MonObj A] (N₁ N₂ P₁ P₂ : CategoryTheory.Mod D A) :
CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj N₁.X N₂.X) (CategoryTheory.MonoidalCategoryStruct.tensorObj P₁.X P₂.X) ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj N₁.X P₁.X) (CategoryTheory.MonoidalCategoryStruct.tensorObj N₂.X P₂.X)

The raw interchange: cross the middle factors.

Equations
Instances For
    source
    noncomputable def RS.rawInterchangeπ {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] (N₁ N₂ P₁ P₂ : CategoryTheory.Mod D A) :
    CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj N₁.X N₂.X) (CategoryTheory.MonoidalCategoryStruct.tensorObj P₁.X P₂.X) ⟶ modTensor A (modTensorMod A N₁ P₁) (modTensorMod A N₂ P₂)

    The raw interchange followed by the projections.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      noncomputable def RS.midArrange {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] (A : D) [CategoryTheory.MonObj A] (N₁ N₂ P₁ P₂ : CategoryTheory.Mod D A) :
      CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj N₁.X A) N₂.X) (CategoryTheory.MonoidalCategoryStruct.tensorObj P₁.X P₂.X) ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj N₁.X P₁.X) A) (CategoryTheory.MonoidalCategoryStruct.tensorObj N₂.X P₂.X)

      The scalar-carrying rearrangement: the interchange at the scalar-extended first block, the scalar crossing to the block boundary.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        theorem RS.interchange_legM {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] (N₁ N₂ P₁ P₂ : CategoryTheory.Mod D A) :
        CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (modTensorLegM A N₁ N₂) (CategoryTheory.MonoidalCategoryStruct.tensorObj P₁.X P₂.X)) (rawInterchangeπ A N₁ N₂ P₁ P₂) = CategoryTheory.CategoryStruct.comp (midArrange A N₁ N₂ P₁ P₂) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.MonoidalCategoryStruct.whiskerRight (modTensorπ A N₁ P₁) A) (modTensorπ A N₂ P₂)) (CategoryTheory.CategoryStruct.comp (modTensorLegM A (modTensorMod A N₁ P₁) (modTensorMod A N₂ P₂)) (modTensorπ A (modTensorMod A N₁ P₁) (modTensorMod A N₂ P₂))))

        The left slide of the first factors becomes the outer left slide of the target.

        source
        theorem RS.interchange_legN {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] (N₁ N₂ P₁ P₂ : CategoryTheory.Mod D A) :
        CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (modTensorLegN A N₁ N₂) (CategoryTheory.MonoidalCategoryStruct.tensorObj P₁.X P₂.X)) (rawInterchangeπ A N₁ N₂ P₁ P₂) = CategoryTheory.CategoryStruct.comp (midArrange A N₁ N₂ P₁ P₂) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.MonoidalCategoryStruct.whiskerRight (modTensorπ A N₁ P₁) A) (modTensorπ A N₂ P₂)) (CategoryTheory.CategoryStruct.comp (modTensorLegN A (modTensorMod A N₁ P₁) (modTensorMod A N₂ P₂)) (modTensorπ A (modTensorMod A N₁ P₁) (modTensorMod A N₂ P₂))))

        The right slide of the second factors becomes the outer right slide of the target.

        source
        noncomputable def RS.midArrangeP {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] (A : D) [CategoryTheory.MonObj A] (N₁ N₂ P₁ P₂ : CategoryTheory.Mod D A) :
        CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj N₁.X N₂.X) (CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj P₁.X A) P₂.X) ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj N₁.X P₁.X) A) (CategoryTheory.MonoidalCategoryStruct.tensorObj N₂.X P₂.X)

        The scalar-carrying rearrangement from the second block: the interchange at the scalar-extended second block, the scalar reassociating to the block boundary.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          theorem RS.interchange_legMP {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] (N₁ N₂ P₁ P₂ : CategoryTheory.Mod D A) :
          CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (CategoryTheory.MonoidalCategoryStruct.tensorObj N₁.X N₂.X) (modTensorLegM A P₁ P₂)) (rawInterchangeπ A N₁ N₂ P₁ P₂) = CategoryTheory.CategoryStruct.comp (midArrangeP A N₁ N₂ P₁ P₂) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.MonoidalCategoryStruct.whiskerRight (modTensorπ A N₁ P₁) A) (modTensorπ A N₂ P₂)) (CategoryTheory.CategoryStruct.comp (modTensorLegM A (modTensorMod A N₁ P₁) (modTensorMod A N₂ P₂)) (modTensorπ A (modTensorMod A N₁ P₁) (modTensorMod A N₂ P₂))))

          The second-block left slide becomes the outer left slide of the target.

          source
          theorem RS.interchange_legNP {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] (N₁ N₂ P₁ P₂ : CategoryTheory.Mod D A) :
          CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (CategoryTheory.MonoidalCategoryStruct.tensorObj N₁.X N₂.X) (modTensorLegN A P₁ P₂)) (rawInterchangeπ A N₁ N₂ P₁ P₂) = CategoryTheory.CategoryStruct.comp (midArrangeP A N₁ N₂ P₁ P₂) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.MonoidalCategoryStruct.whiskerRight (modTensorπ A N₁ P₁) A) (modTensorπ A N₂ P₂)) (CategoryTheory.CategoryStruct.comp (modTensorLegN A (modTensorMod A N₁ P₁) (modTensorMod A N₂ P₂)) (modTensorπ A (modTensorMod A N₁ P₁) (modTensorMod A N₂ P₂))))

          The second-block right slide becomes the outer right slide of the target.

          source
          theorem RS.rawInterchangeπ_condN {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] (N₁ N₂ P₁ P₂ : CategoryTheory.Mod D A) :
          CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (modTensorLegM A N₁ N₂) (CategoryTheory.MonoidalCategoryStruct.tensorObj P₁.X P₂.X)) (rawInterchangeπ A N₁ N₂ P₁ P₂) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (modTensorLegN A N₁ N₂) (CategoryTheory.MonoidalCategoryStruct.tensorObj P₁.X P₂.X)) (rawInterchangeπ A N₁ N₂ P₁ P₂)

          The two first-block legs agree after the raw interchange projection.

          source
          theorem RS.rawInterchangeπ_condP {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] (N₁ N₂ P₁ P₂ : CategoryTheory.Mod D A) :
          CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (CategoryTheory.MonoidalCategoryStruct.tensorObj N₁.X N₂.X) (modTensorLegM A P₁ P₂)) (rawInterchangeπ A N₁ N₂ P₁ P₂) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (CategoryTheory.MonoidalCategoryStruct.tensorObj N₁.X N₂.X) (modTensorLegN A P₁ P₂)) (rawInterchangeπ A N₁ N₂ P₁ P₂)

          The two second-block legs agree after the raw interchange projection.

          source
          noncomputable def RS.interchangeStage1 {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) :
          CategoryTheory.MonoidalCategoryStruct.tensorObj (modTensor A N₁ N₂) (CategoryTheory.MonoidalCategoryStruct.tensorObj P₁.X P₂.X) ⟶ modTensor A (modTensorMod A N₁ P₁) (modTensorMod A N₂ P₂)

          First-stage descent of the interchange, through the coequalizer of the first block.

          Equations
          Instances For
            source
            theorem RS.whiskerRight_π_interchangeStage1 {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) :
            CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (modTensorπ A N₁ N₂) (CategoryTheory.MonoidalCategoryStruct.tensorObj P₁.X P₂.X)) (interchangeStage1 A N₁ N₂ P₁ P₂) = rawInterchangeπ A N₁ N₂ P₁ P₂

            Defining equation of the first-stage descent.

            source
            theorem RS.whiskerRight_π_interchangeStage1_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) {Z : D} (h : modTensor A (modTensorMod A N₁ P₁) (modTensorMod A N₂ P₂) ⟶ Z) :
            CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (modTensorπ A N₁ N₂) (CategoryTheory.MonoidalCategoryStruct.tensorObj P₁.X P₂.X)) (CategoryTheory.CategoryStruct.comp (interchangeStage1 A N₁ N₂ P₁ P₂) h) = CategoryTheory.CategoryStruct.comp (rawInterchangeπ A N₁ N₂ P₁ P₂) h

            Defining equation of the first-stage descent.

            source
            theorem RS.interchangeStage1_condP {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) :
            CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (modTensor A N₁ N₂) (modTensorLegM A P₁ P₂)) (interchangeStage1 A N₁ N₂ P₁ P₂) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (modTensor A N₁ N₂) (modTensorLegN A P₁ P₂)) (interchangeStage1 A N₁ N₂ P₁ P₂)

            The second-block legs agree after the first-stage descent.

            source
            noncomputable def RS.interchange {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) :
            CategoryTheory.MonoidalCategoryStruct.tensorObj (modTensor A N₁ N₂) (modTensor A P₁ P₂) ⟶ modTensor A (modTensorMod A N₁ P₁) (modTensorMod A N₂ P₂)

            The interchange of module tensor products: the tensor product of two module tensor products maps to the module tensor product of the crossed pairs.

            Equations
            Instances For
              source
              @[simp]
              theorem RS.tensorHom_π_interchange {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) :
              CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (modTensorπ A N₁ N₂) (modTensorπ A P₁ P₂)) (interchange A N₁ N₂ P₁ P₂) = rawInterchangeπ A N₁ N₂ P₁ P₂

              Defining equation of the interchange.

              source
              @[simp]
              theorem RS.tensorHom_π_interchange_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) {Z : D} (h : modTensor A (modTensorMod A N₁ P₁) (modTensorMod A N₂ P₂) ⟶ Z) :
              CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (modTensorπ A N₁ N₂) (modTensorπ A P₁ P₂)) (CategoryTheory.CategoryStruct.comp (interchange A N₁ N₂ P₁ P₂) h) = CategoryTheory.CategoryStruct.comp (rawInterchangeπ A N₁ N₂ P₁ P₂) h

              Defining equation of the interchange.