English
The constructed S-linear section sec satisfies that its composition with a canonical lift equals the identity map on M.
Русский
Сконструированное секционное отображение sec удовлетворяет, что композиция с каноническим подъемом даёт тождественный отображения на M.
LaTeX
$$$(\\text{sec} \\;\\circ\\; \\text{lift}) = \\mathrm{id}_M$$$
Lean4
theorem comp_sec :
(TensorProduct.AlgebraTensorModule.lift ((lsmul S S M).toLinearMap.flip.restrictScalars R).flip).comp (sec R S M) =
LinearMap.id :=
by
ext x
simp only [sec, LinearMap.coe_comp, LinearMap.coe_mk, LinearMap.coe_toAddHom, Function.comp_apply,
LinearMap.flip_apply, TensorProduct.AlgebraTensorModule.mapBilinear_apply,
TensorProduct.AlgebraTensorModule.lift_apply, LinearMap.id_coe, id_eq]
trans (TensorProduct.lmul' R (elem R S)) • x
·
induction elem R S using TensorProduct.induction_on with
| zero => simp
| tmul r s => simp [mul_smul, smul_comm r s]
| add y z hy hz => simp [hy, hz, add_smul]
· rw [lmul_elem, one_smul]
