map_map_assoc — Mathlib

English

A symmetric version: applying (f ⊗ g) ⊗ h to a differently bracketed input coincides with first applying f ⊗ (g ⊗ h) and then rebracketing via the associator.

Русский

Симметричная версия: применение (f ⊗ g) ⊗ h к по-разному сгруппированному входу совпадает с сначала применением f ⊗ (g ⊗ h) и затем перераблокировкой через ассоциатор.

LaTeX

$$$\\big((f\\otimes g)\\otimes h\\big)\\circ\\alpha_{M,N,P}^{-1} = \\alpha_{Q,S,T}^{-1} \\circ (f\\otimes (g\\otimes h))$$$

Lean4

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

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