English
Given a submersive presentation P and equivalences e and f, there is a reindexed presentation with variables indexed by ι' and relations indexed by σ'.
Русский
Пусть дано подмассовое представление P и эквивалентности e и f; существует переиндексированное представление с переменными ι' и связями σ'.
LaTeX
$$$\\text{reindex}(P) : \\text{SubmersivePresentation } R S ι' σ'$, defined via the equivalences.$$
Lean4
/-- Given a submersive presentation `P` and equivalences `ι' ≃ ι` and
`σ' ≃ σ`, this is the induced submersive presentation with variables indexed
by `ι'` and relations indexed by `σ'` -/
@[simps toPreSubmersivePresentation]
noncomputable def reindex (P : SubmersivePresentation R S ι σ) {ι' σ' : Type*} [Finite σ'] (e : ι' ≃ ι) (f : σ' ≃ σ) :
SubmersivePresentation R S ι' σ'
where
__ := P.toPreSubmersivePresentation.reindex e f
jacobian_isUnit := by simp [P.jacobian_isUnit]
