Linearity of the base-changed pairing and copairing

The base-changed pairing and copairing of a duality datum are linear over the new base: each factor of the defining composites intertwines the descended actions, and the two linearity laws follow by chaining the factors.

noncomputable def RS.modTensorWhiskerLRIsColimit {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] (M N : CategoryTheory.Mod D A) (P W : D) : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.Cofork.ofπ (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.whiskerLeft P (modTensorπ A M N)) W) ⋯)

Whiskering the module-tensor coequalizer by tensorLeft P and then by tensorRight W yields a colimit cofork.

Equations

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

theorem RS.modTensor_whiskerLR_hom_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] (M N : CategoryTheory.Mod D A) (P W : D) {Z : D} {k l : CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj P (modTensor A M N)) W ⟶ Z} (h : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.whiskerLeft P (modTensorπ A M N)) W) k = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.whiskerLeft P (modTensorπ A M N)) W) l) : k = l

Morphisms out of a left-then-right whiskered tensor product of modules are determined by the doubly whiskered projection.

theorem RS.restrictAct_compat {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] (A B : D) [CategoryTheory.MonObj B] [CategoryTheory.IsCommMonObj B] (φ : A ⟶ B) (P : CategoryTheory.Mod D B) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft B (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft P.X φ) (actRight B P.X))) (actLeft B P.X) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator B P.X A).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (actLeft B P.X) A) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft P.X φ) (actRight B P.X)))

The B-action on a B-module commutes with the braided right action through the base morphism.

noncomputable def RS.collapseAct {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] (B : D) [CategoryTheory.MonObj B] [CategoryTheory.IsCommMonObj B] (φ : A ⟶ B) [CategoryTheory.IsMonHom φ] (P : CategoryTheory.Mod D B) (N : CategoryTheory.Mod D A) : CategoryTheory.MonoidalCategoryStruct.tensorObj B (modTensor A (restrictMod A B φ P) N) ⟶ modTensor A (restrictMod A B φ P) N

The descended B-action on the collapsed tensor: the B-action of the module descends through the coequalizer of the restricted-module tensor.

Equations

• RS.collapseAct A B φ P N = RS.modTensorDescAct A (RS.restrictMod A B φ P) N B (RS.actLeft B P.X) ⋯

theorem RS.whiskerLeft_restrictπ_collapseAct {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] (B : D) [CategoryTheory.MonObj B] [CategoryTheory.IsCommMonObj B] (φ : A ⟶ B) [CategoryTheory.IsMonHom φ] (P : CategoryTheory.Mod D B) (N : CategoryTheory.Mod D A) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft B (restrictπ A B φ P N)) (collapseAct A B φ P N) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator B P.X N.X).inv (CategoryTheory.MonoidalCategoryStruct.whiskerRight (actLeft B P.X) N.X)) (restrictπ A B φ P N)

Defining equation of the descended B-action, in the retyped spelling.

theorem RS.collapseMid_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)] (A : D) [CategoryTheory.MonObj A] (B : D) [CategoryTheory.MonObj B] [CategoryTheory.IsCommMonObj B] (φ : A ⟶ B) [CategoryTheory.IsMonHom φ] (P : CategoryTheory.Mod D B) (N : CategoryTheory.Mod D A) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (actLeft B P.X) (baseChange φ N)) (collapseMid A B φ P N) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator B P.X (baseChange φ N)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft B (collapseMid A B φ P N)) (collapseAct A B φ P N))

The half-descended collapse intertwines the module action with the descended action.

theorem RS.collapseHom_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)] (A : D) [CategoryTheory.MonObj A] (B : D) [CategoryTheory.MonObj B] [CategoryTheory.IsCommMonObj B] (φ : A ⟶ B) [CategoryTheory.IsMonHom φ] (P : CategoryTheory.Mod D B) (N : CategoryTheory.Mod D A) : CategoryTheory.CategoryStruct.comp (modTensorAct B P (baseChangeMod φ N)) (collapseHom A B φ P N) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft B (collapseHom A B φ P N)) (collapseAct A B φ P N)

The collapse is linear over the new base: it intertwines the module action with the descended action.

theorem RS.baseChangeAct_unitRight {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] (B : D) [CategoryTheory.MonObj B] [CategoryTheory.IsCommMonObj B] (φ : A ⟶ B) [CategoryTheory.IsMonHom φ] : CategoryTheory.CategoryStruct.comp (baseChangeAct φ (regularMod A)) (modTensorUnitRight A (restrictRegular φ)).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft B (modTensorUnitRight A (restrictRegular φ)).hom) CategoryTheory.MonObj.mul

The right unit collapse of the induced regular module is linear over the new base.

theorem RS.modTensorDescAct_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] (B : D) {P Q : CategoryTheory.Mod D A} (h : P = Q) (N : CategoryTheory.Mod D A) (actP : CategoryTheory.MonoidalCategoryStruct.tensorObj B P.X ⟶ P.X) (actQ : CategoryTheory.MonoidalCategoryStruct.tensorObj B Q.X ⟶ Q.X) (hcP : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft B (actRight A P.X)) actP = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator B P.X A).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight actP A) (actRight A P.X))) (hcQ : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft B (actRight A Q.X)) actQ = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator B Q.X A).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight actQ A) (actRight A Q.X))) (hact : CategoryTheory.CategoryStruct.comp actP (CategoryTheory.eqToHom ⋯) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft B (CategoryTheory.eqToHom ⋯)) actQ) : CategoryTheory.CategoryStruct.comp (modTensorDescAct A P N B actP hcP) (CategoryTheory.eqToHom ⋯) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft B (CategoryTheory.eqToHom ⋯)) (modTensorDescAct A Q N B actQ hcQ)

Transport of a descended action along an equality of modules: the descended actions of equal modules agree through the induced transport.

noncomputable def RS.bcActR {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] (B : D) [CategoryTheory.MonObj B] [CategoryTheory.IsCommMonObj B] (φ : A ⟶ B) [CategoryTheory.IsMonHom φ] (M : CategoryTheory.Mod D A) : CategoryTheory.MonoidalCategoryStruct.tensorObj B (modTensor A (restrictRegular φ) M) ⟶ modTensor A (restrictRegular φ) M

The base-change action, retyped at the relative-tensor spelling so that goals stay type-correct.

Equations

• RS.bcActR A B φ M = RS.baseChangeAct φ M

theorem RS.whiskerLeft_π_bcActR {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] (B : D) [CategoryTheory.MonObj B] [CategoryTheory.IsCommMonObj B] (φ : A ⟶ B) [CategoryTheory.IsMonHom φ] (M : CategoryTheory.Mod D A) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft B (modTensorπ A (restrictRegular φ) M)) (bcActR A B φ M) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator B B M.X).inv (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.mul M.X)) (modTensorπ A (restrictRegular φ) M)

Defining equation of the retyped base-change action.

theorem RS.bcActR_compat {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] (B : D) [CategoryTheory.MonObj B] [CategoryTheory.IsCommMonObj B] (φ : A ⟶ B) [CategoryTheory.IsMonHom φ] (M : CategoryTheory.Mod D A) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft B (actRight A (modTensorMod A (restrictRegular φ) M).X)) (bcActR A B φ M) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator B (modTensorMod A (restrictRegular φ) M).X A).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (bcActR A B φ M) A) (actRight A (modTensorMod A (restrictRegular φ) M).X))

The retyped base-change action commutes with the braided right action.

theorem RS.assocHom_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] (B : D) [CategoryTheory.MonObj B] [CategoryTheory.IsCommMonObj B] (φ : A ⟶ B) [CategoryTheory.IsMonHom φ] (M N : CategoryTheory.Mod D A) (hc : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft B (actRight A (modTensorMod A (restrictRegular φ) M).X)) (bcActR A B φ M) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator B (modTensorMod A (restrictRegular φ) M).X A).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (bcActR A B φ M) A) (actRight A (modTensorMod A (restrictRegular φ) M).X))) : CategoryTheory.CategoryStruct.comp (modTensorDescAct A (modTensorMod A (restrictRegular φ) M) N B (bcActR A B φ M) hc) (modTensorAssocHom A (restrictRegular φ) M N) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft B (modTensorAssocHom A (restrictRegular φ) M N)) (bcActR A B φ (modTensorMod A M N))

The associator is linear over the new base: it intertwines the action descended on the nested first slot with the action of the base change.

theorem RS.projFormula_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] (B : D) [CategoryTheory.MonObj B] [CategoryTheory.IsCommMonObj B] (φ : A ⟶ B) [CategoryTheory.IsMonHom φ] (M N : CategoryTheory.Mod D A) : CategoryTheory.CategoryStruct.comp (modTensorAct B (baseChangeMod φ M) (baseChangeMod φ N)) (projFormula A B φ M N).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft B (projFormula A B φ M N).hom) (baseChangeAct φ (modTensorMod A M N))

The projection formula is linear over the new base.