English
The generating relation rel' for the power algebra is defined as the relation rel on the direct sum via the lof map, encoding how tensor powers couple with the direct sum.
Русский
Генерирующее отношение rel' для пауэр-алгебры задаётся как отношение rel на прямую сумму через отображение lof, кодирующее связь тензорных степеней с прямой суммой.
LaTeX
$$$\\text{rel'} := \\text{rel } R A \\;\\text{onDirectSum}$$$
Lean4
/-- The generating equivalence relation for elements of the free tensor algebra
that are identified in the free product -/
inductive rel : FreeTensorAlgebra R A → FreeTensorAlgebra R A → Prop
| id : ∀ {i : I}, rel (ι R <| lof R I A i 1) 1
|
prod :
∀ {i : I} {a₁ a₂ : A i},
rel
(tprod R (⨁ i, A i) 2
(fun
| 0 => lof R I A i a₁
| 1 => lof R I A i a₂))
(ι R <| lof R I A i (a₁ * a₂))
