tensorTensorTensorComm_comp_map — Mathlib

English

A symmetric version of map map associativity; the equality holds with the symmetrized associator.

Русский

Симметричная версия ассоциативности отображений; равенство сохраняется при симметризации ассоциатора.

LaTeX

$$$(TensorProduct.map (TensorProduct.map f g) h)^{\\mathrm{symm}} \\circ (TensorProduct.assoc R M N P)^{ -1} = (TensorProduct.assoc R Q S T)^{ -1} \\circ TensorProduct.map (TensorProduct.map f h) (TensorProduct.map g j)$$$

Lean4

theorem tensorTensorTensorComm_comp_map {V W : Type*} [AddCommMonoid V] [AddCommMonoid W] [Module R V] [Module R W]
    (f : M →ₗ[R] S) (g : N →ₗ[R] T) (h : P →ₗ[R] V) (j : Q →ₗ[R] W) :
    tensorTensorTensorComm R S T V W ∘ₗ map (map f g) (map h j) =
      map (map f h) (map g j) ∘ₗ tensorTensorTensorComm R M N P Q :=
  ext_fourfold' fun _ _ _ _ => rfl

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