rTensor — Mathlib

English

The rTensor construction gives the natural bialgebra morphism induced by f: B →_c[R] C on the right factor, yielding B ⊗ A →_bialg C ⊗ A.

Русский

Конструкция rTensor даёт естественный билигебральный морфизм, индуцированный f: B →_c[R] C на правом компоненте, от B ⊗ A к C ⊗ A.

LaTeX

$$$\mathrm{rTensor}(f) : B \otimes_R A \to_{bialg} C \otimes_R A$$$

Lean4

/-- `rTensor A f : B ⊗ A →ₐc C ⊗ A` is the natural bialgebra morphism induced by `f : B →ₐc C`. -/
noncomputable abbrev rTensor (f : B →ₐc[R] C) : B ⊗[R] A →ₐc[R] C ⊗[R] A :=
  Bialgebra.TensorProduct.map f (BialgHom.id R A)

Похожие утверждения