includeLeftRingHom_comp_algebraMap

English

The canonical R-algebra maps from R into A ⊗_R B via A and via B coincide: algebraMap_A(r) ⊗ 1 = 1 ⊗ algebraMap_B(r) for all r in R.

Русский

Канонические R-алгебр-образования R в A ⊗_R B через A и через B совпадают: algebraMap_A(r) ⊗ 1 = 1 ⊗ algebraMap_B(r) для всех r в R.

LaTeX

$$$\forall r\in R: (\text{algebraMap}_A r) \otimes 1 = 1 \otimes (\text{algebraMap}_B r).$$$

Lean4

theorem includeLeftRingHom_comp_algebraMap :
    (includeLeftRingHom.comp (algebraMap R A) : R →+* A ⊗[R] B) = includeRight.toRingHom.comp (algebraMap R B) :=
  by
  ext
  simp

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