English
The heterogeneous differential 𝒅ₕ is defined via hfdifferential with a trivial witness h := rfl, giving a linear map between PointDerivation I x and PointDerivation I' (f x).
Русский
Гетерогенная дифференциал 𝒅ₕ определяется через hfdifferential с очевидным свидетельством h := rfl, образуя линейное отображение между точечными деривациями.
LaTeX
$$$$ \mathrm{fdifferential}(f, x) : \ PointDerivation I x \to_{\mathbb{K}} \ PointDerivation I' (f x). $$$$
Lean4
/-- The heterogeneous differential as a linear map, denoted as `𝒅ₕ` within the `Manifold` namespace.
Instead of taking a function as an argument, this
differential takes `h : f x = y`. It is particularly handy for situations where the points
at which it has to be evaluated are equal but not definitionally equal. -/
def hfdifferential {f : C^∞⟮I, M; I', M'⟯} {x : M} {y : M'} (h : f x = y) :
PointDerivation I x →ₗ[𝕜] PointDerivation I' y
where
toFun
v :=
Derivation.mk'
{ toFun := fun g => v (g.comp f)
map_add' := fun g g' => by rw [ContMDiffMap.add_comp, Derivation.map_add]
map_smul' := fun k g => by dsimp; rw [ContMDiffMap.smul_comp, Derivation.map_smul, smul_eq_mul] } fun g g' =>
by
dsimp
rw [ContMDiffMap.mul_comp, Derivation.leibniz, PointedContMDiffMap.smul_def, ContMDiffMap.comp_apply,
PointedContMDiffMap.smul_def, ContMDiffMap.comp_apply, h]
norm_cast
map_smul' _ _ := rfl
map_add' _ _ := rfl
