Identify the inverse-flow cofactor with the forward flow matrix in the row-Jacobian convention.

theorem AVenhance.Infra.Section5.gradMatrix_comp {F G : Homogenization.Vec 2 → Homogenization.Vec 2} {x : Homogenization.Vec 2} (hF : DifferentiableAt ℝ F (G x)) (hG : DifferentiableAt ℝ G x) : gradMatrix (fun (y : Homogenization.Vec 2) => F (G y)) x = gradMatrix G x * gradMatrix F (G x)

theorem AVenhance.Infra.Section5.FlowPiolaIdentity.gradMatrix_id (x : Homogenization.Vec 2) : gradMatrix (fun (y : Homogenization.Vec 2) => y) x = 1

theorem AVenhance.Infra.Section5.FlowPiolaIdentity.adjugate_eq_rightInverse_of_mul_eq_one (A B : Matrix (Fin 2) (Fin 2) ℝ) (hAB : A * B = 1) (hdet : A.det = 1) : A.adjugate = B

theorem AVenhance.Infra.Section5.xFlowInv_rowCofactor_eq_flowGrad_transpose {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (l : ℤ) (t : ℝ) (x : Homogenization.Vec 2) (hdiv : ∀ (r : ℝ) (y : Homogenization.Vec 2), Flow.spatialDivergence (streamVel (Φ (m - 1))) r y = 0) : rowCofactor (gradMatrix (I.xFlowInv hΦ m l t) x) = (I.flowGrad hΦ m l t x).transpose

For an inverse flow, the row cofactor is the transpose of the forward row-Jacobian evaluated at the inverse image. This is the source Piola coefficient after correcting its row/column convention.