Finite-dimensional inner product space with a (co)algebra structure

This file proves that a finite-dimensional inner product space has a colagebra structure if it has an algebra structure, where the comultiplication and counit maps are given by taking adjoints of the multiplication and algebra linear maps, respectively. This is implemented by providing a linear equivalence between the inner product space and a normed algebra.

And similarly, a finite-dimensional inner product space has an algebra structure if it has a coalgebra structure, where x * y = (adjoint comul) (x ⊗ₜ y), (1 : A) = (adjoint counit) (1 : 𝕜) and algebraMap = adjoint counit.

This is useful for when we have a finite-dimensional C⋆-algebra with a faithful and positive linear functional (so that it induces an inner product structure), and want the coalgebra structure to be the adjoint of the algebra structure. This comes up in non-commutative graph theory for example.

@[reducible, inline]

noncomputable abbrev InnerProductSpace.coalgebraOfAlgebra {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {A : Type u_3} [NormedRing A] [NormedSpace 𝕜 A] [SMulCommClass 𝕜 A A] [IsScalarTower 𝕜 A A] (e : E ≃ₗ[𝕜] A) : Coalgebra 𝕜 E

A finite-dimensional inner product space with an algebra structure induces a coalgebra, where comultiplication is given by the adjoint of multiplication and the counit is given by the adjoint of the algebra map.

This is implemented by providing a linear equivalence between the inner product space and a normed algebra.

See note [reducible non-instances].

Equations

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

@[reducible, inline]

noncomputable abbrev InnerProductSpace.mulOfCoalgebra {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [Coalgebra 𝕜 E] : Mul E

The multiplication on a finite-dimensional inner product space with a coalgebra structure given by x * y = (adjoint comul) (x ⊗ₜ y).

See note [reducible non-instances].

Equations

• InnerProductSpace.mulOfCoalgebra = { mul := fun (x y : E) => (LinearMap.adjoint CoalgebraStruct.comul) (x ⊗ₜ[𝕜] y) }

theorem InnerProductSpace.AlgebraOfCoalgebra.mul_def {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [Coalgebra 𝕜 E] (x y : E) : x * y = (LinearMap.adjoint CoalgebraStruct.comul) (x ⊗ₜ[𝕜] y)

@[reducible, inline]

noncomputable abbrev InnerProductSpace.ringOfCoalgebra {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [Coalgebra 𝕜 E] : Ring E

A finite-dimensional inner product space with a coalgebra structure induces a ring structure, where multiplication is given by x * y = (adjoint comul) (x ⊗ₜ y) and 1 = (adjoint counit) (1 : 𝕜).

See note [reducible non-instances].

Equations

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

@[reducible, inline]

noncomputable abbrev InnerProductSpace.algebraOfCoalgebra {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [Coalgebra 𝕜 E] : Algebra 𝕜 E

A finite-dimensional inner product space with a coalgebra structure induces an algebra structure, where x * y = (adjoint comul) (x ⊗ₜ y), 1 = (adjoint counit) 1 and algebraMap = adjoint counit.

See note [reducible non-instances].

Equations

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