jacobiMatrix_reindex — Mathlib

English

If P is a pre-submersive presentation and e, f are equivalences, then the jacobiMatrix of P.reindex e f equals the reindexed and renamed jacobiMatrix of P.

Русский

Если P — предsub-мерсивное представление, и заданы эквивалентности e и f, то jacobiMatrix(P.reindex e f) равен перераспределённой и переименованной jacobiMatrix(P).

LaTeX

$$$\\operatorname{jacobiMatrix}(P^{e,f}) = (\\operatorname{jacobiMatrix}(P))^{f^{-1},\,f^{-1}} \\mapsto \\mathrm{rename}(e^{-1}).$$$

Lean4

theorem jacobiMatrix_reindex {ι' σ' : Type*} (e : ι' ≃ ι) (f : σ' ≃ σ) [Fintype σ'] [DecidableEq σ'] [Fintype σ]
    [DecidableEq σ] :
    (P.reindex e f).jacobiMatrix = (P.jacobiMatrix.reindex f.symm f.symm).map (MvPolynomial.rename e.symm) :=
  by
  ext i j : 1
  simp [jacobiMatrix_apply, MvPolynomial.pderiv_rename e.symm.injective, reindex, Presentation.reindex]

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