lift — Mathlib

English

Two linear maps from M ⊗ N to P that agree on all simple tensors are equal.

Русский

Два линейных отображения из M ⊗ N в P, совпадающих на всех простых тензорах, равны.

LaTeX

$$$\\forall g,h : M ⊗_R N \\to P,\\; (\\forall x,y, g(x ⊗ y) = h(x ⊗ y)) \\Rightarrow g = h$.$$

Lean4

/-- Constructing a linear map `M ⊗ N → P` given a bilinear map `M → N → P` with the property that
its composition with the canonical bilinear map `M → N → M ⊗ N` is
the given bilinear map `M → N → P`.

This works for semilinear maps. -/
def lift : M ⊗[R] N →ₛₗ[σ₁₂] P₂ :=
  { liftAux f' with map_smul' := liftAux.smulₛₗ }

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