A *-algebra structure on the free algebra. #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.free_monoid and algebra.free_algebra, to avoid importing algebra.star.basic into the entire hierarchy.

source

@[protected, instance]

def free_monoid.star_semigroup {α : Type u_1} :

star_semigroup (free_monoid α)

Equations

free_monoid.star_semigroup = {to_has_involutive_star := {to_has_star := {star := list.reverse α}, star_involutive := _}, star_mul := _}

source

@[simp]

theorem free_monoid.star_of {α : Type u_1} (x : α) :

has_star.star (free_monoid.of x) = free_monoid.of x

source

@[simp]

theorem free_monoid.star_one {α : Type u_1} :

has_star.star 1 = 1

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

source

@[protected, instance]

def free_algebra.star_ring {R : Type u_1} [comm_semiring R] {X : Type u_2} :

star_ring (free_algebra R X)

The star ring formed by reversing the elements of products

Equations

free_algebra.star_ring = {to_star_semigroup := {to_has_involutive_star := {to_has_star := {star := mul_opposite.unop ∘ ⇑(⇑(free_algebra.lift R) (mul_opposite.op ∘ free_algebra.ι R))}, star_involutive := _}, star_mul := _}, star_add := _}

source

@[simp]

theorem free_algebra.star_ι {R : Type u_1} [comm_semiring R] {X : Type u_2} (x : X) :

has_star.star (free_algebra.ι R x) = free_algebra.ι R x

source

@[simp]

theorem free_algebra.star_algebra_map {R : Type u_1} [comm_semiring R] {X : Type u_2} (r : R) :

has_star.star (⇑(algebra_map R (free_algebra R X)) r) = ⇑(algebra_map R (free_algebra R X)) r

source

def free_algebra.star_hom {R : Type u_1} [comm_semiring R] {X : Type u_2} :

free_algebra R X ≃ₐ[R] (free_algebra R X)ᵐᵒᵖ

star as an alg_equiv

Equations

free_algebra.star_hom = {to_fun := star_ring_equiv.to_fun, inv_fun := star_ring_equiv.inv_fun, left_inv := _, right_inv := _, map_mul' := _, map_add' := _, commutes' := _}