English
Congruence relations for the basis-dependent inversion show that the resulting maps agree when bases are altered by an equivalent pair.
Русский
Соответствия по базисам для инверсии согласованы: совпадение отображений при замене базисов на эквивалентную пару.
LaTeX
$$$$ (b,c) \\mapsto dualDistribInvOfBasis b c \\quad \\text{is compatible with} \\quad (b',c') \\mapsto dualDistribInvOfBasis b' c'. $$$$
Lean4
/-- A linear equivalence between `Dual M ⊗ Dual N` and `Dual (M ⊗ N)` given bases for `M` and `N`.
It sends `f ⊗ g` to the composition of `TensorProduct.map f g` with the natural
isomorphism `R ⊗ R ≃ R`.
-/
@[simps!]
noncomputable def dualDistribEquivOfBasis (b : Basis ι R M) (c : Basis κ R N) :
Dual R M ⊗[R] Dual R N ≃ₗ[R] Dual R (M ⊗[R] N) :=
by
refine LinearEquiv.ofLinear (dualDistrib R M N) (dualDistribInvOfBasis b c) ?_ ?_
· exact dualDistrib_dualDistribInvOfBasis_left_inverse _ _
· exact dualDistrib_dualDistribInvOfBasis_right_inverse _ _
