English
For linear maps f and g, tensoring with M preserves the equalizer: the equalizer of the tensorized maps is exactly the image under LTensor of the equalizer of f and g.
Русский
Для линейных отображений f и g тензоризация сохраняет область равенства: равная система после тензорирования совпадает с образцом области равенства f и g под действием lTensor.
LaTeX
$$$\operatorname{eqLocus}(\mathrm{AlgebraTensorModule.lTensor}(S,M,f),\mathrm{AlgebraTensorModule.lTensor}(S,M,g)) = \mathrm{range}\bigl(\mathrm{AlgebraTensorModule.lTensor}(S,M,\operatorname{eqLocus}(f,g)).\text{subtype}\bigr).$$$
Lean4
theorem eqLocus_lTensor_eq [Module.Flat R M] :
LinearMap.eqLocus (AlgebraTensorModule.lTensor S M f) (AlgebraTensorModule.lTensor S M g) =
LinearMap.range (AlgebraTensorModule.lTensor S M (LinearMap.eqLocus f g).subtype) :=
by
rw [LinearMap.eqLocus_eq_ker_sub, LinearMap.eqLocus_eq_ker_sub]
rw [← map_sub, ker_lTensor_eq]
