English
For a given derivation D, lifting Kaehler differential and applying toCotangent coincide with tensorProductTo of D.
Русский
Для данного выводного отображения D, соподнятие Kaehler differential и применение toCotangent совпадают с tensorProductTo D.
LaTeX
$$liftKaehlerDifferential_apply (D : Derivation R S M) (x) : D.liftKaehlerDifferential ((KaehlerDifferential.ideal R S).toCotangent x) = D.tensorProductTo x$$
Lean4
theorem liftKaehlerDifferential_comp (D : Derivation R S M) :
D.liftKaehlerDifferential.compDer (KaehlerDifferential.D R S) = D :=
by
ext a
dsimp [KaehlerDifferential.D_apply]
refine (D.liftKaehlerDifferential_apply _).trans ?_
rw [Subtype.coe_mk, map_sub, Derivation.tensorProductTo_tmul, Derivation.tensorProductTo_tmul, one_smul,
D.map_one_eq_zero, smul_zero, sub_zero]
