lTensor — Mathlib

English

There is a natural coalgebra morphism lTensor sending m ⊗ n to m ⊗ f(n) induced by a coalgebra morphism f: N →ₗc[R] P, acting as identity on M.

Русский

Существует естественный коалгебраический морфизм lTensor, переводящий m ⊗ n в m ⊗ f(n), индуцируемый коалгоморфизмом f: N →ₗc[R] P, действующий как тождественный на M.

LaTeX

$$$\\mathrm{lTensor}(f) : M \\otimes N \\to_{coalg} M \\otimes P \\quad (\\text{defined by } f)$$$

Lean4

/-- `lTensor M f : M ⊗ N →ₗc M ⊗ P` is the natural coalgebra morphism induced by `f : N →ₗc P`. -/
noncomputable abbrev lTensor (f : N →ₗc[R] P) : M ⊗[R] N →ₗc[R] M ⊗[R] P :=
  Coalgebra.TensorProduct.map (CoalgHom.id R M) f

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