A *-algebra structure on the free algebra.

Reversing words gives a *-structure on the free monoid or on the free algebra on a type.

Implementation note

We have this in a separate file, rather than in Algebra.FreeMonoid and Algebra.FreeAlgebra, to avoid importing Algebra.Star.Basic into the entire hierarchy.

instance FreeMonoid.instStarMulFreeMonoidToMulToMulOneClassToMonoidToRightCancelMonoidInstCancelMonoidFreeMonoid {α : Type u_1} : StarMul (FreeMonoid α)

Equations

• FreeMonoid.instStarMulFreeMonoidToMulToMulOneClassToMonoidToRightCancelMonoidInstCancelMonoidFreeMonoid = StarMul.mk ⋯

@[simp]

theorem FreeMonoid.star_of {α : Type u_1} (x : α) : star (FreeMonoid.of x) = FreeMonoid.of x

@[simp]

theorem FreeMonoid.star_one {α : Type u_1} : star 1 = 1

Note that star_one is already a global simp lemma, but this one works with dsimp too

instance FreeAlgebra.instStarRingFreeAlgebraToNonUnitalNonAssocSemiringToNonAssocSemiringInstSemiringFreeAlgebra {R : Type u_1} [CommSemiring R] {X : Type u_2} : StarRing (FreeAlgebra R X)

The star ring formed by reversing the elements of products

Equations

• FreeAlgebra.instStarRingFreeAlgebraToNonUnitalNonAssocSemiringToNonAssocSemiringInstSemiringFreeAlgebra = StarRing.mk ⋯

@[simp]

theorem FreeAlgebra.star_ι {R : Type u_1} [CommSemiring R] {X : Type u_2} (x : X) : star (FreeAlgebra.ι R x) = FreeAlgebra.ι R x

@[simp]

theorem FreeAlgebra.star_algebraMap {R : Type u_1} [CommSemiring R] {X : Type u_2} (r : R) : star ((algebraMap R (FreeAlgebra R X)) r) = (algebraMap R (FreeAlgebra R X)) r

def FreeAlgebra.starHom {R : Type u_1} [CommSemiring R] {X : Type u_2} : FreeAlgebra R X ≃ₐ[R] (FreeAlgebra R X)ᵐᵒᵖ

star as an AlgEquiv

Equations

• FreeAlgebra.starHom = let __src := starRingEquiv; { toEquiv := __src.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }