quotientTensorEquiv_symm_apply_mk_tmul

English

The inverse of the quotient-tensor isomorphism sends the class of x ⊗ y to the tensor x ⊗ y modulo the appropriate submodule, i.e., (quotientTensorEquiv N m)^{-1}([x ⊗ y]) = [x] ⊗ y.

Русский

Обратное отображение канонического тензорного изоморфизма отправляет класс x ⊗ y в x ⊗ ȳ, т.е. [x] ⊗ y.

LaTeX

$$$$(\text{quotientTensorEquiv } N\,m)^{-1}([x \otimes y]) = [x] \otimes y,$$$$

Lean4

@[simp]
theorem quotientTensorEquiv_symm_apply_mk_tmul (m : Submodule R M) (x : M) (y : N) :
    (quotientTensorEquiv N m).symm (Submodule.Quotient.mk (x ⊗ₜ y)) = Submodule.Quotient.mk x ⊗ₜ[R] y :=
  rfl

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