Documentation

Mathlib.LinearAlgebra.Matrix.ToLinearEquiv

Matrices and linear equivalences #

This file gives the map Matrix.toLinearEquiv from matrices with invertible determinant, to linear equivs.

Main definitions #

Main results #

Tags #

matrix, linear_equiv, determinant, inverse

def Matrix.toLinearEquiv' {n : Type u_1} [Fintype n] {R : Type u_2} [CommRing R] [DecidableEq n] (P : Matrix n n R) :
Invertible P(nR) ≃ₗ[R] nR

An invertible matrix yields a linear equivalence from the free module to itself.

See Matrix.toLinearEquiv for the same map on arbitrary modules.

Equations
Instances For
    @[simp]
    theorem Matrix.toLinearEquiv'_apply {n : Type u_1} [Fintype n] {R : Type u_2} [CommRing R] [DecidableEq n] (P : Matrix n n R) (h : Invertible P) :
    (P.toLinearEquiv' h) = Matrix.toLin' P
    @[simp]
    theorem Matrix.toLinearEquiv'_symm_apply {n : Type u_1} [Fintype n] {R : Type u_2} [CommRing R] [DecidableEq n] (P : Matrix n n R) (h : Invertible P) :
    (P.toLinearEquiv' h).symm = Matrix.toLin' P
    @[simp]
    theorem Matrix.toLinearEquiv_apply {n : Type u_1} [Fintype n] {R : Type u_2} {M : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] (b : Basis n R M) [DecidableEq n] (A : Matrix n n R) (hA : IsUnit A.det) (a : M) :
    (Matrix.toLinearEquiv b A hA) a = ((Matrix.toLin b b) A) a
    noncomputable def Matrix.toLinearEquiv {n : Type u_1} [Fintype n] {R : Type u_2} {M : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] (b : Basis n R M) [DecidableEq n] (A : Matrix n n R) (hA : IsUnit A.det) :

    Given hA : IsUnit A.det and b : Basis R b, A.toLinearEquiv b hA is the LinearEquiv arising from toLin b b A.

    See Matrix.toLinearEquiv' for this result on n → R.

    Equations
    Instances For
      theorem Matrix.ker_toLin_eq_bot {n : Type u_1} [Fintype n] {R : Type u_2} {M : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] (b : Basis n R M) [DecidableEq n] (A : Matrix n n R) (hA : IsUnit A.det) :
      theorem Matrix.range_toLin_eq_top {n : Type u_1} [Fintype n] {R : Type u_2} {M : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] (b : Basis n R M) [DecidableEq n] (A : Matrix n n R) (hA : IsUnit A.det) :
      theorem Matrix.exists_mulVec_eq_zero_iff_aux {n : Type u_1} [Fintype n] {K : Type u_4} [DecidableEq n] [Field K] {M : Matrix n n K} :
      (∃ (v : nK), v 0 M.mulVec v = 0) M.det = 0

      This holds for all integral domains (see Matrix.exists_mulVec_eq_zero_iff), not just fields, but it's easier to prove it for the field of fractions first.

      theorem Matrix.exists_mulVec_eq_zero_iff' {n : Type u_1} [Fintype n] {A : Type u_4} (K : Type u_5) [DecidableEq n] [CommRing A] [Nontrivial A] [Field K] [Algebra A K] [IsFractionRing A K] {M : Matrix n n A} :
      (∃ (v : nA), v 0 M.mulVec v = 0) M.det = 0
      theorem Matrix.exists_mulVec_eq_zero_iff {n : Type u_1} [Fintype n] {A : Type u_4} [DecidableEq n] [CommRing A] [IsDomain A] {M : Matrix n n A} :
      (∃ (v : nA), v 0 M.mulVec v = 0) M.det = 0
      theorem Matrix.exists_vecMul_eq_zero_iff {n : Type u_1} [Fintype n] {A : Type u_4} [DecidableEq n] [CommRing A] [IsDomain A] {M : Matrix n n A} :
      (∃ (v : nA), v 0 Matrix.vecMul v M = 0) M.det = 0
      theorem Matrix.nondegenerate_iff_det_ne_zero {n : Type u_1} [Fintype n] {A : Type u_4} [DecidableEq n] [CommRing A] [IsDomain A] {M : Matrix n n A} :
      M.Nondegenerate M.det 0
      theorem Matrix.Nondegenerate.of_det_ne_zero {n : Type u_1} [Fintype n] {A : Type u_4} [DecidableEq n] [CommRing A] [IsDomain A] {M : Matrix n n A} :
      M.det 0M.Nondegenerate

      Alias of the reverse direction of Matrix.nondegenerate_iff_det_ne_zero.

      theorem Matrix.Nondegenerate.det_ne_zero {n : Type u_1} [Fintype n] {A : Type u_4} [DecidableEq n] [CommRing A] [IsDomain A] {M : Matrix n n A} :
      M.NondegenerateM.det 0

      Alias of the forward direction of Matrix.nondegenerate_iff_det_ne_zero.

      theorem Matrix.det_ne_zero_of_sum_col_pos {n : Type u_1} [Fintype n] [DecidableEq n] {S : Type u_2} [LinearOrderedCommRing S] {A : Matrix n n S} (h1 : Pairwise fun (i j : n) => A i j < 0) (h2 : ∀ (j : n), 0 < i : n, A i j) :
      A.det 0

      A matrix whose nondiagonal entries are negative with the sum of the entries of each column positive has nonzero determinant.

      theorem Matrix.det_ne_zero_of_sum_row_pos {n : Type u_1} [Fintype n] [DecidableEq n] {S : Type u_2} [LinearOrderedCommRing S] {A : Matrix n n S} (h1 : Pairwise fun (i j : n) => A i j < 0) (h2 : ∀ (i : n), 0 < j : n, A i j) :
      A.det 0

      A matrix whose nondiagonal entries are negative with the sum of the entries of each row positive has nonzero determinant.