includeRight_surjective — Mathlib

English

If the algebra map R → S is surjective, the right-inclusion map T →ₐ[R] S ⊗_R T is surjective; i.e., every element of S ⊗_R T is in the image of includeRight.

Русский

Пусть отображение R → S сюръективно; тогда отображение includeRight : T →ₐ[R] S ⊗_R T является сюръективным; каждый элемент S ⊗_R T лежит в образе includeRight.

LaTeX

$$$\\text{If } \\operatorname{algebraMap}_R^S \\text{ is surjective, then } includeRight: T \\toₐ[R] S \\otimes_R T \\text{ is surjective.}$$$

Lean4

theorem includeRight_surjective (h : Function.Surjective (algebraMap R S)) :
    Function.Surjective (includeRight : T →ₐ[R] S ⊗[R] T) :=
  TensorProduct.mk_surjective _ _ _ h

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