map_map_assoc_symm — Mathlib

English

The following equality holds on arbitrary x: map f (map g h) (TensorProduct.assoc x) = TensorProduct.assoc (map (map f g) h x).

Русский

Следующее равенство выполняется для любого x: map f (map g h) (assoc x) = assoc (map (map f g) h x).

LaTeX

$$$\\text{map }f\\; (\\text{map }g\\; h)\\; (\\alpha_{M,N,P}(x)) = \\alpha_{Q,S,T}\\; (\\text{map }(\\text{map }f g)\\; h)(x)$$$

Lean4

theorem map_map_assoc_symm (f : M →ₗ[R] Q) (g : N →ₗ[R] S) (h : P →ₗ[R] T) (x : M ⊗[R] (N ⊗[R] P)) :
    map (map f g) h ((TensorProduct.assoc R M N P).symm x) = (TensorProduct.assoc R Q S T).symm (map f (map g h) x) :=
  DFunLike.congr_fun (map_map_comp_assoc_symm_eq _ _ _) _

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