The finite-dimensional algebra in the curl Piola identity. Antisymmetrizing Fᵀ A F transforms by the actual adjugate of F. In particular, a determinant-one change of variables transforms curl by F⁻¹.

@[reducible, inline]

abbrev EulerPacketPiola.Mat3 : Type

Mat3: an abbreviation for Matrix (Fin 3) (Fin 3) ℝ.

Equations

• EulerPacketPiola.Mat3 = Matrix (Fin 3) (Fin 3) ℝ

def EulerPacketPiola.matrixAntisym (A : Mat3) : Fin 3 → ℝ

Matrix antisym, given by ![A 2 1 - A 1 2, A 0 2 - A 2 0, A 1 0 - A 0 1].

Equations

• EulerPacketPiola.matrixAntisym A = ![A 2 1 - A 1 2, A 0 2 - A 2 0, A 1 0 - A 0 1]

theorem EulerPacketPiola.matrixAntisym_congruence (F A : Mat3) : matrixAntisym (Matrix.transpose F * A * F) = (Matrix.adjugate F).mulVec (matrixAntisym A)

The adjugate transformation law is a polynomial identity, without invertibility assumptions.

noncomputable def EulerPacketPiola.operatorMatrix (A : EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) : Mat3

Operator matrix, defined pointwise by (A (EuclideanSpace.single j 1)) i.

Equations

• EulerPacketPiola.operatorMatrix A i j = (A (EuclideanSpace.single j 1)).ofLp i

theorem EulerPacketPiola.operatorMatrix_apply (A : EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) (x : EulerSmoothLimit.Space) (i : Fin 3) : (A x).ofLp i = Matrix.mulVec (operatorMatrix A) x.ofLp i

theorem EulerPacketPiola.operatorMatrix_comp (A B : EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) : operatorMatrix (A ∘SL B) = operatorMatrix A * operatorMatrix B

theorem EulerPacketPiola.operatorMatrix_id : operatorMatrix (ContinuousLinearMap.id ℝ EulerSmoothLimit.Space) = 1

theorem EulerPacketPiola.operatorMatrix_adjoint (A : EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) : operatorMatrix (ContinuousLinearMap.adjoint A) = Matrix.transpose (operatorMatrix A)

theorem EulerPacketPiola.matrixAntisym_operator (A : EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) : matrixAntisym (operatorMatrix A) = (EulerMeanBoundary.curlMatrix A).ofLp

theorem EulerPacketPiola.operatorMatrix_inverse (F : EulerSmoothLimit.Space ≃L[ℝ] EulerSmoothLimit.Space) : operatorMatrix ↑F * operatorMatrix ↑F.symm = 1

theorem EulerPacketPiola.adjugate_operatorMatrix (F : EulerSmoothLimit.Space ≃L[ℝ] EulerSmoothLimit.Space) (hdet : Matrix.det (operatorMatrix ↑F) = 1) : Matrix.adjugate (operatorMatrix ↑F) = operatorMatrix ↑F.symm

theorem EulerPacketPiola.curlMatrix_congruence (F : EulerSmoothLimit.Space ≃L[ℝ] EulerSmoothLimit.Space) (hdet : Matrix.det (operatorMatrix ↑F) = 1) (A : EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) : EulerMeanBoundary.curlMatrix (ContinuousLinearMap.adjoint ↑F ∘SL A ∘SL ↑F) = F.symm (EulerMeanBoundary.curlMatrix A)

The actual Euclidean curl tensor transforms by the inverse under a unit Jacobian.

theorem EulerPacketPiola.curlMatrix_piola (F : EulerSmoothLimit.Space ≃L[ℝ] EulerSmoothLimit.Space) (hdet : Matrix.det (operatorMatrix ↑F) = 1) (B : EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) : EulerMeanBoundary.curlMatrix (ContinuousLinearMap.adjoint ↑F ∘SL B) = F.symm (EulerMeanBoundary.curlMatrix (B ∘SL ↑F.symm))

Algebraic Piola curl identity for a genuine first derivative in label coordinates.