includeLeft — Mathlib

English

There is an S-algebra homomorphism includeLeft: A →_S A ⊗_R B which sends a to a ⊗ 1.

Русский

Существуют S-алгебр-гомоморфизм includeLeft: A →_S A ⊗_R B, который отправляет a на a ⊗ 1.

LaTeX

$$$i_L: A \to_S A \otimes_R B\quad\text{defined by}\quad i_L(a)=a\otimes 1.$$

Lean4

/-- The `R`-algebra morphism `A →ₐ[R] A ⊗[R] B` sending `a` to `a ⊗ₜ 1`. -/
def includeLeft [SMulCommClass R S A] : A →ₐ[S] A ⊗[R] B :=
  { includeLeftRingHom with commutes' := by simp }

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