tensorμ_eq_tensorTensorTensorComm

English

The tensor μ equals the canonical isomorphism given by tensorTensorTensorComm; i.e., tensorμ A B C D = ofHom (TensorProduct.tensorTensorTensorComm R A B C D).toLinearMap.

Русский

Тензорная μ совпадает с каноническим изоморофизмом через tensorTensorTensorComm.

LaTeX

$$$\\text{tensor}\\mu\\; A\\; B\\; C\\; D\\; = \\text{ofHom}\\big(\\text{TensorProduct.tensorTensorTensorComm}\\; R\\; A\\; B\\; C\\; D\\big).toLinearMap$$$

Lean4

theorem tensorμ_eq_tensorTensorTensorComm {A B C D : ModuleCat R} :
    tensorμ A B C D = ofHom (TensorProduct.tensorTensorTensorComm R A B C D).toLinearMap :=
  ModuleCat.hom_ext <|
    TensorProduct.ext <|
      TensorProduct.ext <| LinearMap.ext₂ fun _ _ => TensorProduct.ext <| LinearMap.ext₂ fun _ _ => rfl

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