LeanPool.BruhatTits.Utils.Matrix

noncomputable def Matrix.coeffs {R : Type u_1} {n : Type u_2} {m : Type u_3} (g : Matrix n m R) : Set R

The set of coefficients appearing in a matrix.

Equations

• g.coeffs = Set.image2 g Set.univ Set.univ

theorem Matrix.mem_coeffs {R : Type u_1} {n : Type u_2} {m : Type u_3} (g : Matrix n m R) (i : n) (j : m) : g i j ∈ g.coeffs

theorem Matrix.coeffs_nonempty {R : Type u_1} {n : Type u_2} {m : Type u_3} [Nonempty n] [Nonempty m] (g : Matrix n m R) : g.coeffs.Nonempty

theorem Matrix.finite_coeffs {R : Type u_1} {n : Type u_2} {m : Type u_3} [Finite n] [Finite m] (g : Matrix n m R) : g.coeffs.Finite

@[simp]

theorem Matrix.transpose_coeffs {R : Type u_1} {n : Type u_2} {m : Type u_3} (g : Matrix n m R) : g.transpose.coeffs = g.coeffs

theorem Matrix.coeffs_reindex {R : Type u_1} {n : Type u_2} {m : Type u_3} {n' : Type u_4} {m' : Type u_5} (g : Matrix n m R) (e : n ≃ n') (f : m ≃ m') : ((reindex e f) g).coeffs = g.coeffs

theorem Matrix.coeffs_fromBlocks {R : Type u_1} {n : Type u_2} {m : Type u_3} {n' : Type u_4} {m' : Type u_5} (A : Matrix n n' R) (B : Matrix n m R) (C : Matrix m' n' R) (D : Matrix m' m R) : (fromBlocks A B C D).coeffs = A.coeffs ∪ B.coeffs ∪ C.coeffs ∪ D.coeffs

theorem Matrix.coeffs_zero {R : Type u_1} {n : Type u_2} {m : Type u_3} [Zero R] [Nonempty n] [Nonempty m] : coeffs 0 = {0}

@[simp]

theorem Matrix.coeffs_one {R : Type u_1} {n : Type u_2} [One R] [Zero R] [DecidableEq n] : coeffs 1 ⊆ {0, 1}

theorem Matrix.one_mem_coeffs_one {R : Type u_1} {n : Type u_2} [One R] [Zero R] [Nonempty n] [DecidableEq n] : 1 ∈ coeffs 1

theorem Matrix.coeffs_unique {R : Type u_1} {n : Type u_2} {m : Type u_3} [Unique n] [Unique m] (g : Matrix n m R) : g.coeffs = {g default default}

@[simp]

theorem Matrix.map_ite {R : Type u_1} [CommRing R] {S : Type u_6} [CommRing S] (f : R →+* S) (p : Prop) (a b : R) [Decidable p] : f (if p then a else b) = if p then f a else f b

@[simp]

theorem Matrix.map_transvection {R : Type u_1} {n : Type u_2} [CommRing R] [DecidableEq n] {S : Type u_6} [CommRing S] (f : R →+* S) (i j : n) (c : R) : (transvection i j c).map ⇑f = transvection i j (f c)

theorem Matrix.map_listProd {R : Type u_1} {n : Type u_2} [CommRing R] [DecidableEq n] [Fintype n] {S : Type u_6} [CommRing S] (f : R →+* S) (L : List (Matrix n n R)) : (List.map (fun (g : Matrix n n R) => g.map ⇑f) L).prod = L.prod.map ⇑f

theorem Matrix.map_listProd_toGL {R : Type u_1} {n : Type u_2} [CommRing R] [DecidableEq n] [Fintype n] {S : Type u_6} [CommRing S] (f : R →+* S) (L : List (GL n R)) : (List.map (fun (g : GL n R) => (↑g).map ⇑f) L).prod = (↑L.prod).map ⇑f

noncomputable def Matrix.coeffsSup {R : Type u_1} {n : Type u_2} {m : Type u_3} [CommRing R] {Γ₀ : Type u_6} [LinearOrderedCommMonoidWithZero Γ₀] (v : Valuation R Γ₀) [Finite n] [Finite m] [Nonempty n] [Nonempty m] (g : Matrix n m R) : Γ₀

The supremum of the coefficients.

Equations

• Matrix.coeffsSup v g = ⋯.toFinset.sup' ⋯ ⇑v

theorem Matrix.coeff_le_coeffs_sup {R : Type u_1} {n : Type u_2} {m : Type u_3} [CommRing R] {Γ₀ : Type u_6} [LinearOrderedCommMonoidWithZero Γ₀] (v : Valuation R Γ₀) [Finite n] [Finite m] [Nonempty n] [Nonempty m] (g : Matrix n m R) (i : n) (j : m) : v (g i j) ≤ coeffsSup v g

theorem Matrix.coeffs_sup_le {R : Type u_1} {n : Type u_2} {m : Type u_3} [CommRing R] {Γ₀ : Type u_6} [LinearOrderedCommMonoidWithZero Γ₀] (v : Valuation R Γ₀) [Finite n] [Finite m] [Nonempty n] [Nonempty m] {g : Matrix n m R} {a : Γ₀} (h : ∀ (i : n) (j : m), v (g i j) ≤ a) : coeffsSup v g ≤ a

theorem Matrix.coeffs_sup_exists_repr {R : Type u_1} {n : Type u_2} {m : Type u_3} [CommRing R] {Γ₀ : Type u_6} [LinearOrderedCommMonoidWithZero Γ₀] (v : Valuation R Γ₀) [Finite n] [Finite m] [Nonempty n] [Nonempty m] (g : Matrix n m R) : ∃ (p : n × m), v (g p.1 p.2) = coeffsSup v g

noncomputable def Matrix.coeffsSupAt {R : Type u_1} {n : Type u_2} {m : Type u_3} [CommRing R] {Γ₀ : Type u_6} [LinearOrderedCommMonoidWithZero Γ₀] (v : Valuation R Γ₀) [Finite n] [Finite m] [Nonempty n] [Nonempty m] (g : Matrix n m R) : n × m

A matrix position where the coefficient supremum is attained.

Equations

• Matrix.coeffsSupAt v g = ⋯.choose

theorem Matrix.coeffs_sup_at_sup {R : Type u_1} {n : Type u_2} {m : Type u_3} [CommRing R] {Γ₀ : Type u_6} [LinearOrderedCommMonoidWithZero Γ₀] (v : Valuation R Γ₀) [Finite n] [Finite m] [Nonempty n] [Nonempty m] (g : Matrix n m R) : v (g (coeffsSupAt v g).1 (coeffsSupAt v g).2) = coeffsSup v g

theorem Matrix.coeffs_sup_transpose {R : Type u_1} {n : Type u_2} {m : Type u_3} [CommRing R] {Γ₀ : Type u_6} [LinearOrderedCommMonoidWithZero Γ₀] (v : Valuation R Γ₀) [Finite n] [Finite m] [Nonempty n] [Nonempty m] (g : Matrix n m R) : coeffsSup v g.transpose = coeffsSup v g

The supremum of the coefficients is invariant under transposition.

theorem Matrix.coeffs_sup_fromBlocks {R : Type u_1} {n : Type u_2} {m : Type u_3} {n' : Type u_4} {m' : Type u_5} [CommRing R] {Γ₀ : Type u_6} [LinearOrderedCommMonoidWithZero Γ₀] (v : Valuation R Γ₀) [Finite n] [Finite m] [Finite n'] [Finite m'] [Nonempty n] [Nonempty m] [Nonempty n'] [Nonempty m'] (A : Matrix n n' R) (B : Matrix n m R) (C : Matrix m' n' R) (D : Matrix m' m R) : coeffsSup v (fromBlocks A B C D) = max (max (max (coeffsSup v A) (coeffsSup v B)) (coeffsSup v C)) (coeffsSup v D)

@[simp]

theorem Matrix.mul_swap_coeffs {R : Type u_1} {m : Type u_3} [CommRing R] [DecidableEq m] [Fintype m] (g : Matrix m m R) (i j : m) : (g * swap R i j).coeffs = g.coeffs

@[simp]

theorem Matrix.swap_mul_coeffs {R : Type u_1} {m : Type u_3} [CommRing R] [DecidableEq m] [Fintype m] (g : Matrix m m R) (i j : m) : (swap R i j * g).coeffs = g.coeffs

@[simp]

theorem Matrix.coeffs_sup_mul_swap {R : Type u_1} {m : Type u_3} [CommRing R] {Γ₀ : Type u_6} [LinearOrderedCommMonoidWithZero Γ₀] (v : Valuation R Γ₀) [DecidableEq m] [Fintype m] [Nonempty m] (g : Matrix m m R) (i j : m) : coeffsSup v (g * swap R i j) = coeffsSup v g

@[simp]

theorem Matrix.coeffs_sup_swap_mul {R : Type u_1} {m : Type u_3} [CommRing R] {Γ₀ : Type u_6} [LinearOrderedCommMonoidWithZero Γ₀] (v : Valuation R Γ₀) [DecidableEq m] [Fintype m] [Nonempty m] (g : Matrix m m R) (i j : m) : coeffsSup v (swap R i j * g) = coeffsSup v g

theorem Matrix.coeffs_sup_reindex {R : Type u_1} {n : Type u_2} {m : Type u_3} {n' : Type u_4} {m' : Type u_5} [CommRing R] {Γ₀ : Type u_6} [LinearOrderedCommMonoidWithZero Γ₀] (v : Valuation R Γ₀) [Finite n] [Finite m] [Finite n'] [Finite m'] [Nonempty n] [Nonempty m] [Nonempty n'] [Nonempty m'] (g : Matrix n m R) (e : n ≃ n') (f : m ≃ m') : coeffsSup v ((reindex e f) g) = coeffsSup v g

theorem Matrix.coeffs_sup_toBlock₁₁_le_coeffs_sup {R : Type u_1} {n : Type u_2} {m : Type u_3} {n' : Type u_4} {m' : Type u_5} [CommRing R] {Γ₀ : Type u_6} [LinearOrderedCommMonoidWithZero Γ₀] (v : Valuation R Γ₀) [Finite n] [Finite m] [Finite n'] [Finite m'] [Nonempty n] [Nonempty m'] (g : Matrix (n ⊕ n') (m' ⊕ m) R) : coeffsSup v g.toBlocks₁₁ ≤ coeffsSup v g

theorem Matrix.coeffs_sup_zero {R : Type u_1} {n : Type u_2} {m : Type u_3} [CommRing R] {Γ₀ : Type u_6} [LinearOrderedCommMonoidWithZero Γ₀] (v : Valuation R Γ₀) [Finite n] [Finite m] [Nonempty n] [Nonempty m] : coeffsSup v 0 = 0

theorem Matrix.coeffs_sup_one {R : Type u_1} {n : Type u_2} [CommRing R] {Γ₀ : Type u_6} [LinearOrderedCommMonoidWithZero Γ₀] (v : Valuation R Γ₀) [Finite n] [Nonempty n] [DecidableEq n] : coeffsSup v 1 = 1

theorem Matrix.coeffs_sup_unique {R : Type u_1} {n : Type u_2} [CommRing R] {Γ₀ : Type u_6} [LinearOrderedCommMonoidWithZero Γ₀] (v : Valuation R Γ₀) [Finite n] [Unique n] (g : Matrix n n R) : coeffsSup v g = v (g default default)

def Matrix.TransvectionStruct.toGL {R : Type u_1} {n : Type u_2} [CommRing R] [DecidableEq n] [Fintype n] (t : TransvectionStruct n R) : GL n R

GL version of toMatrix.

Equations

• t.toGL = { val := t.toMatrix, inv := t.inv.toMatrix, val_inv := ⋯, inv_val := ⋯ }

def Matrix.GL.transpose {R : Type u_1} {n : Type u_2} [CommRing R] [DecidableEq n] [Fintype n] (g : GL n R) : GL n R

The transpose of an invertible matrix as an element of GL.

Equations

• Matrix.GL.transpose g = { val := (↑g).transpose, inv := g.inv.transpose, val_inv := ⋯, inv_val := ⋯ }

@[simp]

theorem Matrix.GL.val_transpose {R : Type u_1} {n : Type u_2} [CommRing R] [DecidableEq n] [Fintype n] (g : GL n R) : ↑(transpose g) = (↑g).transpose

theorem Matrix.GL.val_inv_transpose {R : Type u_1} {n : Type u_2} [CommRing R] [DecidableEq n] [Fintype n] (g : GL n R) : ↑(transpose g)⁻¹ = g.inv.transpose

def Matrix.GL.diagonal {R : Type u_1} {n : Type u_2} [CommRing R] [DecidableEq n] [Fintype n] (g : n → Rˣ) : GL n R

A diagonal matrix with unit diagonal entries as an element of GL.

Equations

• Matrix.GL.diagonal g = { val := Matrix.diagonal fun (j : n) => ↑(g j), inv := Matrix.diagonal fun (j : n) => (g j).inv, val_inv := ⋯, inv_val := ⋯ }

@[simp]

theorem Matrix.GL.val_diagonal {R : Type u_1} {n : Type u_2} [CommRing R] [DecidableEq n] [Fintype n] (g : n → Rˣ) : ↑(diagonal g) = Matrix.diagonal fun (j : n) => ↑(g j)

theorem Matrix.GL.val_inv_diagonal {R : Type u_1} {n : Type u_2} [CommRing R] [DecidableEq n] [Fintype n] (g : n → Rˣ) : ↑(diagonal g)⁻¹ = Matrix.diagonal fun (j : n) => (g j).inv

theorem Matrix.GL.diagonal_det {R : Type u_1} {n : Type u_2} [CommRing R] [DecidableEq n] [Fintype n] (g : n → Rˣ) : GeneralLinearGroup.det (diagonal g) = ∏ i : n, g i

def Matrix.GL.diagonalBlocks {R : Type u_1} {n : Type u_2} {m : Type u_3} [CommRing R] [DecidableEq n] [Fintype n] [DecidableEq m] [Fintype m] (g : GL n R) (h : GL m R) : GL (n ⊕ m) R

The block diagonal sum of two general linear matrices.

Equations

• Matrix.GL.diagonalBlocks g h = { val := Matrix.fromBlocks (↑g) 0 0 ↑h, inv := Matrix.fromBlocks g.inv 0 0 h.inv, val_inv := ⋯, inv_val := ⋯ }

@[simp]

theorem Matrix.GL.val_diagonalBlocks {R : Type u_1} {n : Type u_2} {m : Type u_3} [CommRing R] [DecidableEq n] [Fintype n] [DecidableEq m] [Fintype m] (g : GL n R) (h : GL m R) : ↑(diagonalBlocks g h) = fromBlocks (↑g) 0 0 ↑h

theorem Matrix.GL.val_inv_diagonalBlocks {R : Type u_1} {n : Type u_2} {m : Type u_3} [CommRing R] [DecidableEq n] [Fintype n] [DecidableEq m] [Fintype m] (g : GL n R) (h : GL m R) : ↑(diagonalBlocks g h)⁻¹ = fromBlocks g.inv 0 0 h.inv

def Matrix.GL.reindex {R : Type u_1} {n : Type u_2} {m : Type u_3} [CommRing R] [DecidableEq n] [Fintype n] [DecidableEq m] [Fintype m] (e : n ≃ m) (g : GL n R) : GL m R

Reindex the rows and columns of an element of GL along an equivalence.

Equations

• Matrix.GL.reindex e g = { val := (Matrix.reindex e e) ↑g, inv := (Matrix.reindex e e) g.inv, val_inv := ⋯, inv_val := ⋯ }

@[simp]

theorem Matrix.GL.val_reindex {R : Type u_1} {n : Type u_2} {m : Type u_3} [CommRing R] [DecidableEq n] [Fintype n] [DecidableEq m] [Fintype m] (e : n ≃ m) (g : GL n R) : ↑(reindex e g) = (Matrix.reindex e e) ↑g

theorem Matrix.GL.val_inv_reindex {R : Type u_1} {n : Type u_2} {m : Type u_3} [CommRing R] [DecidableEq n] [Fintype n] [DecidableEq m] [Fintype m] (e : n ≃ m) (g : GL n R) : ↑(reindex e g)⁻¹ = (Matrix.reindex e e) g.inv

theorem Matrix.GL.conj_diagonal_apply {R : Type u_1} [CommRing R] {ι : Type u_6} [Fintype ι] [DecidableEq ι] (d : ι → Rˣ) (g : GL ι R) (i j : ι) : ↑((MulAut.conj (diagonal d)) g) i j = ↑(d i) * ↑(d j)⁻¹ * ↑g i j

theorem Matrix.GL.isMulCentral_diagonal {R : Type u_6} [CommRing R] {ι : Type u_7} [Fintype ι] [DecidableEq ι] (a : Rˣ) : IsMulCentral (diagonal fun (x : ι) => a)

theorem Matrix.GeneralLinearGroup.apply_ne_zero_of_isDiag {R : Type u_1} {n : Type u_2} [CommRing R] [DecidableEq n] [Fintype n] [Nontrivial R] (g : GL n R) (h : (↑g).IsDiag) (j : n) : ↑g j j ≠ 0

theorem Matrix.GeneralLinearGroup.coe_mul_inv {R : Type u_1} {n : Type u_2} [CommRing R] [DecidableEq n] [Fintype n] (g : GL n R) : ↑g * (↑g)⁻¹ = 1

theorem Matrix.GeneralLinearGroup.coe_inv_mul {R : Type u_1} {n : Type u_2} [CommRing R] [DecidableEq n] [Fintype n] (g : GL n R) : (↑g)⁻¹ * ↑g = 1

noncomputable def Matrix.GeneralLinearGroup.toBasis {ι : Type u_6} [DecidableEq ι] [Fintype ι] {K : Type u_7} [CommRing K] (g : GL ι K) : Module.Basis ι K (ι → K)

The columns of an invertible matrix over K yields a basis of ι → K.

Equations

• g.toBasis = Module.Basis.ofEquivFun (Matrix.GeneralLinearGroup.toLin g⁻¹).toLinearEquiv

@[simp]

theorem Matrix.GeneralLinearGroup.toBasis_coe_apply {ι : Type u_6} [DecidableEq ι] [Fintype ι] {K : Type u_7} [CommRing K] (g : GL ι K) (i : ι) : g.toBasis i = fun (j : ι) => ↑g j i

def Matrix.GeneralLinearGroup.toSubmodule {ι : Type u_6} [DecidableEq ι] [Fintype ι] {K : Type u_7} [CommRing K] {R : Subring K} (g : GL ι K) : Submodule (↥R) (ι → K)

From an invertible matrix over K, we obtain an R submodule by taking the span of the columns.

Equations

• g.toSubmodule = Submodule.span (↥R) (Set.range fun (col row : ι) => ↑g row col)

theorem Matrix.GeneralLinearGroup.mem_toSubmodule {ι : Type u_6} [DecidableEq ι] [Fintype ι] {K : Type u_7} [CommRing K] {R : Subring K} (g : GL ι K) (x : ι → K) : x ∈ g.toSubmodule ↔ ∃ (y : ι → ↥R), (↑g).mulVec (Subtype.val ∘ y) = x

@[implicit_reducible]

instance Matrix.GeneralLinearGroup.instSMulSubmoduleSubtypeMemSubringForallLeanPool {ι : Type u_6} [DecidableEq ι] [Fintype ι] {K : Type u_7} [CommRing K] {R : Subring K} : SMul (GL ι K) (Submodule (↥R) (ι → K))

Invertible matrices over K act on R-submodules of ι → K.

Equations

• One or more equations did not get rendered due to their size.

theorem Matrix.GeneralLinearGroup.smul_def {ι : Type u_6} [DecidableEq ι] [Fintype ι] {K : Type u_7} [CommRing K] {R : Subring K} (g : GL ι K) (M : Submodule (↥R) (ι → K)) : g • M = Submodule.map (↑↥R (↑g).mulVecLin) M

theorem Matrix.GeneralLinearGroup.mem_smul {ι : Type u_6} [DecidableEq ι] [Fintype ι] {K : Type u_7} [CommRing K] {R : Subring K} (g : GL ι K) (M : Submodule (↥R) (ι → K)) (x : ι → K) : x ∈ g • M ↔ ∃ y ∈ M, (↑g).mulVec y = x

theorem Matrix.GeneralLinearGroup.diagonal_smul {ι : Type u_6} [DecidableEq ι] [Fintype ι] {K : Type u_7} [CommRing K] {R : Subring K} (f : ι → Kˣ) (M : Submodule (↥R) (ι → K)) (hf : ∀ (i j : ι), f i = f j) (i : ι) : «GL».diagonal f • M = f i • M

@[implicit_reducible]

instance Matrix.GeneralLinearGroup.instMulActionSubmoduleSubtypeMemSubringForallLeanPool {ι : Type u_6} [DecidableEq ι] [Fintype ι] {K : Type u_7} [CommRing K] {R : Subring K} : MulAction (GL ι K) (Submodule (↥R) (ι → K))

Invertible matrices over K act on R-submodules of ι → K.

Equations

• One or more equations did not get rendered due to their size.

def Matrix.GeneralLinearGroup.equivSMulGL {ι : Type u_6} [DecidableEq ι] [Fintype ι] {K : Type u_7} [CommRing K] {R : Subring K} (g : GL ι K) (M : Submodule (↥R) (ι → K)) : ↥M ≃ₗ[↥R] ↥(g • M)

The canonical R-linear isomorphism from M to g • M induced by g.

Equations

• g.equivSMulGL M = (LinearEquiv.restrictScalars (↥R) (Matrix.GeneralLinearGroup.toLin g).toLinearEquiv).submoduleMap M

theorem Matrix.GeneralLinearGroup.smul_toSubmodule {ι : Type u_6} [DecidableEq ι] [Fintype ι] {K : Type u_7} [CommRing K] {R : Subring K} (g h : GL ι K) : g • h.toSubmodule = (g * h).toSubmodule

noncomputable def Matrix.GeneralLinearGroup.toLinearEquivOfBasis {ι : Type u_6} [DecidableEq ι] [Fintype ι] {R : Type u_8} {M : Type u_9} [CommRing R] [AddCommMonoid M] [Module R M] (b : Module.Basis ι R M) (g : GL ι R) : M ≃ₗ[R] M

The linear equivalence induced by a matrix in the coordinates of a basis.

Equations

• Matrix.GeneralLinearGroup.toLinearEquivOfBasis b g = (b.equivFun.trans (Matrix.GeneralLinearGroup.toLin g).toLinearEquiv).trans b.equivFun.symm

noncomputable def Matrix.GeneralLinearGroup.smulBasis {ι : Type u_6} [DecidableEq ι] [Fintype ι] {R : Type u_8} {M : Type u_9} [CommRing R] [AddCommMonoid M] [Module R M] (g : GL ι R) (b : Module.Basis ι R M) : Module.Basis ι R M

The basis obtained by acting on coordinates by a matrix in GL.

Equations

• g.smulBasis b = b.map (Matrix.GeneralLinearGroup.toLinearEquivOfBasis b g)

@[implicit_reducible]

noncomputable instance Matrix.GeneralLinearGroup.instSMulMulOppositeSubtypeMemSubringBasisForallSubmoduleLeanPool {ι : Type u_6} [DecidableEq ι] [Fintype ι] {K : Type u_7} [CommRing K] {R : Subring K} (M : Submodule (↥R) (ι → K)) : SMul (GL ι ↥R)ᵐᵒᵖ (Module.Basis ι ↥R ↥M)

Equations

• One or more equations did not get rendered due to their size.

theorem Matrix.GeneralLinearGroup.basis_smul_def {ι : Type u_6} [DecidableEq ι] [Fintype ι] {K : Type u_7} [CommRing K] {R : Subring K} {M : Submodule (↥R) (ι → K)} (g : GL ι ↥R) (b : Module.Basis ι ↥R ↥M) : MulOpposite.op g • b = g.smulBasis b

@[simp]

theorem Matrix.GeneralLinearGroup.ofLinearEquiv_toLinearEquiv {R : Type u_8} {M : Type u_9} [CommRing R] [AddCommMonoid M] [Module R M] (f : M ≃ₗ[R] M) : (LinearMap.GeneralLinearGroup.ofLinearEquiv f).toLinearEquiv = f

instance Matrix.GeneralLinearGroup.instIsPretransitiveMulOppositeSubtypeMemSubringBasisForallSubmodule_leanPool {ι : Type u_6} [DecidableEq ι] [Fintype ι] {K : Type u_7} [CommRing K] {R : Subring K} (M : Submodule (↥R) (ι → K)) : MulAction.IsPretransitive (GL ι ↥R)ᵐᵒᵖ (Module.Basis ι ↥R ↥M)

For fixed R-submodule M of ι → K, GL ι R acts transitively on ι-indexed R basis of M.

def Matrix.GeneralLinearGroup.embDiagonal (R : Type u_8) (ι : Type u_9) [CommRing R] [Fintype ι] [DecidableEq ι] : Rˣ →* GL ι R

The diagonal embedding from the units of R to the general linear group.

Equations

• Matrix.GeneralLinearGroup.embDiagonal R ι = { toFun := fun (x : Rˣ) => Matrix.GL.diagonal fun (x_1 : ι) => x, map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem Matrix.GeneralLinearGroup.embDiagonal_apply (R : Type u_8) (ι : Type u_9) [CommRing R] [Fintype ι] [DecidableEq ι] (x : Rˣ) : (embDiagonal R ι) x = «GL».diagonal fun (x_1 : ι) => x

theorem Matrix.GeneralLinearGroup.isMulCentral_embDiagonal {R : Type u_8} [CommRing R] {ι : Type u_9} [Fintype ι] [DecidableEq ι] (u : Rˣ) : IsMulCentral ((embDiagonal R ι) u)

def Matrix.GeneralLinearGroup.upperTriangularSubgroup (R : Type u_6) [CommRing R] (ι : Type u_7) [Fintype ι] [DecidableEq ι] [LinearOrder ι] : Subgroup (GL ι R)

The subgroup of GL(ι, R) consisting of upper triangular matrices (wrt. to the ordering on ι).

Equations

• Matrix.GeneralLinearGroup.upperTriangularSubgroup R ι = { carrier := {g : GL ι R | (↑g).BlockTriangular id}, mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }

@[simp]

theorem Matrix.GeneralLinearGroup.mem_upperTriangularSubgroup_iff (R : Type u_6) [CommRing R] (ι : Type u_7) [Fintype ι] [DecidableEq ι] [LinearOrder ι] (g : GL ι R) : g ∈ upperTriangularSubgroup R ι ↔ (↑g).BlockTriangular id

@[simp]

theorem Matrix.BlockTriangular.fin_two_iff {R : Type u_6} [Zero R] (M : Matrix (Fin 2) (Fin 2) R) : M.BlockTriangular id ↔ M 1 0 = 0