map_eq — Mathlib

English

Composition of maps respects the IsTensorProduct construction: hf.map hp (i1 ∘ j1) (i2 ∘ j2) equals (hg.map hp i1 i2) ∘ (hf.map hg j1 j2).

Русский

Сопоставление отображений сохраняет конструкцию IsTensorProduct: hf.map hp (i1 ∘ j1) (i2 ∘ j2) = (hg.map hp i1 i2) ∘ (hf.map hg j1 j2).

LaTeX

$$hf.map hp (i₁ ∘ₗ j₁) (i₂ ∘ₗ j₂) = hg.map hp i₁ i₂ ∘ₗ hf.map hg j₁ j₂$$

Lean4

@[simp]
theorem map_eq (hf : IsTensorProduct f) (hg : IsTensorProduct g) (i₁ : M₁ →ₗ[R] N₁) (i₂ : M₂ →ₗ[R] N₂) (x₁ : M₁)
    (x₂ : M₂) : hf.map hg i₁ i₂ (f x₁ x₂) = g (i₁ x₁) (i₂ x₂) := by simp [map]

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