English
An inverse to dualDistrib with respect to bases b and c is given by the explicit finite sum over i,j of f(b_i ⊗ c_j) times b_i^* ⊗ c_j^*, i.e., the expression of the inverse map in terms of dual basis elements.
Русский
Обратное к dualDistrib выражается через базисы b и c как конечная сумма по i,j: f(b_i ⊗ c_j) × b_i^* ⊗ c_j^*, выражающее обратное отображение через двойственные базисы.
LaTeX
$$$$ dualDistribInvOfBasis b c f = \\sum_i \\sum_j f(b_i \\otimes c_j) \\; (b_i^* \\otimes c_j^*). $$$$
Lean4
/-- An inverse to `TensorProduct.dualDistrib` given bases.
-/
noncomputable def dualDistribInvOfBasis (b : Basis ι R M) (c : Basis κ R N) :
Dual R (M ⊗[R] N) →ₗ[R] Dual R M ⊗[R] Dual R N :=
∑ i,
∑ j,
(ringLmapEquivSelf R ℕ _).symm (b.dualBasis i ⊗ₜ c.dualBasis j) ∘ₗ applyₗ (c j) ∘ₗ applyₗ (b i) ∘ₗ lcurry R M N R
