English
A ker equality for a TensorProduct map with HasQuotient.Quotient describes the relation ker(TensorProduct.mk ... 1) and the image of a submodule via TensorProduct maps, linking to right-exactness results.
Русский
Утверждается отношение между ядром и образом линейного отображения, возникающего из тензорирования и квотирования.
LaTeX
$$ker (LinearMap.instFunLike.coe (TensorProduct.mk R (HasQuotient.Quotient R I) Q) 1) = I • ⊤$$
Lean4
theorem ker_tensorProductMk {I : Ideal R} : ker (TensorProduct.mk R (R ⧸ I) Q 1) = I • ⊤ :=
by
apply comap_injective_of_surjective (TensorProduct.lid R Q).surjective
rw [← comap_coe_toLinearMap, ← ker_comp]
convert rTensor_mkQ Q I
· ext; simp
rw [← comap_coe_toLinearMap, ← toLinearMap_eq_coe, comap_equiv_eq_map_symm, toLinearMap_eq_coe, map_coe_toLinearMap,
map_symm_eq_iff, map_range_rTensor_subtype_lid]
