map_id — Mathlib

English

The tensor-product construction respects identity maps in each factor: applying the induced map with the identity on M1 and M2 yields the identity map on the tensor product.

Русский

Тензорная конструкция сохраняет тождественные отображения в каждой факторе: отображение, индуцируемое единицами на M1 и M2, равно тождественному отображению на тензорном произведении.

LaTeX

$$$ hf.map\; hf\; (id_{M_1})\; (id_{M_2}) = id$$$

Lean4

@[simp]
theorem map_id : hf.map hf (LinearMap.id : M₁ →ₗ[R] M₁) (LinearMap.id : M₂ →ₗ[R] M₂) = LinearMap.id :=
  LinearMap.ext <| fun x ↦ hf.inductionOn x (by simp) (by simp) (fun _ _ h₁ h₂ ↦ by simp [h₁, h₂])

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