map — Mathlib

English

The map hf.map hg i1 i2 sends f x1 x2 to g (i1 x1) (i2 x2).

Русский

Гомоморфизм hf.map hg i1 i2 отправляет f x1 x2 в g (i1 x1) (i2 x2).

LaTeX

$$hf.map hg i1 i2 (f x1 x2) = g (i1 x1) (i2 x2)$$

Lean4

/-- The tensor product of a pair of linear maps between modules. -/
noncomputable def map (hf : IsTensorProduct f) (hg : IsTensorProduct g) (i₁ : M₁ →ₗ[R] N₁) (i₂ : M₂ →ₗ[R] N₂) :
    M →ₗ[R] N :=
  hg.equiv.toLinearMap.comp ((TensorProduct.map i₁ i₂).comp hf.equiv.symm.toLinearMap)

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