The scalar-unit hypothesis from a scalar unit

Under the linear structure induced by a ring isomorphism ℂ ≃+* End (𝟙_ D), scaling the identity of the unit recovers the isomorphism, so the scalar-unit hypothesis holds. Applied to the ind-completion this supplies the hypothesis upstairs from the one downstairs.

theorem RS.scalarEnd_unit {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Preadditive D] (φ : ℂ ≃+* CategoryTheory.End (CategoryTheory.MonoidalCategoryStruct.tensorUnit D)) (c : ℂ) : scalarEnd φ c (CategoryTheory.MonoidalCategoryStruct.tensorUnit D) = scalarHom φ c

Scaling the identity of the unit recovers the scalar.

theorem RS.hasScalarUnit_of_scalarUnit {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] (φ : ℂ ≃+* CategoryTheory.End (CategoryTheory.MonoidalCategoryStruct.tensorUnit D)) : HasScalarUnit D

The scalar-unit hypothesis holds under the induced linear structure.