algebraMap_tensorProduct — Mathlib

English

If a CodescendsAlong P Q holds and a suitable Q-condition at R holds, then P holds on the algebra-map into the tensor product.

Русский

Если выполняется CodescendsAlong P Q и существует условие Q на R, то P выполняется на алгебраическом отображении в тензорном произведении.

LaTeX

$$$\text{algebraMap_tensorProduct}(hPQ,h, H) : P( algebraMap R T)$.$$

Lean4

theorem algebraMap_tensorProduct (hPQ : CodescendsAlong P Q) (h : Q (algebraMap R S))
    (H : P (algebraMap S (S ⊗[R] T))) : P (algebraMap R T) :=
  let _ : Algebra T (S ⊗[R] T) := Algebra.TensorProduct.rightAlgebra
  hPQ R T S (S ⊗[R] T) h H

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