ofBijectiveAlgebraMap_jacobian — Mathlib

English

For bijective algebra maps, the Jacobian of the associated pre-submersive presentation is 1.

Русский

Для биективной алгебраической карты якобиан связанного пред-subмersion равен 1.

LaTeX

$$(ofBijectiveAlgebraMap(h)).jacobian = 1$$

Lean4

@[simp]
theorem ofBijectiveAlgebraMap_jacobian (h : Function.Bijective (algebraMap R S)) :
    (ofBijectiveAlgebraMap h).jacobian = 1 := by
  classical
  have : (algebraMap (ofBijectiveAlgebraMap h).Ring S).mapMatrix (ofBijectiveAlgebraMap h).jacobiMatrix = 1 :=
    by
    ext (i j : PEmpty)
    contradiction
  rw [jacobian_eq_jacobiMatrix_det, RingHom.map_det, this, Matrix.det_one]

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