includeLeftRingHom — Mathlib

English

There is a ring homomorphism A → A ⊗_R B sending a to a ⊗ 1, and it is compatible with the algebra structure.

Русский

Существует кольцевое морфизм A → A ⊗_R B, отображающий a на a ⊗ 1 и совместимый с алгебраической структурой.

LaTeX

$$$ includeLeftRingHom : A \to^+ A \otimes_R B, \quad a \mapsto a \otimes 1 $$$

Lean4

/-- The ring morphism `A →+* A ⊗[R] B` sending `a` to `a ⊗ₜ 1`. -/
@[simps]
def includeLeftRingHom : A →+* A ⊗[R] B where
  toFun a := a ⊗ₜ 1
  map_zero' := by simp
  map_add' := by simp [add_tmul]
  map_one' := rfl
  map_mul' := by simp

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