mapBaseChange_tmul — Mathlib

English

The base change map distributes over tensor product with tmul: mapBaseChange(x ⊗ y) equals x times map on y.

Русский

Отображение базового изменения распределяется по тензорному произведению: mapBaseChange(x ⊗ y) равно x умноженному на отображение на y.

LaTeX

$$$\\mathrm{mapBaseChange}\\, (x \\otimes y) = x \\cdot \\mathrm{map}\\, (R,R,A,B)\\, y$$$

Lean4

@[simp]
theorem mapBaseChange_tmul (x : B) (y : Ω[A⁄R]) :
    KaehlerDifferential.mapBaseChange R A B (x ⊗ₜ y) = x • KaehlerDifferential.map R R A B y :=
  by
  conv_lhs => rw [← mul_one x, ← smul_eq_mul, ← TensorProduct.smul_tmul', LinearMap.map_smul]
  congr 1
  exact IsBaseChange.lift_eq _ _ _

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