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

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

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
    source
    @[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) :
    ↑(Matrix.toLinearEquiv' P h) = Matrix.toLin' P
    source
    @[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) :
    ↑(LinearEquiv.symm (Matrix.toLinearEquiv' P h)) = Matrix.toLin' ⅟P
    source
    @[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 (Matrix.det A)) (a : M) :
    (Matrix.toLinearEquiv b A hA) a = ((Matrix.toLin b b) A) a
    source
    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 (Matrix.det A)) :
    M ≃ₗ[R] M

    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
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      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 (Matrix.det A)) :
      LinearMap.ker ((Matrix.toLin b b) A) = ⊥
      source
      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 (Matrix.det A)) :
      LinearMap.range ((Matrix.toLin b b) A) = ⊤
      source
      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 : n → K), v ≠ 0 ∧ Matrix.mulVec M v = 0) ↔ Matrix.det M = 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.

      source
      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 : n → A), v ≠ 0 ∧ Matrix.mulVec M v = 0) ↔ Matrix.det M = 0
      source
      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 : n → A), v ≠ 0 ∧ Matrix.mulVec M v = 0) ↔ Matrix.det M = 0
      source
      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 : n → A), v ≠ 0 ∧ Matrix.vecMul v M = 0) ↔ Matrix.det M = 0
      source
      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} :
      Matrix.Nondegenerate M ↔ Matrix.det M ≠ 0
      source
      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} :
      Matrix.Nondegenerate M → Matrix.det M ≠ 0

      Alias of the forward direction of Matrix.nondegenerate_iff_det_ne_zero.

      source
      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} :
      Matrix.det M ≠ 0 → Matrix.Nondegenerate M

      Alias of the reverse direction of Matrix.nondegenerate_iff_det_ne_zero.

      source
      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 < Finset.sum Finset.univ fun (i : n) => A i j) :
      Matrix.det A ≠ 0

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

      source
      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 < Finset.sum Finset.univ fun (j : n) => A i j) :
      Matrix.det A ≠ 0

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