Matrix.SpecialLinearGroup.det_coe
theorem Matrix.SpecialLinearGroup.det_coe :
∀ {n : Type u} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type v} [inst_2 : CommRing R]
(A : Matrix.SpecialLinearGroup n R), (↑A).det = 1
The theorem `Matrix.SpecialLinearGroup.det_coe` states that for any type `n` with decidable equality and finite number of elements, and any `R` which forms a commutative ring, a matrix `A` from the special linear group of `n by n` matrices with entries from `R` will always have a determinant equal to 1, i.e., if we take the determinant of the underlying matrix of `A` (obtained by the coercion `↑A`), it will always equal 1. This is in accordance with the definition of the special linear group, which is the group of `n by n` matrices with determinant 1.
More concisely: For any commutative ring R and finite type n with decidable equality, the determinant of every special linear group element (n by n matrix with entries from R and determinant 1) is equal to 1.
|
Matrix.SpecialLinearGroup.coe_one
theorem Matrix.SpecialLinearGroup.coe_one :
∀ {n : Type u} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type v} [inst_2 : CommRing R], ↑1 = 1
This theorem states that for any type `n` with decidable equality and finiteness, and for any type `R` that forms a commutative ring, the canonical embedding (denoted by `↑`) of the multiplicative identity element `1` from `R` into matrix special linear group is equal to the identity matrix `1`.
More concisely: For any commutative ring R and decidably finite type n with decidable equality, the canonical embedding of the multiplicative identity 1 in R into the special linear group SL(n R) is equal to the identity matrix 1.
|
IsCoprime.mulVecSL
theorem IsCoprime.mulVecSL :
∀ {R : Type u_1} [inst : CommRing R] {v : Fin 2 → R},
IsCoprime (v 0) (v 1) →
∀ (A : Matrix.SpecialLinearGroup (Fin 2) R), IsCoprime ((↑A).mulVec v 0) ((↑A).mulVec v 1)
The theorem `IsCoprime.mulVecSL` states that for any commutative ring `R` and any vector `v` in `R` with two elements such that the elements of `v` are coprime, if `v` is left-multiplied by any matrix `A` from the special linear group `SL(2, R)` (i.e., 2x2 matrices with determinant 1), the resulting vector also has coprime elements. In mathematical terms, if `(v 0)` and `(v 1)` are coprime, then the elements of the vector resulting from the multiplication `A * v` are also coprime.
More concisely: For any commutative ring `R`, if `v` is a two-element vector in `R` with coprime components and `A` is a 2x2 matrix in `SL(2, R)`, then the components of `A * v` are coprime.
|
IsCoprime.exists_SL2_col
theorem IsCoprime.exists_SL2_col :
∀ {R : Type u_1} [inst : CommRing R] {a b : R}, IsCoprime a b → ∀ (j : Fin 2), ∃ g, ↑g 0 j = a ∧ ↑g 1 j = b := by
sorry
The theorem states that for any pair of coprime elements `a` and `b` in a commutative ring `R`, there exists a matrix `g` in the special linear group SL(2, R) such that the `j`-th column of `g` is formed by the elements `a` and `b`. The special linear group SL(2, R) consists of 2x2 matrices with determinant equal to 1. The coprimality of `a` and `b` is defined by the existence of two elements in `R` whose linear combination with `a` and `b` respectively gives 1.
More concisely: For any coprime elements `a` and `b` in a commutative ring `R`, there exists a matrix `g` in the special linear group SL(2, R) with determinant 1 such that the first and second columns of `g` are `[a, b]`.
|
IsCoprime.vecMulSL
theorem IsCoprime.vecMulSL :
∀ {R : Type u_1} [inst : CommRing R] {v : Fin 2 → R},
IsCoprime (v 0) (v 1) →
∀ (A : Matrix.SpecialLinearGroup (Fin 2) R), IsCoprime (Matrix.vecMul v (↑A) 0) (Matrix.vecMul v (↑A) 1)
The theorem `IsCoprime.vecMulSL` states that for any commutative ring `R` and any vector `v` from `R` with two components such that the components are coprime, if we right-multiply this vector by any matrix `A` from the Special Linear Group of 2x2 matrices with coefficients in `R` (i.e., 2x2 matrices with determinant equal to 1), the resulting vector will also have coprime components. In other words, the operation of right-multiplying by a matrix from the Special Linear Group preserves the property of being coprime for vectors in `R^2`.
More concisely: For any commutative ring R and vectors v in R^2 with coprime components, the components of the resulting vector obtained by right-multiplying v with any 2x2 matrix A in the Special Linear Group over R are also coprime.
|
Matrix.SpecialLinearGroup.coe_mul
theorem Matrix.SpecialLinearGroup.coe_mul :
∀ {n : Type u} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type v} [inst_2 : CommRing R]
(A B : Matrix.SpecialLinearGroup n R), ↑(A * B) = ↑A * ↑B
This theorem states that for any type `n` with decidable equality and finiteness, and any commutative ring `R`, the multiplication operation in the special linear group of `n` by `n` matrices with coefficients in `R` is compatible with the matrix multiplication. Specifically, if `A` and `B` are elements of the special linear group, then the matrix of the product `A * B` in the group is the same as the product of the matrices of `A` and `B`.
More concisely: For any commutative ring R and type n with decidable equality and finiteness, the multiplication operation in the special linear group of n by n matrices over R preserves matrix multiplication.
|
IsCoprime.exists_SL2_row
theorem IsCoprime.exists_SL2_row :
∀ {R : Type u_1} [inst : CommRing R] {a b : R}, IsCoprime a b → ∀ (i : Fin 2), ∃ g, ↑g i 0 = a ∧ ↑g i 1 = b := by
sorry
This theorem states that for any pair of coprime elements, `a` and `b`, in a commutative ring `R`, there exists a matrix `g` in the special linear group SL(2, R) such that either the top row or the bottom row of `g` (depending on whether `i` is `0` or `1`) is `[a, b]`. The special linear group SL(2, R) consists of 2x2 matrices with determinant 1 over the ring `R`. The pair of elements are said to be coprime if there exist two elements in the ring such that their weighted sum is 1, with the weights being the coprime elements themselves.
More concisely: For any coprime elements `a` and `b` in a commutative ring `R`, there exists a matrix `g` in SL(2, R) with determinant 1 such that one of its rows is `[a, b]`.
|