Coarse-graining support: Support.CoarseGraining.AdjointSymmetry.SigmaAdjoint #
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
Adjoint symmetry -- sigma / kappa / deterministic coarse block adjoint #
sigmaStarCoarse / sigmaStarInvKappaCoarse / kappaCoarse / sigmaCoarse / deterministicCoarseBlockMatrix / sigmaStarInvCoarse / sigmaStarInvKappaCoarse equalities under adjointCoeffField, from isSigma / isKappa / isCoarseBlockMatrix hypotheses and their witness-data variants.
theorem
HCPolySupport.sigmaStarCoarse_adjointCoeffField_eq_of_isSigmaStarData
{d : ℕ}
{U : Set (Vec d)}
{a : CoeffField d}
{sigmaStar : Mat d}
(hS : IsSigmaStarCoarse U a sigmaStar)
(hSAdj : IsSigmaStarCoarse U (adjointCoeffField a) sigmaStar)
(hdet : IsUnit (Matrix.det sigmaStar))
:
Note-facing transpose compatibility for \sigma_*(U; a) from primal and
adjoint \sigma_* witness data.
theorem
HCPolySupport.sigmaStarInvKappaCoarse_adjointCoeffField_eq_neg_of_isKappaCoarse
{d : ℕ}
{U : Set (Vec d)}
{a : CoeffField d}
{sigmaStar kappa : Mat d}
(hK : IsKappaCoarse U a sigmaStar kappa)
(hKAdj : IsKappaCoarse U (adjointCoeffField a) sigmaStar (-kappa))
:
theorem
HCPolySupport.sigmaStarInvKappaCoarse_adjointCoeffField_eq_neg_of_isKappaData
{d : ℕ}
{U : Set (Vec d)}
{a : CoeffField d}
{sigmaStar kappa : Mat d}
(hK : IsKappaCoarse U a sigmaStar kappa)
(hKAdj : IsKappaCoarse U (adjointCoeffField a) sigmaStar (-kappa))
:
Note-facing transpose compatibility for \sigma_*^{-1}(U; a)\kappa(U; a)
from primal and adjoint \kappa witness data.
theorem
HCPolySupport.kappaCoarse_adjointCoeffField_eq_neg_of_isKappaCoarse
{d : ℕ}
{U : Set (Vec d)}
{a : CoeffField d}
{sigmaStar kappa : Mat d}
(hS : IsSigmaStarCoarse U a sigmaStar)
(hK : IsKappaCoarse U a sigmaStar kappa)
(hSAdj : IsSigmaStarCoarse U (adjointCoeffField a) sigmaStar)
(hKAdj : IsKappaCoarse U (adjointCoeffField a) sigmaStar (-kappa))
(hdet : IsUnit (Matrix.det sigmaStar))
:
theorem
HCPolySupport.kappaCoarse_adjointCoeffField_eq_neg_of_isKappaData
{d : ℕ}
{U : Set (Vec d)}
{a : CoeffField d}
{sigmaStar kappa : Mat d}
(hS : IsSigmaStarCoarse U a sigmaStar)
(hK : IsKappaCoarse U a sigmaStar kappa)
(hSAdj : IsSigmaStarCoarse U (adjointCoeffField a) sigmaStar)
(hKAdj : IsKappaCoarse U (adjointCoeffField a) sigmaStar (-kappa))
(hdet : IsUnit (Matrix.det sigmaStar))
:
Note-facing transpose compatibility for \kappa(U; a) from primal and
adjoint \sigma_*/\kappa witness data.
theorem
HCPolySupport.sigmaCoarse_adjointCoeffField_eq_of_isSigmaCoarse
{d : ℕ}
{U : Set (Vec d)}
{a : CoeffField d}
{sigma sigmaStar kappa : Mat d}
(hS : IsSigmaStarCoarse U a sigmaStar)
(hK : IsKappaCoarse U a sigmaStar kappa)
(hSigma : IsSigmaCoarse U a sigma sigmaStar kappa)
(hSAdj : IsSigmaStarCoarse U (adjointCoeffField a) sigmaStar)
(hKAdj : IsKappaCoarse U (adjointCoeffField a) sigmaStar (-kappa))
(hSigmaAdj : IsSigmaCoarse U (adjointCoeffField a) sigma sigmaStar (-kappa))
(hdet : IsUnit (Matrix.det sigmaStar))
:
theorem
HCPolySupport.sigmaCoarse_adjointCoeffField_eq_of_isSigmaData
{d : ℕ}
{U : Set (Vec d)}
{a : CoeffField d}
{sigma sigmaStar kappa : Mat d}
(hS : IsSigmaStarCoarse U a sigmaStar)
(hK : IsKappaCoarse U a sigmaStar kappa)
(hSigma : IsSigmaCoarse U a sigma sigmaStar kappa)
(hSAdj : IsSigmaStarCoarse U (adjointCoeffField a) sigmaStar)
(hKAdj : IsKappaCoarse U (adjointCoeffField a) sigmaStar (-kappa))
(hSigmaAdj : IsSigmaCoarse U (adjointCoeffField a) sigma sigmaStar (-kappa))
(hdet : IsUnit (Matrix.det sigmaStar))
:
Note-facing transpose compatibility for \sigma(U; a) from primal and
adjoint deterministic coarse-data witnesses.
theorem
HCPolySupport.deterministicCoarseBlockMatrix_adjointCoeffField_eq_blockMatFlipFlux_of_isSigmaCoarse
{d : ℕ}
{U : Set (Vec d)}
{a : CoeffField d}
{sigma sigmaStar kappa : Mat d}
(hS : IsSigmaStarCoarse U a sigmaStar)
(hK : IsKappaCoarse U a sigmaStar kappa)
(hSigma : IsSigmaCoarse U a sigma sigmaStar kappa)
(hSAdj : IsSigmaStarCoarse U (adjointCoeffField a) sigmaStar)
(hKAdj : IsKappaCoarse U (adjointCoeffField a) sigmaStar (-kappa))
(hSigmaAdj : IsSigmaCoarse U (adjointCoeffField a) sigma sigmaStar (-kappa))
(hdet : IsUnit (Matrix.det sigmaStar))
:
theorem
HCPolySupport.deterministicCoarseBlockMatrix_adjointCoeffField_eq_blockMatFlipFlux_of_isSigmaData
{d : ℕ}
{U : Set (Vec d)}
{a : CoeffField d}
{sigma sigmaStar kappa : Mat d}
(hS : IsSigmaStarCoarse U a sigmaStar)
(hK : IsKappaCoarse U a sigmaStar kappa)
(hSigma : IsSigmaCoarse U a sigma sigmaStar kappa)
(hSAdj : IsSigmaStarCoarse U (adjointCoeffField a) sigmaStar)
(hKAdj : IsKappaCoarse U (adjointCoeffField a) sigmaStar (-kappa))
(hSigmaAdj : IsSigmaCoarse U (adjointCoeffField a) sigma sigmaStar (-kappa))
(hdet : IsUnit (Matrix.det sigmaStar))
:
Note-facing transpose compatibility for the deterministic coarse block matrix built from primal and adjoint scalar coarse-data witnesses.
theorem
HCPolySupport.deterministicCoarseBlockMatrix_upperLeft_adjointCoeffField_eq_of_isSigmaCoarse
{d : ℕ}
{U : Set (Vec d)}
{a : CoeffField d}
{sigma sigmaStar kappa : Mat d}
(hS : IsSigmaStarCoarse U a sigmaStar)
(hK : IsKappaCoarse U a sigmaStar kappa)
(hSigma : IsSigmaCoarse U a sigma sigmaStar kappa)
(hSAdj : IsSigmaStarCoarse U (adjointCoeffField a) sigmaStar)
(hKAdj : IsKappaCoarse U (adjointCoeffField a) sigmaStar (-kappa))
(hSigmaAdj : IsSigmaCoarse U (adjointCoeffField a) sigma sigmaStar (-kappa))
(hdet : IsUnit (Matrix.det sigmaStar))
:
theorem
HCPolySupport.deterministicCoarseBlockMatrix_upperLeft_adjointCoeffField_eq_of_isSigmaData
{d : ℕ}
{U : Set (Vec d)}
{a : CoeffField d}
{sigma sigmaStar kappa : Mat d}
(hS : IsSigmaStarCoarse U a sigmaStar)
(hK : IsKappaCoarse U a sigmaStar kappa)
(hSigma : IsSigmaCoarse U a sigma sigmaStar kappa)
(hSAdj : IsSigmaStarCoarse U (adjointCoeffField a) sigmaStar)
(hKAdj : IsKappaCoarse U (adjointCoeffField a) sigmaStar (-kappa))
(hSigmaAdj : IsSigmaCoarse U (adjointCoeffField a) sigma sigmaStar (-kappa))
(hdet : IsUnit (Matrix.det sigmaStar))
:
Note-facing transpose compatibility for the upper-left block of the deterministic coarse block matrix from primal and adjoint scalar coarse-data witnesses.
theorem
HCPolySupport.deterministicCoarseBlockMatrix_upperRight_adjointCoeffField_eq_neg_of_isSigmaCoarse
{d : ℕ}
{U : Set (Vec d)}
{a : CoeffField d}
{sigma sigmaStar kappa : Mat d}
(hS : IsSigmaStarCoarse U a sigmaStar)
(hK : IsKappaCoarse U a sigmaStar kappa)
(hSigma : IsSigmaCoarse U a sigma sigmaStar kappa)
(hSAdj : IsSigmaStarCoarse U (adjointCoeffField a) sigmaStar)
(hKAdj : IsKappaCoarse U (adjointCoeffField a) sigmaStar (-kappa))
(hSigmaAdj : IsSigmaCoarse U (adjointCoeffField a) sigma sigmaStar (-kappa))
(hdet : IsUnit (Matrix.det sigmaStar))
:
theorem
HCPolySupport.deterministicCoarseBlockMatrix_upperRight_adjointCoeffField_eq_neg_of_isSigmaData
{d : ℕ}
{U : Set (Vec d)}
{a : CoeffField d}
{sigma sigmaStar kappa : Mat d}
(hS : IsSigmaStarCoarse U a sigmaStar)
(hK : IsKappaCoarse U a sigmaStar kappa)
(hSigma : IsSigmaCoarse U a sigma sigmaStar kappa)
(hSAdj : IsSigmaStarCoarse U (adjointCoeffField a) sigmaStar)
(hKAdj : IsKappaCoarse U (adjointCoeffField a) sigmaStar (-kappa))
(hSigmaAdj : IsSigmaCoarse U (adjointCoeffField a) sigma sigmaStar (-kappa))
(hdet : IsUnit (Matrix.det sigmaStar))
:
Note-facing transpose compatibility for the upper-right block of the deterministic coarse block matrix from primal and adjoint scalar coarse-data witnesses.
theorem
HCPolySupport.deterministicCoarseBlockMatrix_lowerLeft_adjointCoeffField_eq_neg_of_isSigmaCoarse
{d : ℕ}
{U : Set (Vec d)}
{a : CoeffField d}
{sigma sigmaStar kappa : Mat d}
(hS : IsSigmaStarCoarse U a sigmaStar)
(hK : IsKappaCoarse U a sigmaStar kappa)
(hSigma : IsSigmaCoarse U a sigma sigmaStar kappa)
(hSAdj : IsSigmaStarCoarse U (adjointCoeffField a) sigmaStar)
(hKAdj : IsKappaCoarse U (adjointCoeffField a) sigmaStar (-kappa))
(hSigmaAdj : IsSigmaCoarse U (adjointCoeffField a) sigma sigmaStar (-kappa))
(hdet : IsUnit (Matrix.det sigmaStar))
:
theorem
HCPolySupport.deterministicCoarseBlockMatrix_lowerLeft_adjointCoeffField_eq_neg_of_isSigmaData
{d : ℕ}
{U : Set (Vec d)}
{a : CoeffField d}
{sigma sigmaStar kappa : Mat d}
(hS : IsSigmaStarCoarse U a sigmaStar)
(hK : IsKappaCoarse U a sigmaStar kappa)
(hSigma : IsSigmaCoarse U a sigma sigmaStar kappa)
(hSAdj : IsSigmaStarCoarse U (adjointCoeffField a) sigmaStar)
(hKAdj : IsKappaCoarse U (adjointCoeffField a) sigmaStar (-kappa))
(hSigmaAdj : IsSigmaCoarse U (adjointCoeffField a) sigma sigmaStar (-kappa))
(hdet : IsUnit (Matrix.det sigmaStar))
:
Note-facing transpose compatibility for the lower-left block of the deterministic coarse block matrix from primal and adjoint scalar coarse-data witnesses.
theorem
HCPolySupport.deterministicCoarseBlockMatrix_lowerRight_adjointCoeffField_eq_of_isSigmaCoarse
{d : ℕ}
{U : Set (Vec d)}
{a : CoeffField d}
{sigma sigmaStar kappa : Mat d}
(hS : IsSigmaStarCoarse U a sigmaStar)
(hK : IsKappaCoarse U a sigmaStar kappa)
(hSigma : IsSigmaCoarse U a sigma sigmaStar kappa)
(hSAdj : IsSigmaStarCoarse U (adjointCoeffField a) sigmaStar)
(hKAdj : IsKappaCoarse U (adjointCoeffField a) sigmaStar (-kappa))
(hSigmaAdj : IsSigmaCoarse U (adjointCoeffField a) sigma sigmaStar (-kappa))
(hdet : IsUnit (Matrix.det sigmaStar))
:
theorem
HCPolySupport.deterministicCoarseBlockMatrix_lowerRight_adjointCoeffField_eq_of_isSigmaData
{d : ℕ}
{U : Set (Vec d)}
{a : CoeffField d}
{sigma sigmaStar kappa : Mat d}
(hS : IsSigmaStarCoarse U a sigmaStar)
(hK : IsKappaCoarse U a sigmaStar kappa)
(hSigma : IsSigmaCoarse U a sigma sigmaStar kappa)
(hSAdj : IsSigmaStarCoarse U (adjointCoeffField a) sigmaStar)
(hKAdj : IsKappaCoarse U (adjointCoeffField a) sigmaStar (-kappa))
(hSigmaAdj : IsSigmaCoarse U (adjointCoeffField a) sigma sigmaStar (-kappa))
(hdet : IsUnit (Matrix.det sigmaStar))
:
Note-facing transpose compatibility for the lower-right block of the deterministic coarse block matrix from primal and adjoint scalar coarse-data witnesses.
theorem
HCPolySupport.deterministicCoarseBlockMatrix_adjointCoeffField_eq_blockMatFlipFlux_of_isCoarseBlockMatrix
{d : ℕ}
{U : Set (Vec d)}
{a : CoeffField d}
(hA : IsCoarseBlockMatrix U a (deterministicCoarseBlockMatrix U a))
(hAadj : IsCoarseBlockMatrix U (adjointCoeffField a) (deterministicCoarseBlockMatrix U (adjointCoeffField a)))
:
theorem
HCPolySupport.deterministicCoarseBlockMatrix_adjointCoeffField_eq_blockMatFlipFlux
{d : ℕ}
{U : Set (Vec d)}
{a : CoeffField d}
(hA : IsCoarseBlockMatrix U a (deterministicCoarseBlockMatrix U a))
(hAadj : IsCoarseBlockMatrix U (adjointCoeffField a) (deterministicCoarseBlockMatrix U (adjointCoeffField a)))
:
Note-facing transpose compatibility for the deterministic coarse block matrix built from the canonical coarse data.
theorem
HCPolySupport.deterministicCoarseBlockMatrix_upperLeft_adjointCoeffField_of_isCoarseBlockMatrix
{d : ℕ}
{U : Set (Vec d)}
{a : CoeffField d}
(hA : IsCoarseBlockMatrix U a (deterministicCoarseBlockMatrix U a))
(hAadj : IsCoarseBlockMatrix U (adjointCoeffField a) (deterministicCoarseBlockMatrix U (adjointCoeffField a)))
:
theorem
HCPolySupport.deterministicCoarseBlockMatrix_upperLeft_adjointCoeffField_eq
{d : ℕ}
{U : Set (Vec d)}
{a : CoeffField d}
(hA : IsCoarseBlockMatrix U a (deterministicCoarseBlockMatrix U a))
(hAadj : IsCoarseBlockMatrix U (adjointCoeffField a) (deterministicCoarseBlockMatrix U (adjointCoeffField a)))
:
Note-facing transpose compatibility for the upper-left block of the deterministic coarse block matrix.
theorem
HCPolySupport.deterministicCoarseBlockMatrix_upperRight_adjointCoeffField_of_isCoarseBlockMatrix
{d : ℕ}
{U : Set (Vec d)}
{a : CoeffField d}
(hA : IsCoarseBlockMatrix U a (deterministicCoarseBlockMatrix U a))
(hAadj : IsCoarseBlockMatrix U (adjointCoeffField a) (deterministicCoarseBlockMatrix U (adjointCoeffField a)))
:
theorem
HCPolySupport.deterministicCoarseBlockMatrix_upperRight_adjointCoeffField_eq_neg
{d : ℕ}
{U : Set (Vec d)}
{a : CoeffField d}
(hA : IsCoarseBlockMatrix U a (deterministicCoarseBlockMatrix U a))
(hAadj : IsCoarseBlockMatrix U (adjointCoeffField a) (deterministicCoarseBlockMatrix U (adjointCoeffField a)))
:
Note-facing transpose compatibility for the upper-right block of the deterministic coarse block matrix.
theorem
HCPolySupport.deterministicCoarseBlockMatrix_lowerLeft_adjointCoeffField_of_isCoarseBlockMatrix
{d : ℕ}
{U : Set (Vec d)}
{a : CoeffField d}
(hA : IsCoarseBlockMatrix U a (deterministicCoarseBlockMatrix U a))
(hAadj : IsCoarseBlockMatrix U (adjointCoeffField a) (deterministicCoarseBlockMatrix U (adjointCoeffField a)))
:
theorem
HCPolySupport.deterministicCoarseBlockMatrix_lowerLeft_adjointCoeffField_eq_neg
{d : ℕ}
{U : Set (Vec d)}
{a : CoeffField d}
(hA : IsCoarseBlockMatrix U a (deterministicCoarseBlockMatrix U a))
(hAadj : IsCoarseBlockMatrix U (adjointCoeffField a) (deterministicCoarseBlockMatrix U (adjointCoeffField a)))
:
Note-facing transpose compatibility for the lower-left block of the deterministic coarse block matrix.
theorem
HCPolySupport.deterministicCoarseBlockMatrix_lowerRight_adjointCoeffField_of_isCoarseBlockMatrix
{d : ℕ}
{U : Set (Vec d)}
{a : CoeffField d}
(hA : IsCoarseBlockMatrix U a (deterministicCoarseBlockMatrix U a))
(hAadj : IsCoarseBlockMatrix U (adjointCoeffField a) (deterministicCoarseBlockMatrix U (adjointCoeffField a)))
:
theorem
HCPolySupport.deterministicCoarseBlockMatrix_lowerRight_adjointCoeffField_eq
{d : ℕ}
{U : Set (Vec d)}
{a : CoeffField d}
(hA : IsCoarseBlockMatrix U a (deterministicCoarseBlockMatrix U a))
(hAadj : IsCoarseBlockMatrix U (adjointCoeffField a) (deterministicCoarseBlockMatrix U (adjointCoeffField a)))
:
Note-facing transpose compatibility for the lower-right block of the deterministic coarse block matrix.
theorem
HCPolySupport.sigmaStarInvCoarse_adjointCoeffField_eq_of_isCoarseBlockMatrix
{d : ℕ}
{U : Set (Vec d)}
{a : CoeffField d}
(hA : IsCoarseBlockMatrix U a (deterministicCoarseBlockMatrix U a))
(hAadj : IsCoarseBlockMatrix U (adjointCoeffField a) (deterministicCoarseBlockMatrix U (adjointCoeffField a)))
:
theorem
HCPolySupport.sigmaStarInvCoarse_adjointCoeffField_eq
{d : ℕ}
{U : Set (Vec d)}
{a : CoeffField d}
{sigmaStar : Mat d}
(hS : IsSigmaStarCoarse U a sigmaStar)
(hSAdj : IsSigmaStarCoarse U (adjointCoeffField a) sigmaStar)
:
Note-facing transpose compatibility for \sigma_*^{-1}(U; a).
theorem
HCPolySupport.sigmaStarInvKappaCoarse_adjointCoeffField_eq_neg_of_isCoarseBlockMatrix
{d : ℕ}
{U : Set (Vec d)}
{a : CoeffField d}
(hA : IsCoarseBlockMatrix U a (deterministicCoarseBlockMatrix U a))
(hAadj : IsCoarseBlockMatrix U (adjointCoeffField a) (deterministicCoarseBlockMatrix U (adjointCoeffField a)))
:
theorem
HCPolySupport.sigmaStarInvKappaCoarse_adjointCoeffField_eq_neg
{d : ℕ}
{U : Set (Vec d)}
{a : CoeffField d}
(hA : IsCoarseBlockMatrix U a (deterministicCoarseBlockMatrix U a))
(hAadj : IsCoarseBlockMatrix U (adjointCoeffField a) (deterministicCoarseBlockMatrix U (adjointCoeffField a)))
:
Note-facing transpose compatibility for \sigma_*^{-1}(U; a)\kappa(U; a).
theorem
HCPolySupport.sigmaStarInvKappaCoarse_eq_zero_of_adjointCoeffField_eq_of_isCoarseBlockMatrix
{d : ℕ}
{U : Set (Vec d)}
{a : CoeffField d}
(hA : IsCoarseBlockMatrix U a (deterministicCoarseBlockMatrix U a))
(hAdj : adjointCoeffField a = a)
:
If the coefficient field is self-adjoint, then the canonical
\sigma_*^{-1}(U; a)\kappa(U; a) vanishes once the deterministic coarse block
matrix is identified as coarse.
theorem
HCPolySupport.sigmaStarCoarse_adjointCoeffField_eq_of_isCoarseBlockMatrix
{d : ℕ}
{U : Set (Vec d)}
{a : CoeffField d}
(hA : IsCoarseBlockMatrix U a (deterministicCoarseBlockMatrix U a))
(hAadj : IsCoarseBlockMatrix U (adjointCoeffField a) (deterministicCoarseBlockMatrix U (adjointCoeffField a)))
:
theorem
HCPolySupport.sigmaStarCoarse_adjointCoeffField_eq
{d : ℕ}
{U : Set (Vec d)}
{a : CoeffField d}
{sigmaStar : Mat d}
(hS : IsSigmaStarCoarse U a sigmaStar)
(hSAdj : IsSigmaStarCoarse U (adjointCoeffField a) sigmaStar)
(hdet : IsUnit (Matrix.det sigmaStar))
:
Note-facing transpose compatibility for \sigma_*(U; a).
theorem
HCPolySupport.kappaCoarse_adjointCoeffField_eq_neg_of_isCoarseBlockMatrix
{d : ℕ}
{U : Set (Vec d)}
{a : CoeffField d}
(hA : IsCoarseBlockMatrix U a (deterministicCoarseBlockMatrix U a))
(hAadj : IsCoarseBlockMatrix U (adjointCoeffField a) (deterministicCoarseBlockMatrix U (adjointCoeffField a)))
:
theorem
HCPolySupport.kappaCoarse_adjointCoeffField_eq_neg
{d : ℕ}
{U : Set (Vec d)}
{a : CoeffField d}
{sigmaStar kappa : Mat d}
(hS : IsSigmaStarCoarse U a sigmaStar)
(hK : IsKappaCoarse U a sigmaStar kappa)
(hSAdj : IsSigmaStarCoarse U (adjointCoeffField a) sigmaStar)
(hKAdj : IsKappaCoarse U (adjointCoeffField a) sigmaStar (-kappa))
(hdet : IsUnit (Matrix.det sigmaStar))
:
Note-facing transpose compatibility for \kappa(U; a).
theorem
HCPolySupport.kappaCoarse_eq_zero_of_adjointCoeffField_eq_of_isCoarseBlockMatrix
{d : ℕ}
{U : Set (Vec d)}
{a : CoeffField d}
(hA : IsCoarseBlockMatrix U a (deterministicCoarseBlockMatrix U a))
(hAdj : adjointCoeffField a = a)
:
If the coefficient field is self-adjoint, then the canonical
\kappa(U; a) vanishes once the deterministic coarse block matrix is
identified as coarse.
theorem
HCPolySupport.sigmaCoarse_adjointCoeffField_eq_of_isCoarseBlockMatrix
{d : ℕ}
{U : Set (Vec d)}
{a : CoeffField d}
(hA : IsCoarseBlockMatrix U a (deterministicCoarseBlockMatrix U a))
(hAadj : IsCoarseBlockMatrix U (adjointCoeffField a) (deterministicCoarseBlockMatrix U (adjointCoeffField a)))
:
theorem
HCPolySupport.sigmaCoarse_adjointCoeffField_eq
{d : ℕ}
{U : Set (Vec d)}
{a : CoeffField d}
{sigma sigmaStar kappa : Mat d}
(hS : IsSigmaStarCoarse U a sigmaStar)
(hK : IsKappaCoarse U a sigmaStar kappa)
(hSigma : IsSigmaCoarse U a sigma sigmaStar kappa)
(hSAdj : IsSigmaStarCoarse U (adjointCoeffField a) sigmaStar)
(hKAdj : IsKappaCoarse U (adjointCoeffField a) sigmaStar (-kappa))
(hSigmaAdj : IsSigmaCoarse U (adjointCoeffField a) sigma sigmaStar (-kappa))
(hdet : IsUnit (Matrix.det sigmaStar))
:
Note-facing transpose compatibility for \sigma(U; a).