English
For any R-algebra T, the Jacobian of the base-changed presentation equals the tensor product of 1 with the original Jacobian: jacobian(baseChange_T(P)) = 1 ⊗ P.jacobian.
Русский
Для любого T, алгебры над R, якобиан базового изменения презентации равен тензорному произведению единицы с исходным якобианом: jacobian(baseChange_T(P)) = 1 ⊗ P.jacobian.
LaTeX
$$$\\operatorname{jacobian}(\\mathrm{baseChange}_T(P)) = 1 \\otimes_R \\operatorname{jacobian}(P).$$$
Lean4
@[simp]
theorem baseChange_jacobian [Finite σ] : (P.baseChange T).jacobian = 1 ⊗ₜ P.jacobian := by
classical
cases nonempty_fintype σ
simp_rw [jacobian_eq_jacobiMatrix_det]
have h : (baseChange T P).jacobiMatrix = (MvPolynomial.map (algebraMap R T)).mapMatrix P.jacobiMatrix :=
by
ext i j : 1
simp only [baseChange, jacobiMatrix_apply, Presentation.baseChange_relation, RingHom.mapMatrix_apply,
Matrix.map_apply, Presentation.baseChange_toGenerators, MvPolynomial.pderiv_map]
rw [h, ← RingHom.map_det, Generators.algebraMap_apply, aeval_map_algebraMap, P.algebraMap_apply]
apply aeval_one_tmul
