The tensor unit of ModuleCat R

The tensor unit 𝟙_ (ModuleCat R) of the monoidal category of modules over a commutative ring R is R itself. This file records the consequences that instance search and Module.finrank do not see through the monoidal structure: the unit is a free, finitely generated R-module (ModuleCat.free_tensorUnit, ModuleCat.finite_tensorUnit), of rank one when R satisfies the strong rank condition (ModuleCat.finrank_tensorUnit).

instance ModuleCat.free_tensorUnit (R : Type u) [CommRing R] : Module.Free R ↑(CategoryTheory.MonoidalCategoryStruct.tensorUnit (ModuleCat R))

The tensor unit of ModuleCat R, which is R itself, is a free R-module.

instance ModuleCat.finite_tensorUnit (R : Type u) [CommRing R] : Module.Finite R ↑(CategoryTheory.MonoidalCategoryStruct.tensorUnit (ModuleCat R))

The tensor unit of ModuleCat R, which is R itself, is a finitely generated R-module.

@[simp]

theorem ModuleCat.finrank_tensorUnit (R : Type u) [CommRing R] [StrongRankCondition R] : Module.finrank R ↑(CategoryTheory.MonoidalCategoryStruct.tensorUnit (ModuleCat R)) = 1

The tensor unit of ModuleCat R, which is R itself, has rank one over R.