English
For a naive construction of a presentation corresponding to a quotient by a range, the jacobiMatrix entry equals the partial derivative of the corresponding variable: (naive a ha s hs).jacobiMatrix i j = (v j).pderiv (a i).
Русский
Для наивного конструктора презентации, соответствующей факторизации по диапазону, элемент jacobiMatrix равен частной производной: (naive a ha s hs).jacobiMatrix i j = (v j).pderiv (a i).
LaTeX
$$$\\operatorname{jacobiMatrix}(\\text{naive}(a,ha,s,hs))_{ij} = (v_j).\\,\\mathrm{pderiv}(a_i).$$$
Lean4
@[simp]
theorem jacobian_reindex (P : PreSubmersivePresentation R S ι σ) {ι' σ' : Type*} (e : ι' ≃ ι) (f : σ' ≃ σ) [Finite σ]
[Finite σ'] : (P.reindex e f).jacobian = P.jacobian := by
classical
cases nonempty_fintype σ
cases nonempty_fintype σ'
simp_rw [PreSubmersivePresentation.jacobian_eq_jacobiMatrix_det]
simp only [reindex_toPresentation, Presentation.reindex_toGenerators, jacobiMatrix_reindex, Matrix.reindex_apply,
Equiv.symm_symm, Generators.algebraMap_apply, Generators.reindex_val]
simp_rw [← MvPolynomial.aeval_rename, ← AlgHom.mapMatrix_apply, ← Matrix.det_submatrix_equiv_self f, AlgHom.map_det,
AlgHom.mapMatrix_apply, Matrix.map_map]
simp [← AlgHom.coe_comp, rename_comp_rename, rename_id]
