includeLeft_surjective — Mathlib

English

If the algebra map R → T is surjective, the left-inclusion map A →ₐ[S] A ⊗_R T is surjective; i.e., every element of A ⊗_R T can be obtained as includeLeft(a) for some a ∈ A.

Русский

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

LaTeX

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

Lean4

theorem includeLeft_surjective (S A : Type*) [CommSemiring S] [Semiring A] [Algebra S A] [Algebra R A]
    [SMulCommClass R S A] (h : Function.Surjective (algebraMap R T)) :
    Function.Surjective (includeLeft : A →ₐ[S] A ⊗[R] T) :=
  TensorProduct.flip_mk_surjective _ h

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