The scalar unit as a ring isomorphism

The scalar-unit hypothesis says that scaling the identity of the tensor unit is a bijection from the complex numbers. It is also a ring homomorphism, so it is a ring isomorphism, which is the form in which the ℂ-linear structure of the Ind-completion consumes it.

def RS.scalarUnitRingHom (A : Type u) [CategoryTheory.Category.{v, u} A] [CategoryTheory.Preadditive A] [CategoryTheory.Linear ℂ A] [CategoryTheory.MonoidalCategory A] : ℂ →+* CategoryTheory.End (CategoryTheory.MonoidalCategoryStruct.tensorUnit A)

Scaling the identity of the tensor unit, as a ring homomorphism.

Equations

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

noncomputable def RS.scalarUnitEquiv {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Preadditive A] [CategoryTheory.Linear ℂ A] [CategoryTheory.MonoidalCategory A] (h : HasScalarUnit A) : ℂ ≃+* CategoryTheory.End (CategoryTheory.MonoidalCategoryStruct.tensorUnit A)

The scalar unit as a ring isomorphism.

Equations

• RS.scalarUnitEquiv h = RingEquiv.ofBijective (RS.scalarUnitRingHom A) h

@[simp]

theorem RS.scalarUnitEquiv_apply {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Preadditive A] [CategoryTheory.Linear ℂ A] [CategoryTheory.MonoidalCategory A] (h : HasScalarUnit A) (c : ℂ) : (scalarUnitEquiv h) c = c • CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit A)