English
Let B be a Hopf algebra over S and A a Hopf algebra over R, with compatible algebra structures and a common ground ring R. Then the antipode on the tensor product B ⊗_R A is obtained by applying the antipodes on each factor, i.e. the antipode map on B ⊗_R A is the AlgebraTensorModule map of antipodes on B and A. Concretely, on pure tensors, S_B⊗A(b ⊗ a) = S_B(b) ⊗ S_A(a).
Русский
Пусть B — Hopf-алгебра над S, A — Hopf-алгебра над R, единые основания R и совместимая структура скаляров. Тогда antipode на тензорном произведении B ⊗_R A задаётся применением antipode к каждому фактору: на чистом тензоре b ⊗ a выполняется S_B⊗A(b ⊗ a) = S_B(b) ⊗ S_A(a).
LaTeX
$$$$\operatorname{antipode}_{B\otimes_R A} = \operatorname{AlgebraTensorModule.map}(\operatorname{antipode}_B, \operatorname{antipode}_A),\quad (\operatorname{antipode}_{B\otimes_R A})(b\otimes a) = \operatorname{antipode}_B(b) \otimes \operatorname{antipode}_A(a). $$$$
Lean4
@[simp]
theorem antipode_def : antipode S (A := B ⊗[R] A) = AlgebraTensorModule.map (antipode S) (antipode R) :=
rfl
