Free modules on units and biproducts

The free module on the tensor unit is the regular module, and the free module on a biproduct is the biproduct of the free modules: the bookkeeping of the mixed free part of the dévissage decomposition.

theorem RS.freeModUnit_linear {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (B : D) [CategoryTheory.MonObj B] : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator B B (CategoryTheory.MonoidalCategoryStruct.tensorUnit D)).inv (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.mul (CategoryTheory.MonoidalCategoryStruct.tensorUnit D))) (CategoryTheory.MonoidalCategoryStruct.rightUnitor B).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft B (CategoryTheory.MonoidalCategoryStruct.rightUnitor B).hom) CategoryTheory.MonObj.mul

The right unitor intertwines the free action on the unit with the regular action.

noncomputable def RS.freeModUnitIso {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (B : D) [CategoryTheory.MonObj B] : freeMod B (CategoryTheory.MonoidalCategoryStruct.tensorUnit D) ≅ regularMod B

The free module on the unit is the regular module.

Equations

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

theorem RS.freeModBiprod_linear {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasBinaryBiproducts D] (B : D) [CategoryTheory.MonObj B] (X Y : D) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator B B (X ⊞ Y)).inv (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.mul (X ⊞ Y))) (CategoryTheory.Limits.biprod.lift (CategoryTheory.MonoidalCategoryStruct.whiskerLeft B CategoryTheory.Limits.biprod.fst) (CategoryTheory.MonoidalCategoryStruct.whiskerLeft B CategoryTheory.Limits.biprod.snd)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft B (CategoryTheory.Limits.biprod.lift (CategoryTheory.MonoidalCategoryStruct.whiskerLeft B CategoryTheory.Limits.biprod.fst) (CategoryTheory.MonoidalCategoryStruct.whiskerLeft B CategoryTheory.Limits.biprod.snd))) (modBiprodAct B (freeMod B X) (freeMod B Y))

The distributor intertwines the free actions.

theorem RS.act_inv_of_act_hom {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (B : D) {P Q : D} {actP : CategoryTheory.MonoidalCategoryStruct.tensorObj B P ⟶ P} {actQ : CategoryTheory.MonoidalCategoryStruct.tensorObj B Q ⟶ Q} (e : P ≅ Q) (h : CategoryTheory.CategoryStruct.comp actP e.hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft B e.hom) actQ) : CategoryTheory.CategoryStruct.comp actQ e.inv = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft B e.inv) actP

The inverse of a linear isomorphism is linear.

noncomputable def RS.freeModBiprodIso {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasBinaryBiproducts D] (B : D) [CategoryTheory.MonObj B] (X Y : D) : freeMod B (X ⊞ Y) ≅ modBiprod B (freeMod B X) (freeMod B Y)

The free module on a biproduct is the biproduct of the free modules.

Equations

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

noncomputable def RS.freeModMapIso {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (B : D) [CategoryTheory.MonObj B] {V W : D} (e : V ≅ W) : freeMod B V ≅ freeMod B W

The free module on an isomorphism.

Equations

• RS.freeModMapIso B e = { hom := RS.freeModMap B e.hom, inv := RS.freeModMap B e.inv, hom_inv_id := ⋯, inv_hom_id := ⋯ }