includeRight — Mathlib

English

There is an R-algebra homomorphism includeRight: B →_R A ⊗_R B sending b to 1 ⊗ b.

Русский

Существуют R-алгебр-гомоморфизм includeRight: B →_R A ⊗_R B, отправляющий b на 1 ⊗ b.

LaTeX

$$$i_R: B \to_R A \otimes_R B\quad\text{defined by}\quad i_R(b)=1\otimes b.$$$

Lean4

/-- The algebra morphism `B →ₐ[R] A ⊗[R] B` sending `b` to `1 ⊗ₜ b`. -/
def includeRight : B →ₐ[R] A ⊗[R] B where
  toFun b := 1 ⊗ₜ b
  map_zero' := by simp
  map_add' := by simp [tmul_add]
  map_one' := rfl
  map_mul' := by simp
  commutes' r := by simp only [algebraMap_apply']

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