Documentation

TauCeti.LinearAlgebra.Matrix.Minor

Minors on a pair of rows and a pair of columns #

A 2 × 2 minor of a matrix is the determinant of the submatrix on an ordered pair of rows and an ordered pair of columns. Matrix.pairMinor names it, so that a family of such minors can be indexed by pairs rather than by Fin 2-valued reindexing functions, and Matrix.pairMinor_mul is the Cauchy--Binet expansion of a minor of a product, summing over the increasing pairs of the middle index type.

The rows and the columns are indexed independently: a 2 × 2 minor makes sense for a rectangular matrix, and the square case specializes.

The middle index type of Cauchy--Binet is linearly ordered, which is how the unordered pairs it sums over are named without choosing representatives: each is written as the increasing one. The sign of a minor depends on the order of its two indices, so some such choice is needed for the statement to be sign-correct.

Main definitions #

Main results #

source
def Matrix.pairMinor {m : Type u_1} {n : Type u_2} {R : Type u} [CommRing R] (g : Matrix m n R) (p : m × m) (q : n × n) :
R

The 2 × 2 minor of a matrix on the ordered row pair p and the ordered column pair q.

Equations
Instances For
    source
    theorem Matrix.pairMinor_eq {m : Type u_1} {n : Type u_2} {R : Type u} [CommRing R] (g : Matrix m n R) (p : m × m) (q : n × n) :
    g.pairMinor p q = g p.1 q.1 * g p.2 q.2 - g p.1 q.2 * g p.2 q.1

    The 2 × 2 minor written out.

    source
    @[simp]
    theorem Matrix.pairMinor_self_left {m : Type u_1} {n : Type u_2} {R : Type u} [CommRing R] (g : Matrix m n R) (a : m) (q : n × n) :
    g.pairMinor (a, a) q = 0

    A minor with a repeated row index vanishes.

    source
    @[simp]
    theorem Matrix.pairMinor_self_right {m : Type u_1} {n : Type u_2} {R : Type u} [CommRing R] (g : Matrix m n R) (p : m × m) (b : n) :
    g.pairMinor p (b, b) = 0

    A minor with a repeated column index vanishes.

    source
    theorem Matrix.pairMinor_swap_left {m : Type u_1} {n : Type u_2} {R : Type u} [CommRing R] (g : Matrix m n R) (a b : m) (q : n × n) :
    g.pairMinor (b, a) q = -g.pairMinor (a, b) q

    Swapping the two row indices negates the minor.

    source
    theorem Matrix.pairMinor_swap_right {m : Type u_1} {n : Type u_2} {R : Type u} [CommRing R] (g : Matrix m n R) (p : m × m) (a b : n) :
    g.pairMinor p (b, a) = -g.pairMinor p (a, b)

    Swapping the two column indices negates the minor.

    source
    @[simp]
    theorem Matrix.pairMinor_transpose {m : Type u_1} {n : Type u_2} {R : Type u} [CommRing R] (g : Matrix m n R) (p : m × m) (q : n × n) :
    g.transpose.pairMinor q p = g.pairMinor p q

    A minor of the transpose is the minor of the matrix with the row and column pairs exchanged.

    source
    @[simp]
    theorem Matrix.pairMinor_map {m : Type u_1} {n : Type u_2} {R : Type u} [CommRing R] {S : Type u_3} [CommRing S] (f : R →+* S) (g : Matrix m n R) (p : m × m) (q : n × n) :
    (g.map ⇑f).pairMinor p q = f (g.pairMinor p q)

    A ring morphism carries a minor to the minor of the mapped matrix.

    source
    theorem Matrix.pairMinor_mul {m : Type u_1} {n : Type u_2} {R : Type u} [CommRing R] {l : Type u_3} [Fintype l] [LinearOrder l] (g : Matrix m l R) (h : Matrix l n R) (p : m × m) (q : n × n) :
    (g * h).pairMinor p q = ∑ ij : l × l with ij.1 < ij.2, g.pairMinor p ij * h.pairMinor ij q

    Cauchy--Binet for 2 × 2 minors. A minor of a product is the sum, over the increasing pairs of the middle index type, of the products of the corresponding minors of the two factors.

    source
    theorem Matrix.pairMinor_mul_fin_four {m : Type u_1} {n : Type u_2} {R : Type u} [CommRing R] (g : Matrix m (Fin 4) R) (h : Matrix (Fin 4) n R) (p : m × m) (q : n × n) :
    (g * h).pairMinor p q = g.pairMinor p (0, 1) * h.pairMinor (0, 1) q + g.pairMinor p (0, 2) * h.pairMinor (0, 2) q + g.pairMinor p (0, 3) * h.pairMinor (0, 3) q + g.pairMinor p (1, 2) * h.pairMinor (1, 2) q + g.pairMinor p (1, 3) * h.pairMinor (1, 3) q + g.pairMinor p (2, 3) * h.pairMinor (2, 3) q

    Cauchy--Binet across a four-element middle index type, with the six increasing pairs written out. This is the shape the rank-two symplectic calculation consumes.