Documentation

TauCeti.LinearAlgebra.Matrix.BlockSucc

Placing a square matrix in the upper-left block of the next size #

A square matrix of size n becomes one of size n + 1 by putting it in the upper-left block and filling the last row and column with those of the identity matrix. This file builds that map, Matrix.blockSucc, and shows it is multiplicative, unital and injective, and that it leaves the determinant unchanged while adding 1 to the trace.

The construction is written with Fin.snoc rather than as Matrix.fromBlocks M 0 0 1 reindexed along finSumFinEquiv, because Fin (n + 1) is the index type the general linear groups and their standard representations are stated over: a Fin n ⊕ Fin 1 presentation would have to be reindexed away again at once.

TauCeti/LinearAlgebra/Matrix/GeneralLinearGroup/BlockSucc.lean deduces from this the block inclusion TauCeti.glBlockSucc : GL (Fin n) k →* GL (Fin (n + 1)) k, the embedding that fixes the last basis vector.

Main definitions #

Main results #

source
def Matrix.blockSucc {k : Type u} {n : ℕ} [Semiring k] (M : Matrix (Fin n) (Fin n) k) :
Matrix (Fin (n + 1)) (Fin (n + 1)) k

A square matrix of size n, placed in the upper-left block of a square matrix of size n + 1 whose last row and column are those of the identity matrix.

Instances For
    source
    @[simp]
    theorem Matrix.blockSucc_castSucc_castSucc {k : Type u} {n : ℕ} [Semiring k] (M : Matrix (Fin n) (Fin n) k) (i j : Fin n) :
    M.blockSucc i.castSucc j.castSucc = M i j
    source
    @[simp]
    theorem Matrix.blockSucc_castSucc_last {k : Type u} {n : ℕ} [Semiring k] (M : Matrix (Fin n) (Fin n) k) (i : Fin n) :
    M.blockSucc i.castSucc (Fin.last n) = 0
    source
    @[simp]
    theorem Matrix.blockSucc_last_castSucc {k : Type u} {n : ℕ} [Semiring k] (M : Matrix (Fin n) (Fin n) k) (j : Fin n) :
    M.blockSucc (Fin.last n) j.castSucc = 0
    source
    @[simp]
    theorem Matrix.blockSucc_last_last {k : Type u} {n : ℕ} [Semiring k] (M : Matrix (Fin n) (Fin n) k) :
    M.blockSucc (Fin.last n) (Fin.last n) = 1
    source
    @[simp]
    theorem Matrix.submatrix_blockSucc_castSucc {k : Type u} {n : ℕ} [Semiring k] (M : Matrix (Fin n) (Fin n) k) :
    M.blockSucc.submatrix Fin.castSucc Fin.castSucc = M

    The upper-left block of the extension of a matrix is the matrix itself.

    source
    @[simp]
    theorem Matrix.blockSucc_one {k : Type u} {n : ℕ} [Semiring k] :
    blockSucc 1 = 1
    source
    @[simp]
    theorem Matrix.map_blockSucc {k : Type u} {n : ℕ} [Semiring k] {l : Type u_1} [Semiring l] {F : Type u_2} [FunLike F k l] [RingHomClass F k l] (f : F) (M : Matrix (Fin n) (Fin n) k) :
    M.blockSucc.map ⇑f = (M.map ⇑f).blockSucc

    Extending a matrix commutes with applying a ring homomorphism to its entries, since the new entries 0 and 1 are preserved.

    source
    @[simp]
    theorem Matrix.transpose_blockSucc {k : Type u} {n : ℕ} [Semiring k] (M : Matrix (Fin n) (Fin n) k) :
    M.blockSucc.transpose = M.transpose.blockSucc

    Extending a matrix commutes with transposing it: the last row and the last column of Matrix.blockSucc M are those of the identity matrix, so transposing exchanges them with each other and transposes the upper-left block. This is what carries orthogonality of a matrix to orthogonality of its extension.

    source
    @[simp]
    theorem Matrix.conjTranspose_blockSucc {k : Type u} {n : ℕ} [Semiring k] [StarRing k] (M : Matrix (Fin n) (Fin n) k) :
    M.blockSucc.conjTranspose = M.conjTranspose.blockSucc

    Extending a matrix commutes with taking its conjugate transpose, the last row and column being those of the identity matrix. This carries the contravariance of the conjugate transpose along the block inclusion.

    source
    theorem Matrix.blockSucc_mul {k : Type u} {n : ℕ} [Semiring k] (M N : Matrix (Fin n) (Fin n) k) :
    (M * N).blockSucc = M.blockSucc * N.blockSucc

    Extending a product is the product of the extensions: the last row and column of Matrix.blockSucc M are those of the identity matrix, so the extra index contributes only its own diagonal entry. This is what makes Matrix.blockSuccMonoidHom and hence the block inclusion TauCeti.glBlockSucc multiplicative.

    source
    def Matrix.blockSuccMonoidHom (k : Type u) (n : ℕ) [Semiring k] :
    Matrix (Fin n) (Fin n) k →* Matrix (Fin (n + 1)) (Fin (n + 1)) k

    The upper-left block embedding of matrices, bundled as a monoid homomorphism. It is unital because the last row and column of Matrix.blockSucc M are those of the identity matrix, and for the same reason it is not additive.

    Instances For
      source
      @[simp]
      theorem Matrix.blockSuccMonoidHom_apply {k : Type u} {n : ℕ} [Semiring k] (M : Matrix (Fin n) (Fin n) k) :
      (blockSuccMonoidHom k n) M = M.blockSucc
      source
      theorem Matrix.blockSucc_injective {k : Type u} {n : ℕ} [Semiring k] :
      Function.Injective blockSucc

      Extending a matrix loses no information: Matrix.blockSucc is injective, because the upper-left block of Matrix.blockSucc M is M. Use it to transfer an equation between extended matrices back to the original size; TauCeti.glBlockSucc_injective is the group-level form.

      source
      @[simp]
      theorem Matrix.blockSucc_mulVec {k : Type u} {n : ℕ} [Semiring k] (M : Matrix (Fin n) (Fin n) k) (v : Fin (n + 1) → k) :
      M.blockSucc.mulVec v = Fin.snoc (M.mulVec (Fin.init v)) (v (Fin.last n))

      The extended matrix acts by M on the first n coordinates and fixes the last one.

      source
      @[simp]
      theorem Matrix.trace_blockSucc {k : Type u} {n : ℕ} [Semiring k] (M : Matrix (Fin n) (Fin n) k) :
      M.blockSucc.trace = M.trace + 1

      Extending a matrix adds 1 to its trace: the new diagonal entry is the last diagonal entry of the identity matrix.

      source
      @[simp]
      theorem Matrix.det_blockSucc {k : Type u} {n : ℕ} [CommRing k] (M : Matrix (Fin n) (Fin n) k) :
      M.blockSucc.det = M.det

      Extending a matrix leaves its determinant unchanged, so it takes matrices of determinant 1 to matrices of determinant 1.