comp_jacobian_eq_jacobian_smul_jacobian

English

Let P and Q be pre-submersive presentations of algebras over a base ring. The Jacobian of their composition equals the product of the Jacobians: jacobian(Q ∘ P) = jacobian(P) · jacobian(Q).

Русский

Пусть P и Q — предподмассовые презентации алгебр над базовым кольцом. Якобиан их композиции равен произведению якобианов: jacobian(Q ∘ P) = jacobian(P) · jacobian(Q).

LaTeX

$$$\\operatorname{jacobian}(Q \\circ P) = \\operatorname{jacobian}(P) \\cdot \\operatorname{jacobian}(Q).$$$

Lean4

/-- The Jacobian of the composition of presentations is the product of the Jacobians. -/
@[simp]
theorem comp_jacobian_eq_jacobian_smul_jacobian [Finite σ] [Finite σ'] :
    (Q.comp P).jacobian = P.jacobian • Q.jacobian := by
  classical
  cases nonempty_fintype σ'
  cases nonempty_fintype σ
  rw [jacobian_eq_jacobiMatrix_det, ← Matrix.fromBlocks_toBlocks ((Q.comp P).jacobiMatrix), jacobiMatrix_comp_₁₂]
  convert_to
    (aeval (Q.comp P).val) (Q.comp P).jacobiMatrix.toBlocks₁₁.det *
        (aeval (Q.comp P).val) (Q.comp P).jacobiMatrix.toBlocks₂₂.det =
      P.jacobian • Q.jacobian
  · simp only [Generators.algebraMap_apply, ← map_mul]
    congr
    convert
      Matrix.det_fromBlocks_zero₁₂ (Q.comp P).jacobiMatrix.toBlocks₁₁ (Q.comp P).jacobiMatrix.toBlocks₂₁
        (Q.comp P).jacobiMatrix.toBlocks₂₂
  · rw [jacobiMatrix_comp_₁₁_det, jacobiMatrix_comp_₂₂_det, mul_comm, Algebra.smul_def]

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