map_comp — Mathlib

English

A compatibility identity for map with commutativity of the tensor product.

Русский

Совпадение отображений с перестановкой факторов в тензорном произведении.

LaTeX

$$$\\mathrm{map}\\ (f_2) (g_2) \\circ_\\ell \\mathrm{TensorProduct.comm}\\ N M = \\mathrm{TensorProduct.comm}\\ Q P \\circ_\\ell \\mathrm{map}\\ g f$$$

Lean4

theorem map_comp (f₂ : M₂ →ₛₗ[σ₂₃] M₃) (g₂ : N₂ →ₛₗ[σ₂₃] N₃) (f₁ : M →ₛₗ[σ₁₂] M₂) (g₁ : N →ₛₗ[σ₁₂] N₂) :
    map (f₂ ∘ₛₗ f₁) (g₂ ∘ₛₗ g₁) = (map f₂ g₂) ∘ₛₗ (map f₁ g₁) :=
  ext' fun _ _ => rfl

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