English
If g is surjective, the kernel of the left-tensor product map is generated by the kernel of g.
Русский
Если g сюръективен, ядро левойTensor отображения тензорного произведения генерируется ядром g.
LaTeX
$$$\\ker(\\mathrm{Algebra.TensorProduct.map}(\\mathrm{id}_A, g)) = (\\ker g).map(\\mathrm{Algebra.TensorProduct.includeLeft})$$$
Lean4
/-- If `g` is surjective, then the kernel of `(id A) ⊗ g` is generated by the kernel of `g` -/
theorem lTensor_ker (hg : Function.Surjective g) :
RingHom.ker (map (AlgHom.id R A) g) = (RingHom.ker g).map (Algebra.TensorProduct.includeRight : C →ₐ[R] A ⊗[R] C) :=
by
rw [← Submodule.restrictScalars_inj R]
have :
(RingHom.ker (map (AlgHom.id R A) g)).restrictScalars R =
LinearMap.ker (LinearMap.lTensor A (AlgHom.toLinearMap g)) :=
rfl
rw [this, Ideal.map_includeRight_eq]
rw [(lTensor_exact A g.toLinearMap.exact_subtype_ker_map hg).linearMap_ker_eq]
rfl
