map — Mathlib

English

There is a heterobasic version of TensorProduct.map which constructs a map M ⊗R N →A P ⊗R Q from maps M →A P and N →R Q.

Русский

Существует гетеробазовая версия TensorProduct.map, которая строит отображение M ⊗R N →A P ⊗R Q из отображений M →A P и N →R Q.

LaTeX

$$$\text{map} : (M \to_A P) (N \to_R Q) \to M \otimes_R N \to_A P \otimes_R Q$$$

Lean4

/-- Heterobasic version of `TensorProduct.map` -/
def map (f : M →ₗ[A] P) (g : N →ₗ[R] Q) : M ⊗[R] N →ₗ[A] P ⊗[R] Q :=
  lift <|
    { toFun := fun h => h ∘ₗ g, map_add' := fun h₁ h₂ => LinearMap.add_comp g h₂ h₁,
        map_smul' := fun c h => LinearMap.smul_comp c h g } ∘ₗ
      mk R A P Q ∘ₗ f

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