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