The trivial module as a free module

Over the tensor unit as base algebra the free module on V and the trivial module on V agree, through the left unitor.

• unitFreeIso: the trivial module unitMod V is isomorphic, as a module over the unit, to the free module freeMod (𝟙_ D) V, by the inverse left unitor (λ_ V).inv : V ⟶ 𝟙_ D ⊗ V.

This is the collapse freeModUnitBase read in the direction that presents a bare object as a free module; the linearity of either leg is the coherence identity in the monoidal unit recorded by freeModUnitBase_linear and freeModUnitBase_linear_inv.

noncomputable def RS.unitFreeIso {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (V : D) : unitMod V ≅ freeMod (CategoryTheory.MonoidalCategoryStruct.tensorUnit D) V

The trivial module on V is the free module on V over the tensor unit, through the inverse left unitor.

Equations

• RS.unitFreeIso V = (RS.freeModUnitBase V).symm

@[simp]

theorem RS.unitFreeIso_hom_hom {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (V : D) : (unitFreeIso V).hom.hom = (CategoryTheory.MonoidalCategoryStruct.leftUnitor V).inv

@[simp]

theorem RS.unitFreeIso_inv_hom {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (V : D) : (unitFreeIso V).inv.hom = (CategoryTheory.MonoidalCategoryStruct.leftUnitor V).hom