Exact source: MathlibAnnex/LinearAlgebra/Matrix/MaximalMinor.lean
Pinned GitHub source · Raw UTF-8 source
Back to A unique right factor from proportional oriented maximal minors
1import Mathlib.LinearAlgebra.Matrix.Determinant.Basic2import Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Basic3import Mathlib.LinearAlgebra.Matrix.ToLin4import Mathlib.Order.Hom.PowersetCard5import Mathlib.Topology.Algebra.Module.FiniteDimension6import Mathlib.Topology.Instances.Matrix7import Mathlib.Tactic89/-!10# Maximal minors selected by ordered rows1112A maximal minor of a matrix with `n` columns is obtained by choosing `n` rows.13A finite set of rows does not itself determine the sign of the determinant, so14`MaximalMinorIndex.orderedRows` uses the increasing order on the row type.1516The basic algebra is stated over a commutative ring and for an arbitrary linearly17ordered row type. The bridge from an order embedding is included because it is18the sign-sensitive interface needed by consumers that already carry ordered rows.19-/2021noncomputable section2223open scoped BigOperators2425namespace MathlibAnnex26namespace Matrix2728universe u v2930/-- An `n`-element set of rows, used to index maximal minors of an `n`-column matrix. -/31abbrev MaximalMinorIndex (n : ℕ) (ι : Type u) [LinearOrder ι] : Type u :=32 ↥(Set.powersetCard ι n)3334namespace MaximalMinorIndex3536/-- The increasing enumeration of the rows in a maximal-minor index. -/37def orderedRows {n : ℕ} {ι : Type u} [LinearOrder ι]38 (s : MaximalMinorIndex n ι) : Fin n ↪o ι :=39 Set.powersetCard.ofFinEmbEquiv.symm s4041/-- The row set underlying an order embedding. -/42noncomputable def ofOrderEmbedding {n : ℕ} {ι : Type u} [LinearOrder ι]43 (ρ : Fin n ↪o ι) : MaximalMinorIndex n ι :=44 Set.powersetCard.ofFinEmbEquiv ρ4546/-- Canonical increasing enumeration recovers the original order embedding. -/47@[simp] theorem orderedRows_ofOrderEmbedding {n : ℕ} {ι : Type u} [LinearOrder ι]48 (ρ : Fin n ↪o ι) :49 orderedRows (ofOrderEmbedding ρ) = ρ := by50 exact Set.powersetCard.ofFinEmbEquiv.symm_apply_apply ρ5152end MaximalMinorIndex5354/-- The square submatrix obtained from an `n`-element row set in increasing order. -/55def maximalSubmatrix {n : ℕ} {ι : Type u} {R : Type v} [LinearOrder ι]56 (A : _root_.Matrix ι (Fin n) R) (s : MaximalMinorIndex n ι) :57 _root_.Matrix (Fin n) (Fin n) R :=58 A.submatrix s.orderedRows id5960/-- The determinant of a maximal submatrix. -/61def maximalMinor {n : ℕ} {ι : Type u} {R : Type v} [LinearOrder ι] [CommRing R]62 (A : _root_.Matrix ι (Fin n) R) (s : MaximalMinorIndex n ι) : R :=63 (maximalSubmatrix A s).det6465/-- The family of all maximal minors, with the canonical increasing-row sign convention. -/66def maximalMinors {n : ℕ} {ι : Type u} {R : Type v} [LinearOrder ι] [CommRing R]67 (A : _root_.Matrix ι (Fin n) R) : MaximalMinorIndex n ι → R :=68 fun s => maximalMinor A s6970/-- The maximal submatrix associated with an order embedding has exactly those rows. -/71@[simp] theorem maximalSubmatrix_ofOrderEmbedding72 {n : ℕ} {ι : Type u} {R : Type v} [LinearOrder ι]73 (A : _root_.Matrix ι (Fin n) R) (ρ : Fin n ↪o ι) :74 maximalSubmatrix A (MaximalMinorIndex.ofOrderEmbedding ρ) =75 fun i j => A (ρ i) j := by76 ext i j77 simp [maximalSubmatrix]7879/-- The maximal minor associated with an order embedding is the determinant of its row matrix. -/80@[simp] theorem maximalMinor_ofOrderEmbedding81 {n : ℕ} {ι : Type u} {R : Type v} [LinearOrder ι] [CommRing R]82 (A : _root_.Matrix ι (Fin n) R) (ρ : Fin n ↪o ι) :83 maximalMinor A (MaximalMinorIndex.ofOrderEmbedding ρ) =84 _root_.Matrix.det (fun i j => A (ρ i) j) := by85 rw [maximalMinor, maximalSubmatrix_ofOrderEmbedding]8687/-- Selecting rows commutes with multiplication by a square right factor. -/88theorem maximalSubmatrix_mul89 {n : ℕ} {ι : Type u} {R : Type v} [LinearOrder ι] [Semiring R]90 (A : _root_.Matrix ι (Fin n) R)91 (L : _root_.Matrix (Fin n) (Fin n) R)92 (s : MaximalMinorIndex n ι) :93 maximalSubmatrix (A * L) s = maximalSubmatrix A s * L := by94 ext i j95 simp [maximalSubmatrix, _root_.Matrix.mul_apply]9697/-- A square right factor contributes its determinant to every maximal minor. -/98theorem maximalMinor_mul99 {n : ℕ} {ι : Type u} {R : Type v} [LinearOrder ι] [CommRing R]100 (A : _root_.Matrix ι (Fin n) R)101 (L : _root_.Matrix (Fin n) (Fin n) R)102 (s : MaximalMinorIndex n ι) :103 maximalMinor (A * L) s = maximalMinor A s * L.det := by104 rw [maximalMinor, maximalSubmatrix_mul, _root_.Matrix.det_mul]105 rfl106107/-- Vector form of maximal-minor scaling by a square right factor. -/108theorem maximalMinors_mul109 {n : ℕ} {ι : Type u} {R : Type v} [LinearOrder ι] [CommRing R]110 (A : _root_.Matrix ι (Fin n) R)111 (L : _root_.Matrix (Fin n) (Fin n) R) :112 maximalMinors (A * L) = L.det • maximalMinors A := by113 ext s114 simp [maximalMinors, maximalMinor_mul, mul_comm]115116/-- Scalar multiplication scales every maximal minor by the `n`th power. -/117theorem maximalMinors_smul118 {n : ℕ} {ι : Type u} {R : Type v} [LinearOrder ι] [CommRing R]119 (c : R) (A : _root_.Matrix ι (Fin n) R) :120 maximalMinors (c • A) = c ^ n • maximalMinors A := by121 ext s122 change _root_.Matrix.det (maximalSubmatrix (c • A) s) =123 c ^ n * _root_.Matrix.det (maximalSubmatrix A s)124 have hsel : maximalSubmatrix (c • A) s = c • maximalSubmatrix A s := by125 ext i j126 rfl127 rw [hsel]128 simp129130@[simp] theorem maximalSubmatrix_zero131 {n : ℕ} {ι : Type u} {R : Type v} [LinearOrder ι] [Zero R]132 (s : MaximalMinorIndex n ι) :133 maximalSubmatrix (0 : _root_.Matrix ι (Fin n) R) s = 0 := by134 ext i j135 rfl136137/-- The empty determinant is `1`, so the zero-minor formula requires positive size. -/138@[simp] theorem maximalMinor_zero_of_pos139 {n : ℕ} {ι : Type u} {R : Type v} [LinearOrder ι] [CommRing R]140 (hn : 0 < n) (s : MaximalMinorIndex n ι) :141 maximalMinor (0 : _root_.Matrix ι (Fin n) R) s = 0 := by142 letI : Nonempty (Fin n) := ⟨⟨0, hn⟩⟩143 unfold maximalMinor144 rw [maximalSubmatrix_zero]145 exact _root_.Matrix.det_zero (inferInstance : Nonempty (Fin n))146147@[simp] theorem maximalMinors_zero_of_pos148 {n : ℕ} {ι : Type u} {R : Type v} [LinearOrder ι] [CommRing R]149 (hn : 0 < n) :150 maximalMinors (0 : _root_.Matrix ι (Fin n) R) = 0 := by151 funext s152 simp [maximalMinors, maximalMinor_zero_of_pos hn]153154/-- Selecting the rows of a maximal submatrix commutes with matrix-vector multiplication. -/155theorem maximalSubmatrix_mulVec156 {n : ℕ} {ι : Type u} {R : Type v} [LinearOrder ι] [Semiring R]157 (A : _root_.Matrix ι (Fin n) R) (s : MaximalMinorIndex n ι)158 (x : Fin n → R) :159 (maximalSubmatrix A s).mulVec x =160 fun i => A.mulVec x (s.orderedRows i) := by161 funext i162 simp [maximalSubmatrix, _root_.Matrix.mulVec]163164/-- One nonzero maximal minor implies injectivity of matrix-vector multiplication. -/165theorem mulVec_injective_of_maximalMinor_ne_zero166 {n : ℕ} {ι : Type u} {K : Type v} [LinearOrder ι] [Field K]167 (A : _root_.Matrix ι (Fin n) K) (s : MaximalMinorIndex n ι)168 (hs : maximalMinor A s ≠ 0) :169 Function.Injective A.mulVec := by170 let g : _root_.Matrix.GeneralLinearGroup (Fin n) K :=171 _root_.Matrix.GeneralLinearGroup.mkOfDetNeZero (maximalSubmatrix A s) hs172 intro x y hxy173 apply (_root_.Matrix.GeneralLinearGroup.toLin g).toLinearEquiv.injective174 change (maximalSubmatrix A s).mulVec x = (maximalSubmatrix A s).mulVec y175 rw [maximalSubmatrix_mulVec, maximalSubmatrix_mulVec]176 funext i177 exact congrFun hxy (s.orderedRows i)178179/-- All maximal minors vary continuously with the matrix entries over `ℝ`. -/180theorem continuous_maximalMinors181 {n : ℕ} {ι : Type u} [LinearOrder ι] :182 Continuous183 (maximalMinors : _root_.Matrix ι (Fin n) ℝ → MaximalMinorIndex n ι → ℝ) := by184 apply continuous_pi185 intro s186 change Continuous fun A : _root_.Matrix ι (Fin n) ℝ =>187 _root_.Matrix.det (maximalSubmatrix A s)188 apply Continuous.matrix_det189 apply continuous_matrix190 intro i j191 change Continuous fun A : _root_.Matrix ι (Fin n) ℝ => A (s.orderedRows i) j192 exact continuous_apply_apply _ _193194end Matrix195end MathlibAnnex