English
If f and g are surjective algebra morphisms, the kernel of their tensor product map is generated by the kernels of f and g, via left and right inclusions respectively.
Русский
Если f и g — сюръективные морфизмы алгебр, то ядро отображения тензорного произведения порождается ядрами f и g через соответствующие левое и правое включения.
LaTeX
$$$\\ker(\\mathrm{Algebra.TensorProduct.map}(f,g)) = \\ker f\\mapsto \\mathrm{includeLeft} ⊔ \\ker g\\mapsto \\mathrm{includeRight}$$$
Lean4
/-- If `f` and `g` are surjective morphisms of algebras, then
the kernel of `Algebra.TensorProduct.map f g` is generated by the kernels of `f` and `g` -/
theorem map_ker (hf : Function.Surjective f) (hg : Function.Surjective g) :
RingHom.ker (map f g) =
(RingHom.ker f).map (Algebra.TensorProduct.includeLeft : A →ₐ[R] A ⊗[R] C) ⊔
(RingHom.ker g).map (Algebra.TensorProduct.includeRight : C →ₐ[R] A ⊗[R] C) :=
by
-- rewrite map f g as the composition of two maps
have : map f g = (map f (AlgHom.id R D)).comp (map (AlgHom.id R A) g) := ext rfl rfl
rw [this]
-- this needs some rewriting to RingHom
-- TODO: can `RingHom.comap_ker` take an arbitrary `RingHomClass`, rather than just `RingHom`?
simp only [AlgHom.ker_coe, AlgHom.comp_toRingHom]
rw [← RingHom.comap_ker]
simp only [← AlgHom.ker_coe]
-- apply one step of exactness
rw [← Algebra.TensorProduct.lTensor_ker _ hg, RingHom.ker_eq_comap_bot (map (AlgHom.id R A) g)]
rw [← Ideal.comap_map_of_surjective (map (AlgHom.id R A) g) (LinearMap.lTensor_surjective A hg)]
-- apply the other step of exactness
rw [Algebra.TensorProduct.rTensor_ker _ hf]
apply congr_arg₂ _ rfl
simp only [AlgHom.coe_ideal_map, Ideal.map_map]
rw [← AlgHom.comp_toRingHom, Algebra.TensorProduct.map_comp_includeLeft]
rfl
