Documentation

TauCeti.LinearAlgebra.Matrix.Adjugate.FinTwo

Adjugation of two-by-two matrices #

The adjugate of a two-by-two matrix is linear over any commutative ring, including in characteristic two. It is the unique function reversing products for which every matrix plus its image is scalar; linearity is not needed for this characterization. These facts identify Clifford reversal with adjugation in the two-by-two matrix model of Spin(3).

For complex matrices, composing adjugation with conjugate transpose gives a real-algebra endomorphism. This packages the multiplicative map used by real low-rank matrix models.

source
@[simp]
theorem Matrix.adjugate_fin_two_eq_trace_smul_one_sub {K : Type u_1} [CommRing K] (A : Matrix (Fin 2) (Fin 2) K) :
A.adjugate = A.trace • 1 - A

The adjugate of a two-by-two matrix is its trace times the identity minus itself.

source
noncomputable def Matrix.adjugateFinTwoLinearMap {K : Type u_1} [CommRing K] :
Matrix (Fin 2) (Fin 2) K →ₗ[K] Matrix (Fin 2) (Fin 2) K

The adjugate as a linear map on 2 × 2 matrices over a commutative ring.

Equations
Instances For
    source
    @[simp]
    theorem Matrix.adjugateFinTwoLinearMap_apply {K : Type u_1} [CommRing K] (A : Matrix (Fin 2) (Fin 2) K) :
    adjugateFinTwoLinearMap A = A.adjugate

    Applying adjugateFinTwoLinearMap computes the ordinary matrix adjugate.

    source
    noncomputable def Matrix.starAdjugateFinTwoAlgHom :
    Matrix (Fin 2) (Fin 2) ℂ →ₐ[ℝ] Matrix (Fin 2) (Fin 2) ℂ

    Adjugation followed by conjugate transpose, as a real-algebra endomorphism of complex 2 × 2 matrices.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem Matrix.starAdjugateFinTwoAlgHom_apply (A : Matrix (Fin 2) (Fin 2) ℂ) :
      starAdjugateFinTwoAlgHom A = star A.adjugate

      Applying starAdjugateFinTwoAlgHom computes the conjugate transpose of the adjugate.

      source
      theorem Matrix.eq_adjugate_of_antimultiplicative_of_exists_add_eq_smul_one {K : Type u_1} [CommRing K] (f : Matrix (Fin 2) (Fin 2) K → Matrix (Fin 2) (Fin 2) K) (hmul : ∀ (A B : Matrix (Fin 2) (Fin 2) K), f (A * B) = f B * f A) (hscalar : ∀ (A : Matrix (Fin 2) (Fin 2) K), ∃ (r : K), A + f A = r • 1) (A : Matrix (Fin 2) (Fin 2) K) :
      f A = A.adjugate

      An anti-multiplicative function for which every matrix plus its image is scalar is adjugation. No additivity or homogeneity assumption is needed.