lTensor — Mathlib

English

The canonical coevaluation of lTensor equals the lifted version of the corresponding LTensor map.

Русский

Коэвалюация lTensor равна поднятой версии соответствующей карты LTensor.

LaTeX

$$$ (lTensor\; A\; M\; f) : M \otimes_R N \to_A M \otimes_R Q \;\text{ coe } = f.lTensor M$$$

Lean4

/-- Heterobasic version of `LinearMap.lTensor` -/
def lTensor : (N →ₗ[R] Q) →ₗ[R] M ⊗[R] N →ₗ[A] M ⊗[R] Q
    where
  toFun f := map LinearMap.id f
  map_add' f₁ f₂ := map_add_right _ f₁ f₂
  map_smul' _ _ := map_smul_right _ _ _

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