English
The left inverse property of the Kaehler tensor equiv: applying base-change followed by lifting Kaehler differential and restricting scalars yields the identity on the module.
Русский
Левая инверсия каэлеровской тензорной эквивалентности: последовательности базового изменения и последующего подъёма дают тождественный отображение.
LaTeX
$$$\\Big( (\\mathrm{derivationTensorProduct}(R,S,A,B).liftKaehlerDifferential).restrictScalars S \\Big) \\circ \\Big( (\\mathrm{map}(R,S,A,B).restrictScalars R).liftBaseChange S \\Big) = \\mathrm{id}$$$
Lean4
theorem tensorKaehlerEquiv_left_inv [Algebra.IsPushout R S A B] :
((derivationTensorProduct R S A B).liftKaehlerDifferential.restrictScalars S).comp
(((map R S A B).restrictScalars R).liftBaseChange S) =
LinearMap.id :=
by
refine LinearMap.restrictScalars_injective R ?_
apply TensorProduct.ext'
intro x y
obtain ⟨y, rfl⟩ := tensorProductTo_surjective _ _ y
induction y
· simp only [map_zero, TensorProduct.tmul_zero]
· simp only [LinearMap.restrictScalars_comp, Derivation.tensorProductTo_tmul, LinearMap.coe_comp,
LinearMap.coe_restrictScalars, Function.comp_apply, LinearMap.liftBaseChange_tmul, map_smul, map_D,
LinearMap.map_smul_of_tower, Derivation.liftKaehlerDifferential_comp_D, LinearMap.id_coe, id_eq,
derivationTensorProduct_algebraMap]
rw [smul_comm, TensorProduct.smul_tmul', smul_eq_mul, mul_one]
rfl
· simp only [map_add, TensorProduct.tmul_add, *]
