English
There is a bilinear construction that takes a module M and a kernel element x in ker f to produce an element in the kernel of the lifted map lTensor S M f, bilinear in M and ker f.
Русский
Существует билинейная конструкция, которая выводит элемент ядра растянутого отображения из M в ker f в ядро отображения lTensor(S,M,f), билинейна по M и ker f.
LaTeX
$$$\text{tensorKerBil} : M \to_\text{S} (ker f) \to_\text{R} ker( lTensor\; S\; M\; f )$$$
Lean4
/-- The bilinear map corresponding to `LinearMap.tensorKer`. -/
def tensorKerBil : M →ₗ[S] LinearMap.ker f →ₗ[R] LinearMap.ker (AlgebraTensorModule.lTensor S M f)
where
toFun
m :=
{ toFun := fun a ↦ ⟨m ⊗ₜ a, by simp⟩
map_add' := fun x y ↦ by simp [tmul_add]
map_smul' := fun r x ↦ by simp }
map_add' x y := by ext; simp [add_tmul]
map_smul' r x := by ext y; simp [smul_tmul']
