English
There is a canonical linear equivalence between uncurry and lcurry induced by lift, forming a bridge between bilinear maps and tensor maps.
Русский
Существует каноническая линейная эквалентность между uncurry и lcurry, индуцируемая lift, связывающая билинейные отображения и отображения на тензоре.
LaTeX
$$$\text{equiv} = \text{LinearEquiv.ofLinear}(\text{uncurry},\text{lcurry},\ldots)$$$
Lean4
/-- Heterobasic version of `TensorProduct.lift.equiv`:
A linear equivalence 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`. -/
def equiv : (M →ₗ[A] N →ₗ[R] P) ≃ₗ[B] M ⊗[R] N →ₗ[A] P :=
LinearEquiv.ofLinear (uncurry R A B M N P) (lcurry R A B M N P)
(LinearMap.ext fun _ => ext fun x y => lift_tmul _ x y)
(LinearMap.ext fun f => LinearMap.ext fun x => LinearMap.ext fun y => lift_tmul f x y)
