English
The Free Algebra on X over R carries a star-structure defined by reversing the order of factors; star is involutive and anti-multiplicative, and star distributes over addition.
Русский
Свободная алгебра на X над R оснащена операцией звезды, обращающей порядок факторов; звезда инволютивна и антипроизводна, а также раскрывается по сложению.
LaTeX
$$$\text{FreeAlgebra}(R,X)$ имеет структуру StarRing: $\star(uv) = \star(v)\star(u)$, $\star(\star x)=x$, $\star(x+y)=\star x + \star y$.$$
Lean4
/-- The star ring formed by reversing the elements of products -/
instance : StarRing (FreeAlgebra R X)
where
star := MulOpposite.unop ∘ lift R (MulOpposite.op ∘ ι R)
star_involutive
x := by
simp only [Function.comp_apply]
let y := lift R (X := X) (MulOpposite.op ∘ ι R)
refine induction (motive := fun x ↦ (y (y x).unop).unop = x) _ _ ?_ ?_ ?_ ?_ x
· intros
simp only [AlgHom.commutes, MulOpposite.algebraMap_apply, MulOpposite.unop_op]
· intros
simp only [y, lift_ι_apply, Function.comp_apply, MulOpposite.unop_op]
· intros
simp only [*, map_mul, MulOpposite.unop_mul]
· intros
simp only [*, map_add, MulOpposite.unop_add]
star_mul a b := by simp only [Function.comp_apply, map_mul, MulOpposite.unop_mul]
star_add a b := by simp only [Function.comp_apply, map_add, MulOpposite.unop_add]
