map_tmul — Mathlib

English

The map on cotangent spaces acts on simple tensors by sending x ⊗ D y to (algebraMap x) ⊗ D (f(y)).

Русский

Отображение на котант Spaces действует на простые тензоры: x ⊗ D y ↦ (algebraMap x) ⊗ D (f(y)).

LaTeX

$$$\\mathrm{CotangentSpace}.map(f)(x \\otimes \\mathrm{D} y) = (\\mathrm{algebraMap}\\; S \\; S'\\; x) \\otimes \\mathrm{D}(f(y))$$$

Lean4

@[simp]
theorem map_tmul (f : Hom P P') (x y) :
    CotangentSpace.map f (x ⊗ₜ .D _ _ y) = (algebraMap _ _ x) ⊗ₜ .D _ _ (f.toAlgHom y) :=
  by
  simp only [CotangentSpace.map, AlgHom.toRingHom_eq_coe, LinearMap.liftBaseChange_tmul, LinearMap.coe_comp,
    LinearMap.coe_restrictScalars, Function.comp_apply, map_D, mk_apply]
  rw [smul_tmul', ← Algebra.algebraMap_eq_smul_one]
  rfl

Похожие утверждения