Documentation

Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs

The General Linear group $GL(n, R)$ #

This file defines the elements of the General Linear group Matrix.GeneralLinearGroup n R, consisting of all invertible n by n R-matrices.

Main definitions #

Tags #

matrix group, group, matrix inverse

@[reducible, inline]
abbrev Matrix.GeneralLinearGroup (n : Type u) (R : Type v) [DecidableEq n] [Fintype n] [CommRing R] :
Type (max v u)

GL n R is the group of n by n R-matrices with unit determinant. Defined as a subtype of matrices

Equations
Instances For

    GL n R is the group of n by n R-matrices with unit determinant. Defined as a subtype of matrices

    Equations
    Instances For
      instance Matrix.GeneralLinearGroup.instCoeFun {n : Type u} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] :
      CoeFun (GL n R) fun (x : GL n R) => nnR

      This instance is here for convenience, but is not the simp-normal form.

      Equations
      • Matrix.GeneralLinearGroup.instCoeFun = { coe := fun (A : GL n R) => A }
      @[simp]
      theorem Matrix.GeneralLinearGroup.val_det_apply {n : Type u} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] (A : GL n R) :
      (Matrix.GeneralLinearGroup.det A) = (↑A).det
      @[simp]
      theorem Matrix.GeneralLinearGroup.val_inv_det_apply {n : Type u} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] (A : GL n R) :
      (Matrix.GeneralLinearGroup.det A)⁻¹ = (↑A⁻¹).det

      The determinant of a unit matrix is itself a unit.

      Equations
      • Matrix.GeneralLinearGroup.det = { toFun := fun (A : GL n R) => { val := (↑A).det, inv := (↑A⁻¹).det, val_inv := , inv_val := }, map_one' := , map_mul' := }
      Instances For

        The GL n R and Matrix.GeneralLinearGroup R n groups are multiplicatively equivalent

        Equations
        • Matrix.GeneralLinearGroup.toLin = Units.mapEquiv Matrix.toLinAlgEquiv'.toMulEquiv
        Instances For
          def Matrix.GeneralLinearGroup.mk' {n : Type u} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] (A : Matrix n n R) :
          Invertible A.detGL n R

          Given a matrix with invertible determinant we get an element of GL n R

          Equations
          Instances For
            noncomputable def Matrix.GeneralLinearGroup.mk'' {n : Type u} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] (A : Matrix n n R) (h : IsUnit A.det) :
            GL n R

            Given a matrix with unit determinant we get an element of GL n R

            Equations
            Instances For
              def Matrix.GeneralLinearGroup.mkOfDetNeZero {n : Type u} [DecidableEq n] [Fintype n] {K : Type u_1} [Field K] (A : Matrix n n K) (h : A.det 0) :
              GL n K

              Given a matrix with non-zero determinant over a field, we get an element of GL n K

              Equations
              Instances For
                theorem Matrix.GeneralLinearGroup.ext_iff {n : Type u} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] (A : GL n R) (B : GL n R) :
                A = B ∀ (i j : n), A i j = B i j
                theorem Matrix.GeneralLinearGroup.ext {n : Type u} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] ⦃A : GL n R ⦃B : GL n R (h : ∀ (i j : n), A i j = B i j) :
                A = B

                Not marked @[ext] as the ext tactic already solves this.

                @[simp]
                theorem Matrix.GeneralLinearGroup.coe_mul {n : Type u} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] (A : GL n R) (B : GL n R) :
                (A * B) = A * B
                @[simp]
                theorem Matrix.GeneralLinearGroup.coe_one {n : Type u} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] :
                1 = 1
                theorem Matrix.GeneralLinearGroup.coe_inv {n : Type u} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] (A : GL n R) :
                A⁻¹ = (↑A)⁻¹

                An element of the matrix general linear group on (n) [Fintype n] can be considered as an element of the endomorphism general linear group on n → R.

                Equations
                • Matrix.GeneralLinearGroup.toLinear = Units.mapEquiv Matrix.toLinAlgEquiv'.toRingEquiv.toMulEquiv
                Instances For
                  @[simp]
                  theorem Matrix.GeneralLinearGroup.coe_toLinear {n : Type u} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] (A : GL n R) :
                  (Matrix.GeneralLinearGroup.toLinear A) = (↑A).mulVecLin
                  @[simp]
                  theorem Matrix.GeneralLinearGroup.toLinear_apply {n : Type u} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] (A : GL n R) (v : nR) :
                  (Matrix.GeneralLinearGroup.toLinear A).toLinearEquiv v = (↑A).mulVecLin v
                  def Matrix.GeneralLinearGroup.map {n : Type u} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] {S : Type u_1} [CommRing S] (f : R →+* S) :
                  GL n R →* GL n S

                  A ring homomorphism f : R →+* S induces a homomorphism GLₙ(f) : GLₙ(R) →* GLₙ(S).

                  Equations
                  Instances For
                    @[simp]
                    theorem Matrix.GeneralLinearGroup.map_apply {n : Type u} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] {S : Type u_1} [CommRing S] (f : R →+* S) (i : n) (j : n) (g : GL n R) :
                    ((Matrix.GeneralLinearGroup.map f) g) i j = f (g i j)
                    @[simp]
                    @[simp]
                    theorem Matrix.GeneralLinearGroup.map_one {n : Type u} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] {S : Type u_1} [CommRing S] (f : R →+* S) :
                    theorem Matrix.GeneralLinearGroup.map_det {n : Type u} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] {S : Type u_1} [CommRing S] (f : R →+* S) (g : GL n R) :
                    Matrix.GeneralLinearGroup.det ((Matrix.GeneralLinearGroup.map f) g) = (Units.map f) (Matrix.GeneralLinearGroup.det g)
                    @[simp]
                    theorem Matrix.GeneralLinearGroup.coe_map_mul_map_inv {n : Type u} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] {S : Type u_1} [CommRing S] (f : R →+* S) (g : GL n R) :
                    (↑g).map f * (↑g)⁻¹.map f = 1
                    @[simp]
                    theorem Matrix.GeneralLinearGroup.coe_map_inv_mul_map {n : Type u} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] {S : Type u_1} [CommRing S] (f : R →+* S) (g : GL n R) :
                    (↑g)⁻¹.map f * (↑g).map f = 1

                    The map from SL(n) to GL(n) underlying the coercion, forgetting the value of the determinant.

                    Equations
                    • A = { val := A, inv := A⁻¹, val_inv := , inv_val := }
                    Instances For
                      Equations
                      • Matrix.SpecialLinearGroup.hasCoeToGeneralLinearGroup = { coe := Matrix.SpecialLinearGroup.coeToGL }
                      @[simp]
                      theorem Matrix.SpecialLinearGroup.coeToGL_det {n : Type u} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] (g : Matrix.SpecialLinearGroup n R) :
                      Matrix.GeneralLinearGroup.det g = 1
                      def Matrix.GLPos (n : Type u) (R : Type v) [DecidableEq n] [Fintype n] [LinearOrderedCommRing R] :
                      Subgroup (GL n R)

                      This is the subgroup of nxn matrices with entries over a linear ordered ring and positive determinant.

                      Equations
                      Instances For
                        @[simp]
                        theorem Matrix.mem_glpos {n : Type u} {R : Type v} [DecidableEq n] [Fintype n] [LinearOrderedCommRing R] (A : GL n R) :
                        A Matrix.GLPos n R 0 < (Matrix.GeneralLinearGroup.det A)
                        theorem Matrix.GLPos.det_ne_zero {n : Type u} {R : Type v} [DecidableEq n] [Fintype n] [LinearOrderedCommRing R] (A : (Matrix.GLPos n R)) :
                        (↑A).det 0

                        Formal operation of negation on general linear group on even cardinality n given by negating each element.

                        Equations
                        • Matrix.instNegSubtypeGeneralLinearGroupMemSubgroupGLPos = { neg := fun (g : (Matrix.GLPos n R)) => -g, }
                        @[simp]
                        theorem Matrix.GLPos.coe_neg_GL {n : Type u} {R : Type v} [DecidableEq n] [Fintype n] [LinearOrderedCommRing R] [Fact (Even (Fintype.card n))] (g : (Matrix.GLPos n R)) :
                        (-g) = -g
                        @[simp]
                        theorem Matrix.GLPos.coe_neg {n : Type u} {R : Type v} [DecidableEq n] [Fintype n] [LinearOrderedCommRing R] [Fact (Even (Fintype.card n))] (g : (Matrix.GLPos n R)) :
                        (-g) = -g
                        @[simp]
                        theorem Matrix.GLPos.coe_neg_apply {n : Type u} {R : Type v} [DecidableEq n] [Fintype n] [LinearOrderedCommRing R] [Fact (Even (Fintype.card n))] (g : (Matrix.GLPos n R)) (i : n) (j : n) :
                        (-g) i j = -g i j
                        Equations

                        Matrix.SpecialLinearGroup n R embeds into GL_pos n R

                        Equations
                        • Matrix.SpecialLinearGroup.toGLPos = { toFun := fun (A : Matrix.SpecialLinearGroup n R) => A, , map_one' := , map_mul' := }
                        Instances For
                          Equations
                          • Matrix.SpecialLinearGroup.instCoeSubtypeGeneralLinearGroupMemSubgroupGLPos = { coe := Matrix.SpecialLinearGroup.toGLPos }
                          theorem Matrix.SpecialLinearGroup.toGLPos_injective {n : Type u} [DecidableEq n] [Fintype n] {R : Type v} [LinearOrderedCommRing R] :
                          Function.Injective Matrix.SpecialLinearGroup.toGLPos
                          @[simp]
                          theorem Matrix.SpecialLinearGroup.coe_GLPos_coe_GL_coe_matrix {n : Type u} [DecidableEq n] [Fintype n] {R : Type v} [LinearOrderedCommRing R] (g : Matrix.SpecialLinearGroup n R) :
                          (Matrix.SpecialLinearGroup.toGLPos g) = g

                          Coercing a Matrix.SpecialLinearGroup via GL_pos and GL is the same as coercing straight to a matrix.

                          @[simp]
                          theorem Matrix.SpecialLinearGroup.coe_to_GLPos_to_GL_det {n : Type u} [DecidableEq n] [Fintype n] {R : Type v} [LinearOrderedCommRing R] (g : Matrix.SpecialLinearGroup n R) :
                          Matrix.GeneralLinearGroup.det (Matrix.SpecialLinearGroup.toGLPos g) = 1
                          theorem Matrix.SpecialLinearGroup.coe_GLPos_neg {n : Type u} [DecidableEq n] [Fintype n] {R : Type v} [LinearOrderedCommRing R] [Fact (Even (Fintype.card n))] (g : Matrix.SpecialLinearGroup n R) :
                          Matrix.SpecialLinearGroup.toGLPos (-g) = -Matrix.SpecialLinearGroup.toGLPos g