English
If P is submersive, there is a linear equivalence aevalDifferentialEquiv between the σ→S and itself, induced by P.
Русский
Если P является субмассовым, существует линейное эквивалентное отображение aevalDifferentialEquiv между функциями σ→S и самим собой, индукированное P.
LaTeX
$$$\\text{aevalDifferentialEquiv}(P) : (σ \\to S) \\simeq_{S} (σ \\to S)$$$
Lean4
/-- If `P` is submersive, `PreSubmersivePresentation.aevalDifferential` is an isomorphism. -/
noncomputable def aevalDifferentialEquiv (P : SubmersivePresentation R S ι σ) : (σ → S) ≃ₗ[S] (σ → S) :=
haveI : Fintype σ := Fintype.ofFinite σ
have : IsUnit (LinearMap.toMatrix (Pi.basisFun S σ) (Pi.basisFun S σ) P.aevalDifferential).det :=
by
convert P.jacobian_isUnit
rw [LinearMap.toMatrix_eq_toMatrix', jacobian_eq_jacobiMatrix_det,
aevalDifferential_toMatrix'_eq_mapMatrix_jacobiMatrix, P.algebraMap_eq]
simp [RingHom.map_det]
LinearEquiv.ofIsUnitDet this
