English
The composition of dualDistrib with dualDistribInvOfBasis is the identity on the tensor of duals; i.e., dualDistrib ∘ dualDistribInvOfBasis b c = id.
Русский
Композиция dualDistrib с dualDistribInvOfBasis даёт тождественный отображение: dualDistrib ∘ dualDistribInvOfBasis b c = id.
LaTeX
$$$$ dualDistrib \\circ dualDistribInvOfBasis b c = \\mathrm{id}. $$$$
Lean4
theorem dualDistrib_dualDistribInvOfBasis_left_inverse (b : Basis ι R M) (c : Basis κ R N) :
comp (dualDistrib R M N) (dualDistribInvOfBasis b c) = LinearMap.id :=
by
apply (b.tensorProduct c).dualBasis.ext
rintro ⟨i, j⟩
apply (b.tensorProduct c).ext
rintro ⟨i', j'⟩
simp only [dualDistrib, Basis.coe_dualBasis, coe_comp, Function.comp_apply, dualDistribInvOfBasis_apply,
Basis.coord_apply, Basis.tensorProduct_repr_tmul_apply, Basis.repr_self, _root_.map_sum, map_smul,
homTensorHomMap_apply, compRight_apply, Basis.tensorProduct_apply, coeFn_sum, Finset.sum_apply, smul_apply,
LinearEquiv.coe_coe, map_tmul, lid_tmul, smul_eq_mul, id_coe, id_eq]
rw [Finset.sum_eq_single i, Finset.sum_eq_single j]
· simpa using mul_comm _ _
all_goals { intros; simp [*] at *
}
