Biproducts of internal modules

The biproduct of two modules over a monoid object carries the componentwise action: the tensor distributes over the biproduct in a monoidally preadditive category, and the two actions act in each summand. The injections and projections are module maps, and morphisms out of the biproduct module are determined by the two components.

noncomputable def RS.modBiprodAct {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasBinaryBiproducts D] (A : D) [CategoryTheory.MonObj A] (M N : CategoryTheory.Mod D A) : CategoryTheory.MonoidalCategoryStruct.tensorObj A (M.X ⊞ N.X) ⟶ M.X ⊞ N.X

The componentwise action on the biproduct of the carriers.

Equations

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

theorem RS.modBiprodAct_one {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasBinaryBiproducts D] (A : D) [CategoryTheory.MonObj A] (M N : CategoryTheory.Mod D A) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.one (M.X ⊞ N.X)) (modBiprodAct A M N) = (CategoryTheory.MonoidalCategoryStruct.leftUnitor (M.X ⊞ N.X)).hom

The unit law of the componentwise action.

theorem RS.modBiprodAct_mul {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasBinaryBiproducts D] (A : D) [CategoryTheory.MonObj A] (M N : CategoryTheory.Mod D A) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.mul (M.X ⊞ N.X)) (modBiprodAct A M N) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator A A (M.X ⊞ N.X)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (modBiprodAct A M N)) (modBiprodAct A M N))

The multiplication law of the componentwise action.

@[implicit_reducible]

noncomputable def RS.modBiprodModObj {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasBinaryBiproducts D] (A : D) [CategoryTheory.MonObj A] (M N : CategoryTheory.Mod D A) : CategoryTheory.ModObj A (M.X ⊞ N.X)

The module structure on the biproduct of the carriers.

Equations

• RS.modBiprodModObj A M N = { smul := RS.modBiprodAct A M N, one_smul := ⋯, mul_smul := ⋯ }

noncomputable def RS.modBiprod {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasBinaryBiproducts D] (A : D) [CategoryTheory.MonObj A] (M N : CategoryTheory.Mod D A) : CategoryTheory.Mod D A

The biproduct of modules, bundled.

Equations

• RS.modBiprod A M N = { X := M.X ⊞ N.X, mod := RS.modBiprodModObj A M N }

@[simp]

theorem RS.modBiprod_X {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasBinaryBiproducts D] (A : D) [CategoryTheory.MonObj A] (M N : CategoryTheory.Mod D A) : (modBiprod A M N).X = (M.X ⊞ N.X)

theorem RS.actLeft_modBiprodInl {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasBinaryBiproducts D] (A : D) [CategoryTheory.MonObj A] (M N : CategoryTheory.Mod D A) : CategoryTheory.CategoryStruct.comp (actLeft A M.X) CategoryTheory.Limits.biprod.inl = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A CategoryTheory.Limits.biprod.inl) (modBiprodAct A M N)

The first injection intertwines the actions.

theorem RS.actLeft_modBiprodInr {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasBinaryBiproducts D] (A : D) [CategoryTheory.MonObj A] (M N : CategoryTheory.Mod D A) : CategoryTheory.CategoryStruct.comp (actLeft A N.X) CategoryTheory.Limits.biprod.inr = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A CategoryTheory.Limits.biprod.inr) (modBiprodAct A M N)

The second injection intertwines the actions.

theorem RS.modBiprodAct_fst {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasBinaryBiproducts D] (A : D) [CategoryTheory.MonObj A] (M N : CategoryTheory.Mod D A) : CategoryTheory.CategoryStruct.comp (modBiprodAct A M N) CategoryTheory.Limits.biprod.fst = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A CategoryTheory.Limits.biprod.fst) (actLeft A M.X)

The first projection intertwines the actions.

theorem RS.modBiprodAct_snd {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasBinaryBiproducts D] (A : D) [CategoryTheory.MonObj A] (M N : CategoryTheory.Mod D A) : CategoryTheory.CategoryStruct.comp (modBiprodAct A M N) CategoryTheory.Limits.biprod.snd = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A CategoryTheory.Limits.biprod.snd) (actLeft A N.X)

The second projection intertwines the actions.

noncomputable def RS.modBiprodInl {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasBinaryBiproducts D] (A : D) [CategoryTheory.MonObj A] (M N : CategoryTheory.Mod D A) : M ⟶ modBiprod A M N

The first injection is a module map.

Equations

• RS.modBiprodInl A M N = CategoryTheory.Mod.Hom.mk' CategoryTheory.Limits.biprod.inl ⋯

noncomputable def RS.modBiprodInr {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasBinaryBiproducts D] (A : D) [CategoryTheory.MonObj A] (M N : CategoryTheory.Mod D A) : N ⟶ modBiprod A M N

The second injection is a module map.

Equations

• RS.modBiprodInr A M N = CategoryTheory.Mod.Hom.mk' CategoryTheory.Limits.biprod.inr ⋯

noncomputable def RS.modBiprodFst {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasBinaryBiproducts D] (A : D) [CategoryTheory.MonObj A] (M N : CategoryTheory.Mod D A) : modBiprod A M N ⟶ M

The first projection is a module map.

Equations

• RS.modBiprodFst A M N = CategoryTheory.Mod.Hom.mk' CategoryTheory.Limits.biprod.fst ⋯

noncomputable def RS.modBiprodSnd {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasBinaryBiproducts D] (A : D) [CategoryTheory.MonObj A] (M N : CategoryTheory.Mod D A) : modBiprod A M N ⟶ N

The second projection is a module map.

Equations

• RS.modBiprodSnd A M N = CategoryTheory.Mod.Hom.mk' CategoryTheory.Limits.biprod.snd ⋯

@[simp]

theorem RS.modBiprodInl_hom {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasBinaryBiproducts D] (A : D) [CategoryTheory.MonObj A] (M N : CategoryTheory.Mod D A) : (modBiprodInl A M N).hom = CategoryTheory.Limits.biprod.inl

@[simp]

theorem RS.modBiprodInr_hom {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasBinaryBiproducts D] (A : D) [CategoryTheory.MonObj A] (M N : CategoryTheory.Mod D A) : (modBiprodInr A M N).hom = CategoryTheory.Limits.biprod.inr

theorem RS.modBiprodAct_map {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasBinaryBiproducts D] (A : D) [CategoryTheory.MonObj A] (M N : CategoryTheory.Mod D A) {M' N' : CategoryTheory.Mod D A} (f : M ⟶ M') (g : N ⟶ N') : CategoryTheory.CategoryStruct.comp (modBiprodAct A M N) (CategoryTheory.Limits.biprod.map f.hom g.hom) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (CategoryTheory.Limits.biprod.map f.hom g.hom)) (modBiprodAct A M' N')

Componentwise maps intertwine the biproduct actions.

noncomputable def RS.modBiprodMap {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasBinaryBiproducts D] (A : D) [CategoryTheory.MonObj A] (M N : CategoryTheory.Mod D A) {M' N' : CategoryTheory.Mod D A} (f : M ⟶ M') (g : N ⟶ N') : modBiprod A M N ⟶ modBiprod A M' N'

Functoriality of the module biproduct.

Equations

• RS.modBiprodMap A M N f g = CategoryTheory.Mod.Hom.mk' (CategoryTheory.Limits.biprod.map f.hom g.hom) ⋯

@[simp]

theorem RS.modBiprodMap_hom {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasBinaryBiproducts D] (A : D) [CategoryTheory.MonObj A] (M N : CategoryTheory.Mod D A) {M' N' : CategoryTheory.Mod D A} (f : M ⟶ M') (g : N ⟶ N') : (modBiprodMap A M N f g).hom = CategoryTheory.Limits.biprod.map f.hom g.hom

noncomputable def RS.modBiprodMapIso {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasBinaryBiproducts D] (A : D) [CategoryTheory.MonObj A] (M N : CategoryTheory.Mod D A) {M' N' : CategoryTheory.Mod D A} (e₁ : M ≅ M') (e₂ : N ≅ N') : modBiprod A M N ≅ modBiprod A M' N'

The module biproduct of two isomorphisms.

Equations

• RS.modBiprodMapIso A M N e₁ e₂ = { hom := RS.modBiprodMap A M N e₁.hom e₂.hom, inv := RS.modBiprodMap A M' N' e₁.inv e₂.inv, hom_inv_id := ⋯, inv_hom_id := ⋯ }

@[simp]

theorem RS.modBiprodFst_hom {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasBinaryBiproducts D] (A : D) [CategoryTheory.MonObj A] (M N : CategoryTheory.Mod D A) : (modBiprodFst A M N).hom = CategoryTheory.Limits.biprod.fst

@[simp]

theorem RS.modBiprodSnd_hom {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasBinaryBiproducts D] (A : D) [CategoryTheory.MonObj A] (M N : CategoryTheory.Mod D A) : (modBiprodSnd A M N).hom = CategoryTheory.Limits.biprod.snd

theorem RS.modBiprodAct_braiding {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasBinaryBiproducts D] (A : D) [CategoryTheory.MonObj A] (M N : CategoryTheory.Mod D A) : CategoryTheory.CategoryStruct.comp (modBiprodAct A M N) (CategoryTheory.Limits.biprod.braiding M.X N.X).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (CategoryTheory.Limits.biprod.braiding M.X N.X).hom) (modBiprodAct A N M)

The braiding of a module biproduct is linear.

noncomputable def RS.modBiprodSymmIso {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasBinaryBiproducts D] (A : D) [CategoryTheory.MonObj A] (M N : CategoryTheory.Mod D A) : modBiprod A M N ≅ modBiprod A N M

The biproduct of modules is symmetric.

Equations

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

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

The action on the left-nested triple biproduct, retyped.

Equations

• RS.actLeftNest A M N P = RS.modBiprodAct A (RS.modBiprod A M N) P

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

The action on the right-nested triple biproduct, retyped.

Equations

• RS.actRightNest A M N P = RS.modBiprodAct A M (RS.modBiprod A N P)

theorem RS.modBiprodAct_associator {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasBinaryBiproducts D] (A : D) [CategoryTheory.MonObj A] (M N P : CategoryTheory.Mod D A) : CategoryTheory.CategoryStruct.comp (actLeftNest A M N P) (CategoryTheory.Limits.biprod.associator M.X N.X P.X).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (CategoryTheory.Limits.biprod.associator M.X N.X P.X).hom) (actRightNest A M N P)

The associator of a module biproduct is linear.

noncomputable def RS.modBiprodAssocIso {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasBinaryBiproducts D] (A : D) [CategoryTheory.MonObj A] (M N P : CategoryTheory.Mod D A) : modBiprod A (modBiprod A M N) P ≅ modBiprod A M (modBiprod A N P)

The biproduct of modules is associative.

Equations

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