tensorKer — Mathlib

English

There is a canonical map from M ⊗ ker f to ker(lTensor S M f), providing a concrete tensor-theoretic realization of the kernel relation after tensoring.

Русский

Существует каноническое отображение от M ⊗ ker f к ker(lTensor S M f), дающее конкретную тензорную реализацию связи ядра после тензорирования.

LaTeX

$$$\text{tensorKer} : M \otimes_R ker f \to_\text{S} ker( lTensor\; S\; M\; f )$$$

Lean4

/-- The canonical map `M ⊗[R] ker f →ₗ[R] ker (𝟙 ⊗ f)`. -/
def tensorKer : M ⊗[R] (LinearMap.ker f) →ₗ[S] LinearMap.ker (AlgebraTensorModule.lTensor S M f) :=
  AlgebraTensorModule.lift (f.tensorKerBil S M)

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