map_surjective — Mathlib

English

Let g: N → P and g': N' → P' be surjective linear maps between R-modules. Then the induced map on tensor products TensorProduct.map g g' : N ⊗_R N' → P ⊗_R P' is surjective.

Русский

Пусть g: N → P и g': N' → P' – сюръективные линейные отображения над R. Тогда индуцированное отображение на тензорных произведениях TensorProduct.map g g' : N ⊗ N' → P ⊗ P' сюръективно.

LaTeX

$$\\operatorname{Surjective}( \\mathrm{TensorProduct.map}(g,g') )$$

Lean4

theorem map_surjective : Function.Surjective (TensorProduct.map g g') :=
  by
  rw [← lTensor_comp_rTensor, coe_comp]
  exact Function.Surjective.comp (lTensor_surjective _ hg') (rTensor_surjective _ hg)

Похожие утверждения