map_comp — Mathlib

English

Applying the heterobasic map with identity maps yields the identity map on the tensor product.

Русский

Применение гетеробазовой операции map к тождественным отображениям дает тождественное отображение на тензорном произведении.

LaTeX

$$$\text{map}(\mathrm{id}, \mathrm{id}) = \mathrm{id}$$$

Lean4

theorem map_comp (f₂ : P →ₗ[A] P') (f₁ : M →ₗ[A] P) (g₂ : Q →ₗ[R] Q') (g₁ : N →ₗ[R] Q) :
    map (f₂.comp f₁) (g₂.comp g₁) = (map f₂ g₂).comp (map f₁ g₁) :=
  ext fun _ _ => rfl

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