English
There is a linear equivalence between uncurry and lcurry related by lift, giving a dual description of bilinear maps.
Русский
Существует линейная эквивалентность между uncurry и lcurry, связанная через lift, дающая двойственное описание билинейных отображений.
LaTeX
$$$\text{equiv} : (M \to_A N \to_R P) \simeq_B M \otimes_R N \to_A P$$$
Lean4
/-- Heterobasic version of `TensorProduct.uncurry`:
Linearly constructing a linear map `M ⊗[R] N →[A] P` given a bilinear map `M →[A] N →[R] P`
with the property that its composition with the canonical bilinear map `M →[A] N →[R] M ⊗[R] N` is
the given bilinear map `M →[A] N →[R] P`. -/
@[simps]
def uncurry : (M →ₗ[A] N →ₗ[R] P) →ₗ[B] M ⊗[R] N →ₗ[A] P
where
toFun := lift
map_add' _ _ := ext fun x y => by simp only [lift_tmul, add_apply]
map_smul' _ _ := ext fun x y => by simp only [lift_tmul, smul_apply, RingHom.id_apply]
