Coherence of the base-change structure map #

The projection formula is compatible with the right unit collapse: contracting the regular factor before or after the base change gives the same map.

source

theorem RS.restrictπ_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] (B : D) [CategoryTheory.MonObj B] [CategoryTheory.IsCommMonObj B] (φ : A ⟶ B) [CategoryTheory.IsMonHom φ] (M N : CategoryTheory.Mod D A) :

CategoryTheory.CategoryStruct.comp (restrictπ A B φ (baseChangeMod φ M) N) (CategoryTheory.eqToHom ⋯) = modTensorπ A (modTensorMod A (restrictRegular φ) M) N

The cast leg is invisible on projections: the restricted projection, transported along the identification of the restricted base change, is the projection of the relative tensor.

source

theorem RS.projFormula_cover {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 (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (baseChangeMod φ M).X (modTensorπ A (restrictRegular φ) N)) (CategoryTheory.CategoryStruct.comp (modTensorπ B (baseChangeMod φ M) (baseChangeMod φ N)) (projFormula A B φ M N).hom) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator (baseChangeMod φ M).X B N.X).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (actRight B (baseChangeMod φ M).X) N.X) (modTensorAssocMid A (restrictRegular φ) M N))

The projection formula on the cover: composing the structure map with the inner projection unwinds to the right action of the new base followed by the half-descended module associator, with no transport left in the way.

source

theorem RS.modTensorAssocMid_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)] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorRight Z)] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.IsCommMonObj A] (P N : CategoryTheory.Mod D A) :

CategoryTheory.CategoryStruct.comp (modTensorAssocMid A P N (regularMod A)) (modTensorMap A (CategoryTheory.CategoryStruct.id P) (modTensorUnitRightMod A N).hom) = actRight A (modTensorMod A P N).X

The module triangle: reassociating and collapsing the regular factor on the right is the braided right action on the relative tensor.

source

theorem RS.actRight_modTensor_restrictRegular {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 φ] (M : CategoryTheory.Mod D A) :

actRight A (modTensorMod A (restrictRegular φ) M).X = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (baseChangeMod φ M).X φ) (actRight B (baseChangeMod φ M).X)

The restricted action on a base change: the A-action on the relative tensor is the B-action taken through the base morphism.

source

theorem RS.projFormula_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)] [∀ (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 (projFormula A B φ M (regularMod A)).hom (modTensorMap A (CategoryTheory.CategoryStruct.id (restrictRegular φ)) (modTensorUnitRightMod A M).hom) = CategoryTheory.CategoryStruct.comp (modTensorMap B (CategoryTheory.CategoryStruct.id (baseChangeMod φ M)) (baseChangeUnitIso A B φ).hom) (modTensorUnitRight B (baseChangeMod φ M)).hom

The unit coherence of the projection formula: collapsing the regular factor after the base change agrees with collapsing the base-changed regular module over the new base.

source

theorem RS.actRight_toRegular {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.IsCommMonObj A] (Q : CategoryTheory.Mod D A) (g : Q ⟶ regularMod A) :

CategoryTheory.CategoryStruct.comp (actRight A Q.X) g.hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight g.hom A) CategoryTheory.MonObj.mul

A module map into the regular module intertwines the braided right action with multiplication.

source

theorem RS.modTensorAssocMid_unitLeft {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] (P N : CategoryTheory.Mod D A) :

CategoryTheory.CategoryStruct.comp (modTensorAssocMid A P (regularMod A) N) (modTensorMap A (CategoryTheory.CategoryStruct.id P) (modTensorUnitLeftMod A N).hom) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (modTensorUnitRight A P).hom N.X) (modTensorπ A P N)

The module triangle on the left: reassociating and collapsing the regular factor in the middle is the collapse of the leading factor against the balance.

source

theorem RS.projFormula_unitLeft {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 φ] (N : CategoryTheory.Mod D A) :

CategoryTheory.CategoryStruct.comp (projFormula A B φ (regularMod A) N).hom (modTensorMap A (CategoryTheory.CategoryStruct.id (restrictRegular φ)) (modTensorUnitLeftMod A N).hom) = CategoryTheory.CategoryStruct.comp (modTensorMap B (baseChangeUnitIso A B φ).hom (CategoryTheory.CategoryStruct.id (baseChangeMod φ N))) (modTensorUnitLeft B (baseChangeMod φ N)).hom

The left unit coherence of the projection formula: collapsing the regular factor on the left commutes with the base change.

source

theorem RS.whiskerRight_modTensorπ_actRight_baseChange {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) :

The projection into a base change, whiskered against the new base, multiplies the two base factors after braiding the trailing one past the module.

source

theorem RS.projFormula_full_cover {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) :

The projection formula on the full cover: on the two covering projections the structure map multiplies the two base factors and projects — an explicit formula with no descent left in it.

source

theorem RS.baseShuffle {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] (B : D) [CategoryTheory.MonObj B] [CategoryTheory.IsCommMonObj B] (Q W : D) :

The base shuffle: bringing the second copy of the base to the front and multiplying is the middle-four interchange followed by the multiplication. Commutativity of the base is what makes the two orders agree.

source

theorem RS.baseAssoc {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] (B : D) [CategoryTheory.MonObj B] (Q₁ Q₂ Q₃ : D) :

The base multiplication is associative on covers: interchange-and-multiply is the structure map of a lax monoidal functor, so it satisfies the associativity square.

source

theorem RS.baseMul_natural_left {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] (B : D) [CategoryTheory.MonObj B] {Q Q' : D} (f : Q ⟶ Q') (W : D) :

Interchange-and-multiply is natural in the first module slot.

source

theorem RS.baseMul_natural_right {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] (B : D) [CategoryTheory.MonObj B] (Q : D) {W W' : D} (g : W ⟶ W') :

Interchange-and-multiply is natural in the second module slot.

source

theorem RS.projFormula_tensorμ_cover {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 (CategoryTheory.MonoidalCategoryStruct.whiskerRight (modTensorπ A (restrictRegular φ) M) (CategoryTheory.MonoidalCategoryStruct.tensorObj B N.X)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (baseChangeMod φ M).X (modTensorπ A (restrictRegular φ) N)) (CategoryTheory.CategoryStruct.comp (modTensorπ B (baseChangeMod φ M) (baseChangeMod φ N)) (projFormula A B φ M N).hom)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorμ B M.X B N.X) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.mul (CategoryTheory.MonoidalCategoryStruct.tensorObj M.X N.X)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft B (modTensorπ A M N)) (modTensorπ A (restrictRegular φ) (modTensorMod A M N))))

The projection formula on the full cover, in interchange form: the structure map multiplies the two base factors through the middle-four interchange and projects.

source

theorem RS.projFormula_assoc_core {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] (M N P : CategoryTheory.Mod D A) :

The core of the associator coherence: on the triple cover the two ways of multiplying three base factors and projecting agree. Naturality of interchange-and-multiply moves the two projections to the right, the defining equation of the half-descended associator merges them, and what is left is the associativity of interchange-and-multiply.

source