Twisting distributes over the biproduct of modules

Tensoring on the left by a fixed object distributes over the biproduct of two modules. At the level of carriers this is the standard distributivity of the tensor over a binary biproduct, assembled from biprod.lift and biprod.desc; the two round-trips use the totality relation of the biproduct together with the additivity of the left whiskering. The distributivity map intertwines the action through the right tensor factor with the componentwise action of the biproduct, because each biproduct projection is a module map and the twist of a module map is again a module map.

The carrier-level distributivity

noncomputable def RS.tensorLeftBiprodHom {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasBinaryBiproducts D] (V X Y : D) : CategoryTheory.MonoidalCategoryStruct.tensorObj V (X ⊞ Y) ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj V X ⊞ CategoryTheory.MonoidalCategoryStruct.tensorObj V Y

Distributivity of the tensor over a binary biproduct: the comparison map assembled from the two whiskered projections.

Equations

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

noncomputable def RS.tensorLeftBiprodInv {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasBinaryBiproducts D] (V X Y : D) : CategoryTheory.MonoidalCategoryStruct.tensorObj V X ⊞ CategoryTheory.MonoidalCategoryStruct.tensorObj V Y ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj V (X ⊞ Y)

The inverse comparison map, assembled from the two whiskered injections.

Equations

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

@[simp]

theorem RS.tensorLeftBiprodHom_fst {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasBinaryBiproducts D] (V X Y : D) : CategoryTheory.CategoryStruct.comp (tensorLeftBiprodHom V X Y) CategoryTheory.Limits.biprod.fst = CategoryTheory.MonoidalCategoryStruct.whiskerLeft V CategoryTheory.Limits.biprod.fst

@[simp]

theorem RS.tensorLeftBiprodHom_snd {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasBinaryBiproducts D] (V X Y : D) : CategoryTheory.CategoryStruct.comp (tensorLeftBiprodHom V X Y) CategoryTheory.Limits.biprod.snd = CategoryTheory.MonoidalCategoryStruct.whiskerLeft V CategoryTheory.Limits.biprod.snd

@[simp]

theorem RS.inl_tensorLeftBiprodInv {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasBinaryBiproducts D] (V X Y : D) : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inl (tensorLeftBiprodInv V X Y) = CategoryTheory.MonoidalCategoryStruct.whiskerLeft V CategoryTheory.Limits.biprod.inl

@[simp]

theorem RS.inr_tensorLeftBiprodInv {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasBinaryBiproducts D] (V X Y : D) : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inr (tensorLeftBiprodInv V X Y) = CategoryTheory.MonoidalCategoryStruct.whiskerLeft V CategoryTheory.Limits.biprod.inr

@[simp]

theorem RS.tensorLeftBiprodHom_inv {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasBinaryBiproducts D] (V X Y : D) : CategoryTheory.CategoryStruct.comp (tensorLeftBiprodHom V X Y) (tensorLeftBiprodInv V X Y) = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj V (X ⊞ Y))

The comparison map is split by its inverse: the totality relation of the biproduct, whiskered.

@[simp]

theorem RS.tensorLeftBiprodInv_hom {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasBinaryBiproducts D] (V X Y : D) : CategoryTheory.CategoryStruct.comp (tensorLeftBiprodInv V X Y) (tensorLeftBiprodHom V X Y) = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj V X ⊞ CategoryTheory.MonoidalCategoryStruct.tensorObj V Y)

The inverse comparison map is split by the comparison map.

The distributivity as a module isomorphism

theorem RS.actAcross_whiskerLeft_of {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] (A : D) [CategoryTheory.MonObj A] (V : D) {X Y : D} [CategoryTheory.ModObj A X] [CategoryTheory.ModObj A Y] (g : X ⟶ Y) (hg : CategoryTheory.CategoryStruct.comp (actLeft A X) g = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A g) (actLeft A Y)) : CategoryTheory.CategoryStruct.comp (actAcross A V X) (CategoryTheory.MonoidalCategoryStruct.whiskerLeft V g) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (CategoryTheory.MonoidalCategoryStruct.whiskerLeft V g)) (actAcross A V Y)

The twist of a module map is a module map: a map intertwining the actions still intertwines them after whiskering by a fixed object on the left.

noncomputable def RS.twistBiprodActL {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasBinaryBiproducts D] [CategoryTheory.SymmetricCategory D] (A : D) [CategoryTheory.MonObj A] (V : D) (P Q : CategoryTheory.Mod D A) : CategoryTheory.MonoidalCategoryStruct.tensorObj A (CategoryTheory.MonoidalCategoryStruct.tensorObj V (P.X ⊞ Q.X)) ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj V (P.X ⊞ Q.X)

The action on the twist of the module biproduct, retyped.

Equations

• RS.twistBiprodActL A V P Q = RS.actAcross A V (RS.modBiprod A P Q).X

noncomputable def RS.twistBiprodActR {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasBinaryBiproducts D] [CategoryTheory.SymmetricCategory D] (A : D) [CategoryTheory.MonObj A] (V : D) (P Q : CategoryTheory.Mod D A) : CategoryTheory.MonoidalCategoryStruct.tensorObj A (CategoryTheory.MonoidalCategoryStruct.tensorObj V P.X ⊞ CategoryTheory.MonoidalCategoryStruct.tensorObj V Q.X) ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj V P.X ⊞ CategoryTheory.MonoidalCategoryStruct.tensorObj V Q.X

The componentwise action on the biproduct of the twists, retyped.

Equations

• RS.twistBiprodActR A V P Q = RS.modBiprodAct A (RS.tensorLeftMod A V P) (RS.tensorLeftMod A V Q)

theorem RS.twistBiprodActL_fst {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasBinaryBiproducts D] [CategoryTheory.SymmetricCategory D] (A : D) [CategoryTheory.MonObj A] (V : D) (P Q : CategoryTheory.Mod D A) : CategoryTheory.CategoryStruct.comp (twistBiprodActL A V P Q) (CategoryTheory.MonoidalCategoryStruct.whiskerLeft V CategoryTheory.Limits.biprod.fst) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (CategoryTheory.MonoidalCategoryStruct.whiskerLeft V CategoryTheory.Limits.biprod.fst)) (actAcross A V P.X)

The twisted first projection intertwines the actions.

theorem RS.twistBiprodActL_snd {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasBinaryBiproducts D] [CategoryTheory.SymmetricCategory D] (A : D) [CategoryTheory.MonObj A] (V : D) (P Q : CategoryTheory.Mod D A) : CategoryTheory.CategoryStruct.comp (twistBiprodActL A V P Q) (CategoryTheory.MonoidalCategoryStruct.whiskerLeft V CategoryTheory.Limits.biprod.snd) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (CategoryTheory.MonoidalCategoryStruct.whiskerLeft V CategoryTheory.Limits.biprod.snd)) (actAcross A V Q.X)

The twisted second projection intertwines the actions.

theorem RS.twistBiprodActR_fst {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasBinaryBiproducts D] [CategoryTheory.SymmetricCategory D] (A : D) [CategoryTheory.MonObj A] (V : D) (P Q : CategoryTheory.Mod D A) : CategoryTheory.CategoryStruct.comp (twistBiprodActR A V P Q) CategoryTheory.Limits.biprod.fst = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A CategoryTheory.Limits.biprod.fst) (actAcross A V P.X)

The first component of the componentwise action.

theorem RS.twistBiprodActR_snd {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasBinaryBiproducts D] [CategoryTheory.SymmetricCategory D] (A : D) [CategoryTheory.MonObj A] (V : D) (P Q : CategoryTheory.Mod D A) : CategoryTheory.CategoryStruct.comp (twistBiprodActR A V P Q) CategoryTheory.Limits.biprod.snd = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A CategoryTheory.Limits.biprod.snd) (actAcross A V Q.X)

The second component of the componentwise action.

theorem RS.twistBiprodActL_hom {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasBinaryBiproducts D] [CategoryTheory.SymmetricCategory D] (A : D) [CategoryTheory.MonObj A] (V : D) (P Q : CategoryTheory.Mod D A) : CategoryTheory.CategoryStruct.comp (twistBiprodActL A V P Q) (tensorLeftBiprodHom V P.X Q.X) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (tensorLeftBiprodHom V P.X Q.X)) (twistBiprodActR A V P Q)

The distributivity map is linear: it intertwines the action through the right tensor factor with the componentwise action of the biproduct.

theorem RS.twistBiprodActR_inv {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasBinaryBiproducts D] [CategoryTheory.SymmetricCategory D] (A : D) [CategoryTheory.MonObj A] (V : D) (P Q : CategoryTheory.Mod D A) : CategoryTheory.CategoryStruct.comp (twistBiprodActR A V P Q) (tensorLeftBiprodInv V P.X Q.X) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (tensorLeftBiprodInv V P.X Q.X)) (twistBiprodActL A V P Q)

The inverse distributivity map is linear.

noncomputable def RS.tensorLeftBiprodModHom {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasBinaryBiproducts D] [CategoryTheory.SymmetricCategory D] (A : D) [CategoryTheory.MonObj A] (V : D) (P Q : CategoryTheory.Mod D A) : tensorLeftMod A V (modBiprod A P Q) ⟶ modBiprod A (tensorLeftMod A V P) (tensorLeftMod A V Q)

The distributivity map, as a module map.

Equations

• RS.tensorLeftBiprodModHom A V P Q = CategoryTheory.Mod.Hom.mk' (RS.tensorLeftBiprodHom V P.X Q.X) ⋯

noncomputable def RS.tensorLeftBiprodModInv {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasBinaryBiproducts D] [CategoryTheory.SymmetricCategory D] (A : D) [CategoryTheory.MonObj A] (V : D) (P Q : CategoryTheory.Mod D A) : modBiprod A (tensorLeftMod A V P) (tensorLeftMod A V Q) ⟶ tensorLeftMod A V (modBiprod A P Q)

The inverse distributivity map, as a module map.

Equations

• RS.tensorLeftBiprodModInv A V P Q = CategoryTheory.Mod.Hom.mk' (RS.tensorLeftBiprodInv V P.X Q.X) ⋯

@[simp]

theorem RS.tensorLeftBiprodModHom_hom {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasBinaryBiproducts D] [CategoryTheory.SymmetricCategory D] (A : D) [CategoryTheory.MonObj A] (V : D) (P Q : CategoryTheory.Mod D A) : (tensorLeftBiprodModHom A V P Q).hom = tensorLeftBiprodHom V P.X Q.X

@[simp]

theorem RS.tensorLeftBiprodModInv_hom {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasBinaryBiproducts D] [CategoryTheory.SymmetricCategory D] (A : D) [CategoryTheory.MonObj A] (V : D) (P Q : CategoryTheory.Mod D A) : (tensorLeftBiprodModInv A V P Q).hom = tensorLeftBiprodInv V P.X Q.X

noncomputable def RS.tensorLeftBiprodIso {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasBinaryBiproducts D] [CategoryTheory.SymmetricCategory D] (A : D) [CategoryTheory.MonObj A] (V : D) (P Q : CategoryTheory.Mod D A) : tensorLeftMod A V (modBiprod A P Q) ≅ modBiprod A (tensorLeftMod A V P) (tensorLeftMod A V Q)

Twisting distributes over the biproduct of modules: the twist of a biproduct of modules is the biproduct of the twists.

Equations

• RS.tensorLeftBiprodIso A V P Q = { hom := RS.tensorLeftBiprodModHom A V P Q, inv := RS.tensorLeftBiprodModInv A V P Q, hom_inv_id := ⋯, inv_hom_id := ⋯ }