English
A simplification form of lift_unique asserting the same equality in a simplified form.
Русский
Упрощенная форма lift_unique, утверждающая ту же эквивалентность в упрощенной форме.
LaTeX
$$$\text{simp}\,\text{lift_unique}$$$
Lean4
/-- The free algebra on `X` is "just" the monoid algebra on the free monoid on `X`.
This would be useful when constructing linear maps out of a free algebra,
for example.
-/
noncomputable def equivMonoidAlgebraFreeMonoid : FreeAlgebra R X ≃ₐ[R] MonoidAlgebra R (FreeMonoid X) :=
AlgEquiv.ofAlgHom (lift R fun x ↦ (MonoidAlgebra.of R (FreeMonoid X)) (FreeMonoid.of x))
((MonoidAlgebra.lift R (FreeMonoid X) (FreeAlgebra R X)) (FreeMonoid.lift (ι R)))
(by
apply MonoidAlgebra.algHom_ext; intro x
refine FreeMonoid.recOn x ?_ ?_
· simp
rfl
· intro x y ih
simp at ih
simp [ih])
(by
ext
simp)
