Documentation

TauCeti.LinearAlgebra.Matrix.GeneralLinearGroup.BlockSucc

The upper-left block embedding of a general linear group in the next one #

An invertible matrix of size n becomes one of size n + 1 by placing it in the upper-left block and filling the last row and column with those of the identity matrix. That map on matrices is Matrix.blockSucc, from TauCeti/LinearAlgebra/Matrix/BlockSucc.lean; being multiplicative and unital, it induces the block inclusion TauCeti.glBlockSucc : GL (Fin n) k →* GL (Fin (n + 1)) k, the embedding that fixes the last basis vector, which this file builds.

This is the step of the chain GL 1 ⊂ GL 2 ⊂ ⋯ ⊂ GL n along which the general linear groups are restricted. TauCeti.glBlockSucc_diagGL records that it matches the corresponding chain of diagonal tori, and TauCeti.det_glBlockSucc that it carries special linear matrices to special linear matrices.

Main definitions #

Main results #

source
def TauCeti.glBlockSucc (k : Type u) (n : ℕ) [Semiring k] :
GL (Fin n) k →* GL (Fin (n + 1)) k

The block inclusion GL (Fin n) k →* GL (Fin (n + 1)) k: an invertible matrix is placed in the upper-left block and the last basis vector is fixed. This is the step of the chain GL 1 ⊂ GL 2 ⊂ ⋯ along which representations of the general linear groups are restricted.

Instances For
    source
    @[simp]
    theorem TauCeti.coe_glBlockSucc (k : Type u) (n : ℕ) [Semiring k] (g : GL (Fin n) k) :
    ↑((glBlockSucc k n) g) = (↑g).blockSucc
    source
    theorem TauCeti.glBlockSucc_star (k : Type u) (n : ℕ) [Semiring k] [StarRing k] (g : GL (Fin n) k) :
    (glBlockSucc k n) (star g) = star ((glBlockSucc k n) g)

    The block inclusion commutes with the conjugate transpose.

    source
    theorem TauCeti.glBlockSucc_injective (k : Type u) (n : ℕ) [Semiring k] :
    Function.Injective ⇑(glBlockSucc k n)

    The block inclusion is injective, so it really embeds GL (Fin n) k in GL (Fin (n + 1)) k and the chain GL 1 ⊂ GL 2 ⊂ ⋯ is a chain of subgroups. Use it to identify two invertible matrices from the equality of their extensions.

    source
    @[simp]
    theorem TauCeti.glBlockSucc_diagGL (k : Type u) (n : ℕ) [Semiring k] (t : Fin n → kˣ) :
    (glBlockSucc k n) (diagGL t) = diagGL (Fin.snoc t 1)

    The block inclusion matches the chains of diagonal tori: it sends the diagonal matrix with entries t to the one whose entries are t followed by 1.

    source
    @[simp]
    theorem TauCeti.det_glBlockSucc (k : Type u) (n : ℕ) [CommRing k] (g : GL (Fin n) k) :
    Matrix.GeneralLinearGroup.det ((glBlockSucc k n) g) = Matrix.GeneralLinearGroup.det g

    The block inclusion preserves determinants, so it carries special linear matrices to special linear matrices.