English
The canonical embedding from FreeRing α to FreeCommRing α agrees with the map given by translating words to multisets; i.e., the embedding corresponds to mapping lists of generators to their multisets of letters.
Русский
Каноническое вложение из FreeRing α в FreeCommRing α согласуется с отображением, переводящим слова в мультимножества; вложение эквивалентно отображению списка генераторов в мультсет его букв.
LaTeX
$$$\\uparrow = \\mathrm{FreeAbelianGroup}.lift(\\text{on lists to multisets})$ (equivalently, the embedding corresponds to lists $l:\\mathrm{List}(\\alpha)$ mapping to $(l:\\mathrm{Multiset}(\\alpha))$)$$
Lean4
theorem coe_eq :
((↑) : FreeRing α → FreeCommRing α) = @Functor.map FreeAbelianGroup _ _ _ fun l : List α => (l : Multiset α) :=
by
funext x
dsimp [castFreeCommRing, toFreeCommRing, FreeRing.lift, FreeRing, FreeAbelianGroup.liftMonoid_coe, Functor.map]
rw [← AddMonoidHom.coe_coe]
apply FreeAbelianGroup.lift_unique; intro L
simp only [AddMonoidHom.coe_coe, comp_apply, FreeAbelianGroup.lift_apply_of]
exact
FreeMonoid.recOn L rfl fun hd tl ih =>
by
rw [(FreeMonoid.lift _).map_mul, FreeMonoid.lift_eval_of, ih]
conv_lhs => reduce
rfl
