Matrix Groups - Mizar

1. Matrix Groups
2. References

1. Matrix Groups

1.1. General Linear Group

Let \(K\) be a field, \(n\in\NN\) be a positive integer. The General Linear Group denoted \(GL(n,K)\) or \(GL_{n}(K)\) is the group consisting of invertible \(n\times n\) matrices over the field \(K\) using matrix multiplication as the binary operation.

We don't really need \(K\) to be a field, it could just be an associative unital ring (see the entry in the Encyclopedia of Mathematics).

This is a deceptive example, because it defines a "functor": given a specific \(n\) and \(K\), we get a group. Most of this has been formalized in, e.g., matrix_3 and related articles ("invertible" is defined in matrix_6).

Matrix inversion is closed on the set of invertible square matrices, as proven in theorem MATRIX_6:16.

Matrix multiplication is closed on the set of invertible square matrices, as proven in MATRIX_6:45.

Associativity of matrix multiplication is proven in MATRIX_3:33.

definition
  let n, k, m be Nat;
  let K be Ring;
  let A be Matrix of n,k,K;
  let B be Matrix of width A,m,K;
  func matrix_mult (A,B) -> Matrix of len A, width B,K equals
  A*B;
end;

definition
  let n be Nat;
  let K be Field;
  func GL(n,K) -> Group means
  (for M being object
   holds (M is invertible Matrix of n,K) iff (M in it)) &
  (the multF of it = matrix_mult||(the carrier of it));
  existence
  proof
    thus ex G being Group st (for M being object
         holds (M is invertible Matrix of n,K) iff (M in G)) &
         (the multF of G = matrix_mult||(the carrier of G));
  end;
  uniqueness
  proof
    defpred P[Group] means (for M being object
    holds (M is invertible Matrix of n,K) iff (M in $1)) &
    (the multF of $1 = matrix_mult||(the carrier of $1));

    let G1,G2 be Group;
    assume A1: P[G1];
    assume A2: P[G2];
    thus G1=G2;
  end;
end;

:: MATRIX_3:18 proves (1.(K,n))*A = A
:: MATRIX_3:19 proves A*(1.(K,n)) = A
theorem
  for n being Nat
  for K being Field
  holds 1_(GL(n,K)) = 1.(K,n) by GROUP_1:def 4,MATRIX_3:18,19;

theorem
  for n being Nat
  for K being Field
  for M being Element of GL(n,K)
  holds inverse_op(GL(n,K)).M = M ~ by MATRIX_6:def 4,GROUP_1:def 6;

linear-transformation is defined in RANKNULL
The associated matrix for a linear transformation is defined in MATRLIN as AutMt.
The linear transformation for a given matrix is defined in MATRLIN2 as Mx2Tran.

1.2. Special Linear Group

Let \(n\) be a positive integer, \(K\) be a field. The Special Linear Group \(SL(n,K)\) consists of invertible matrices of determinant one, and its binary operation is matrix multiplication.

The determinant of the identity matrix being unity is proven in theorem MATRIX_7:16.

definition
  let n be Nat;
  let K be Field;
  func SL(n,K) -> Group means
  :Def:
  (for M being invertible Matrix of n,K
   holds (Det M = 1.K) iff (M in it)) &
  (the multF of it = matrix_mult||(the carrier of it));
  existence
  proof
    thus ex G being Group st
    (for M being invertible Matrix of n,K
     holds (Det M = 1.K) iff (M in G)) &
    (the multF of G = matrix_mult||(the carrier of G));
  end;
  uniqueness
  proof
    defpred P[Group] means
    (for M being invertible Matrix of n,K
     holds (Det M = 1.K) iff (M in $1)) &
    (the multF of $1 = matrix_mult||(the carrier of $1));
    let G1,G2 be Group;
    assume A1: P[G1];
    assume A2: P[G2];
    thus G1=G2;
  end;
end;

theorem
  for n being Nat
  for K being Field
  holds SL(n,K) is Subgroup of GL(n,K)
proof
  let n be Nat;
  let K be Field;
  set UH = the carrier of SL(n,K);
  set UG = the carrier of GL(n,K);
  A1: UH c= UG;
  hence UH c= UG;
  A2: [:UH,UH:] c= [:UG,UG:] by A1,ZFMISC_1:96;
  the multF of SL(n,K) = matrix_mult||UH &
  the multF of GL(n,K) = matrix_mult||UG by GROUP_2:def 5;
  hence thesis by A2,FUNCT_1:51;
end;

1.3. Projective Linear Groups

We could then define the projective linear groups as:

definition
  let n be Nat;
  let K be Field;
  func PGL(n,K) -> Group equals GL(n,K)./.(center GL(n,K));
  coherence
  proof
    thus GL(n,K)./.(center GL(n,K)) is Group;
  end;
  
  func PSL(n,L) -> Group equals SL(n,K)./.(center SL(n,K))
  coherence
  proof
    thus SL(n,K)./.(center SL(n,K)) is Group;
  end;
end;

If we include NAT_6 in our registrations, then we can register positive for Nat. Be sure to include XCMPLX_0 in the vocabulary.

registration
  cluster positive for Nat;
  existence
  proof
    take 1;
    thus thesis;
  end;
  cluster zero for natural number;
  existence
  proof
    take 0;
    thus thesis;
  end;
  cluster non zero for Nat; :: natural number;
  existence
  proof
    take 1;
    thus thesis;
  end;
end;
registration
  cluster non zero -> positive for Nat;
  coherence
  proof
    for x being Nat st x is non zero holds x is positive
    proof
      let x be Nat;
      assume A1: x is non zero;
      then x <> 0;
      then x > 0;
      hence x is positive;
    end;
    hence thesis;
  end;
end;

2. References

Bourbaki, Algebra; ch II §1.2 (pg 195) defines \(\mathbf{GL}(E)\) and II §10.7 (pg. 349) defines \(\mathbf{GL}_{n}(A)\) or \(\mathbf{GL}(n,A)\)