Exact source: MathlibAnnex/LinearAlgebra/Matrix/MaximalMinorFactorization.lean
Pinned GitHub source · Raw UTF-8 source
Back to Almost-contractive linear recovery with exact volume scaling
1import MathlibAnnex.LinearAlgebra.Matrix.MaximalMinor2import Mathlib.LinearAlgebra.Matrix.NonsingularInverse3import Mathlib.Tactic45/-!6# Factorization from proportional oriented maximal minors78This candidate separates the sign-sensitive, ordered-row theorem from the9adapter to `MathlibAnnex.Matrix.maximalMinor`, whose indices use increasing row10order. The matrix convention is `source = target * factor`, corresponding to11`target ∘ factor = source` for column-vector linear maps.1213Canonical set-indexed minors are transported to arbitrary ordered row tuples14by sorting and a common determinant sign. Noninjective tuples are handled by15the repeated-row determinant theorem, and dimension zero is explicit.16-/1718noncomputable section1920open scoped Matrix2122namespace MathlibAnnex23namespace Matrix2425universe u v2627/-- Determinant of the square matrix obtained from an ordered tuple of rows.28The tuple is allowed to repeat rows; then the determinant vanishes. -/29def orientedMaximalMinor {n : ℕ} {ι : Type u} {R : Type v} [CommRing R]30 (A : _root_.Matrix ι (Fin n) R) (rows : Fin n → ι) : R :=31 (A.submatrix rows id).det3233/-- All ordered maximal minors of `source` equal `scale` times those of34`target`. Repeated-row tuples are included to make row replacement sign-free. -/35def OrientedMaximalMinorsProportional36 {n : ℕ} {ι : Type u} {R : Type v} [CommRing R]37 (source target : _root_.Matrix ι (Fin n) R) (scale : R) : Prop :=38 ∀ rows : Fin n → ι,39 orientedMaximalMinor source rows =40 scale * orientedMaximalMinor target rows4142/-- Canonical increasing-row maximal minors are pointwise proportional. -/43def MaximalMinorsProportional44 {n : ℕ} {ι : Type u} {R : Type v}45 [LinearOrder ι] [CommRing R]46 (source target : _root_.Matrix ι (Fin n) R) (scale : R) : Prop :=47 ∀ s : MaximalMinorIndex n ι,48 maximalMinor source s = scale * maximalMinor target s4950/-- The canonical order-embedding bridge converts a maximal-minor relation51at one increasing row tuple to the oriented convention without a sign. -/52theorem orientedMaximalMinor_eq_of_orderEmbedding53 {n : ℕ} {ι : Type u} {R : Type v}54 [LinearOrder ι] [CommRing R]55 (source target : _root_.Matrix ι (Fin n) R) (scale : R)56 (hminor : MaximalMinorsProportional source target scale)57 (rows : Fin n ↪o ι) :58 orientedMaximalMinor source rows =59 scale * orientedMaximalMinor target rows := by60 have h := hminor (MaximalMinorIndex.ofOrderEmbedding rows)61 change _root_.Matrix.det (fun i j => source (rows i) j) =62 scale * _root_.Matrix.det (fun i j => target (rows i) j)63 simpa only [maximalMinor_ofOrderEmbedding] using h6465/-- The square factor read from one selected target chart and the matching66source chart. -/67def chartFactor {n : ℕ} {ι : Type u} {K : Type v} [Field K]68 (target source : _root_.Matrix ι (Fin n) K) (rows : Fin n → ι) :69 _root_.Matrix (Fin n) (Fin n) K :=70 (target.submatrix rows id)⁻¹ * source.submatrix rows id7172/-- Replacing one entry of the row tuple is the same as updating that row of73its selected square matrix. -/74theorem submatrix_update_rowTuple75 {n : ℕ} {ι : Type u} {R : Type v} [CommRing R]76 (A : _root_.Matrix ι (Fin n) R) (rows : Fin n → ι)77 (j : Fin n) (i : ι) :78 A.submatrix (Function.update rows j i) id =79 (A.submatrix rows id).updateRow j (A i) := by80 ext k l81 by_cases hkj : k = j82 · subst k83 simp84 · simp [hkj]8586/-- Cramer's rule in the row convention: replacement determinants are the87selected determinant times the coordinates of the new row. -/88theorem det_smul_vecMul_nonsingInv_eq_updateRowDet89 {n : ℕ} {K : Type v} [Field K]90 (A : _root_.Matrix (Fin n) (Fin n) K) (r : Fin n → K)91 (hA : A.det ≠ 0) :92 A.det • (r ᵥ* A⁻¹) = fun j => (A.updateRow j r).det := by93 have hunit : IsUnit A.det := (isUnit_iff_ne_zero).2 hA94 funext j95 simpa only [Pi.smul_apply, _root_.Matrix.cramer_transpose_apply] using96 congrFun97 (_root_.Matrix.det_smul_inv_vecMul_eq_cramer_transpose A r hunit) j9899/-- The selected target rows composed with the chart factor are exactly the100selected source rows. -/101theorem selectedSubmatrix_mul_chartFactor102 {n : ℕ} {ι : Type u} {K : Type v} [Field K]103 (target source : _root_.Matrix ι (Fin n) K) (rows : Fin n → ι)104 (htarget : orientedMaximalMinor target rows ≠ 0) :105 target.submatrix rows id * chartFactor target source rows =106 source.submatrix rows id := by107 have hdet : (target.submatrix rows id).det ≠ 0 := by108 simpa [orientedMaximalMinor] using htarget109 have hunit : IsUnit (target.submatrix rows id).det :=110 (isUnit_iff_ne_zero).2 hdet111 simp only [chartFactor]112 rw [← _root_.Matrix.mul_assoc,113 _root_.Matrix.mul_nonsing_inv _ hunit,114 _root_.Matrix.one_mul]115116/-- The determinant of the chart factor is the proportionality scalar. -/117theorem det_chartFactor118 {n : ℕ} {ι : Type u} {K : Type v} [Field K]119 (target source : _root_.Matrix ι (Fin n) K) (rows : Fin n → ι)120 (scale : K)121 (htarget : orientedMaximalMinor target rows ≠ 0)122 (hbase : orientedMaximalMinor source rows =123 scale * orientedMaximalMinor target rows) :124 (chartFactor target source rows).det = scale := by125 have hmatrix := selectedSubmatrix_mul_chartFactor target source rows htarget126 have hdet := congrArg _root_.Matrix.det hmatrix127 rw [_root_.Matrix.det_mul] at hdet128 apply mul_left_cancel₀ htarget129 calc130 orientedMaximalMinor target rows * (chartFactor target source rows).det =131 orientedMaximalMinor source rows := by132 simpa [orientedMaximalMinor] using hdet133 _ = scale * orientedMaximalMinor target rows := hbase134 _ = orientedMaximalMinor target rows * scale := by ac_rfl135136/-- Equality of all ordered maximal minors gives equality of the row137coordinates relative to the selected source and target charts. -/138theorem rowCoordinates_eq_of_orientedMaximalMinorsProportional139 {n : ℕ} {ι : Type u} {K : Type v} [Field K]140 (source target : _root_.Matrix ι (Fin n) K) (scale : K)141 (hscale : scale ≠ 0)142 (hminor : OrientedMaximalMinorsProportional source target scale)143 (rows : Fin n → ι)144 (htarget : orientedMaximalMinor target rows ≠ 0)145 (i : ι) :146 source i ᵥ* (source.submatrix rows id)⁻¹ =147 target i ᵥ* (target.submatrix rows id)⁻¹ := by148 let S : _root_.Matrix (Fin n) (Fin n) K := source.submatrix rows id149 let T : _root_.Matrix (Fin n) (Fin n) K := target.submatrix rows id150 have hbase : S.det = scale * T.det := by151 simpa [S, T, orientedMaximalMinor] using hminor rows152 have hT : T.det ≠ 0 := by153 simpa [T, orientedMaximalMinor] using htarget154 have hS : S.det ≠ 0 := by155 rw [hbase]156 exact mul_ne_zero hscale hT157 have hsource := det_smul_vecMul_nonsingInv_eq_updateRowDet S (source i) hS158 have htargetC := det_smul_vecMul_nonsingInv_eq_updateRowDet T (target i) hT159 funext j160 have hreplace := hminor (Function.update rows j i)161 have hrep : (S.updateRow j (source i)).det =162 scale * (T.updateRow j (target i)).det := by163 simpa [S, T, orientedMaximalMinor, submatrix_update_rowTuple] using hreplace164 have hleft : S.det * (source i ᵥ* S⁻¹) j =165 (S.updateRow j (source i)).det := by166 simpa only [Pi.smul_apply, smul_eq_mul] using congrFun hsource j167 have hright : T.det * (target i ᵥ* T⁻¹) j =168 (T.updateRow j (target i)).det := by169 simpa only [Pi.smul_apply, smul_eq_mul] using congrFun htargetC j170 apply mul_left_cancel₀ hS171 calc172 S.det * (source i ᵥ* S⁻¹) j =173 (S.updateRow j (source i)).det := hleft174 _ = scale * (T.updateRow j (target i)).det := hrep175 _ = scale * (T.det * (target i ᵥ* T⁻¹) j) := by rw [← hright]176 _ = (scale * T.det) * (target i ᵥ* T⁻¹) j := by ac_rfl177 _ = S.det * (target i ᵥ* T⁻¹) j := by rw [hbase]178179/-- A nonzero proportionality scalar and one nonzero target chart force the180rectangular factorization `target * factor = source`. -/181theorem mul_chartFactor_eq_of_orientedMaximalMinorsProportional182 {n : ℕ} {ι : Type u} {K : Type v} [Field K]183 (source target : _root_.Matrix ι (Fin n) K) (scale : K)184 (hscale : scale ≠ 0)185 (hminor : OrientedMaximalMinorsProportional source target scale)186 (rows : Fin n → ι)187 (htarget : orientedMaximalMinor target rows ≠ 0) :188 target * chartFactor target source rows = source := by189 ext i j190 have hcoord := rowCoordinates_eq_of_orientedMaximalMinorsProportional191 source target scale hscale hminor rows htarget i192 have hsource : orientedMaximalMinor source rows ≠ 0 := by193 rw [hminor rows]194 exact mul_ne_zero hscale htarget195 have hsourceDet : (source.submatrix rows id).det ≠ 0 := by196 simpa [orientedMaximalMinor] using hsource197 have hsourceUnit : IsUnit (source.submatrix rows id).det :=198 (isUnit_iff_ne_zero).2 hsourceDet199 calc200 (target * chartFactor target source rows) i j =201 (target i ᵥ* chartFactor target source rows) j := rfl202 _ = ((target i ᵥ* (target.submatrix rows id)⁻¹) ᵥ*203 source.submatrix rows id) j := by204 rw [chartFactor, ← _root_.Matrix.vecMul_vecMul]205 _ = ((source i ᵥ* (source.submatrix rows id)⁻¹) ᵥ*206 source.submatrix rows id) j := by rw [hcoord]207 _ = (source i ᵥ*208 ((source.submatrix rows id)⁻¹ * source.submatrix rows id)) j := by209 rw [_root_.Matrix.vecMul_vecMul]210 _ = source i j := by211 rw [_root_.Matrix.nonsing_inv_mul _ hsourceUnit,212 _root_.Matrix.vecMul_one]213214/-- The chart factor is the unique square matrix factoring `source` through a215rectangular `target` with a nonzero selected chart. -/216theorem chartFactor_unique217 {n : ℕ} {ι : Type u} {K : Type v} [Field K]218 (target source : _root_.Matrix ι (Fin n) K) (rows : Fin n → ι)219 (htarget : orientedMaximalMinor target rows ≠ 0)220 (L : _root_.Matrix (Fin n) (Fin n) K)221 (hL : target * L = source) :222 L = chartFactor target source rows := by223 have hdet : (target.submatrix rows id).det ≠ 0 := by224 simpa [orientedMaximalMinor] using htarget225 have hunit : IsUnit (target.submatrix rows id).det :=226 (isUnit_iff_ne_zero).2 hdet227 have hselected : target.submatrix rows id * L = source.submatrix rows id := by228 calc229 target.submatrix rows id * L = (target * L).submatrix rows id := by230 simpa using231 (_root_.Matrix.submatrix_mul target L rows id id Function.bijective_id).symm232 _ = source.submatrix rows id := by rw [hL]233 calc234 L = 1 * L := by rw [_root_.Matrix.one_mul]235 _ = ((target.submatrix rows id)⁻¹ * target.submatrix rows id) * L := by236 rw [_root_.Matrix.nonsing_inv_mul _ hunit]237 _ = (target.submatrix rows id)⁻¹ *238 (target.submatrix rows id * L) := by239 rw [_root_.Matrix.mul_assoc]240 _ = (target.submatrix rows id)⁻¹ * source.submatrix rows id := by241 rw [hselected]242 _ = chartFactor target source rows := rfl243244/-- Combined existence, determinant, and uniqueness statement. It includes245`n = 0`: then the oriented-minor hypothesis forces `scale = 1`. -/246theorem existsUnique_factor_of_orientedMaximalMinorsProportional247 {n : ℕ} {ι : Type u} {K : Type v} [Field K]248 (source target : _root_.Matrix ι (Fin n) K) (scale : K)249 (hscale : scale ≠ 0)250 (hminor : OrientedMaximalMinorsProportional source target scale)251 (rows : Fin n → ι)252 (htarget : orientedMaximalMinor target rows ≠ 0) :253 ∃! L : _root_.Matrix (Fin n) (Fin n) K,254 target * L = source ∧ L.det = scale := by255 refine ⟨chartFactor target source rows, ?_, ?_⟩256 · constructor257 · exact mul_chartFactor_eq_of_orientedMaximalMinorsProportional258 source target scale hscale hminor rows htarget259 · exact det_chartFactor target source rows scale htarget (hminor rows)260 · intro L hL261 exact chartFactor_unique target source rows htarget L hL.1262263/-- A permutation of the ordered rows contributes its determinant sign. -/264theorem orientedMaximalMinor_permute265 {n : ℕ} {ι : Type u} {R : Type v} [CommRing R]266 (A : _root_.Matrix ι (Fin n) R) (rows : Fin n → ι)267 (σ : Equiv.Perm (Fin n)) :268 orientedMaximalMinor A (rows ∘ σ) =269 (Equiv.Perm.sign σ : R) * orientedMaximalMinor A rows := by270 exact _root_.Matrix.det_permute σ (A.submatrix rows id)271272/-- Noninjective row tuples give zero determinants, including repeated rows. -/273theorem orientedMaximalMinor_eq_zero_of_not_injective274 {n : ℕ} {ι : Type u} {R : Type v} [CommRing R]275 (A : _root_.Matrix ι (Fin n) R) (rows : Fin n → ι)276 (hrows : ¬ Function.Injective rows) : orientedMaximalMinor A rows = 0 := by277 classical278 obtain ⟨i, j, hij, hne⟩ := Function.not_injective_iff.mp hrows279 exact _root_.Matrix.det_zero_of_row_eq hne (by280 change A (rows i) = A (rows j)281 rw [hij])282283/-- Sorting an injective tuple gives an increasing embedding and a permutation.284The proof also covers the unique tuple in dimension zero. -/285theorem exists_orderEmbedding_perm_of_injective286 {n : ℕ} {ι : Type u} [LinearOrder ι]287 (rows : Fin n → ι) (hrows : Function.Injective rows) :288 ∃ (sorted : Fin n ↪o ι) (σ : Equiv.Perm (Fin n)),289 rows = sorted ∘ σ := by290 classical291 let s : Finset ι := Finset.univ.image rows292 have hcard : s.card = n := by293 simpa [s] using Finset.card_image_of_injective Finset.univ hrows294 let e := s.orderIsoOfFin hcard295 let p : Fin n → Fin n := fun i => e.symm ⟨rows i, by simp [s]⟩296 have hp : ∀ i, s.orderEmbOfFin hcard (p i) = rows i := by297 intro i298 exact congrArg Subtype.val (e.apply_symm_apply ⟨rows i, by simp [s]⟩)299 have hpinj : Function.Injective p := by300 intro i j hij301 apply hrows302 rw [← hp i, ← hp j, hij]303 let σ : Equiv.Perm (Fin n) := Equiv.ofBijective p304 ((Finite.injective_iff_bijective).mp hpinj)305 refine ⟨s.orderEmbOfFin hcard, σ, ?_⟩306 funext i307 exact (hp i).symm308309/-- Canonical increasing-row proportionality determines every ordered minor.310Both matrices use the same permutation sign; repeated rows vanish separately. -/311theorem orientedMaximalMinorsProportional_of_maximalMinorsProportional312 {n : ℕ} {ι : Type u} {R : Type v} [LinearOrder ι] [CommRing R]313 (source target : _root_.Matrix ι (Fin n) R) (scale : R)314 (hminor : MaximalMinorsProportional source target scale) :315 OrientedMaximalMinorsProportional source target scale := by316 classical317 intro rows318 by_cases hinj : Function.Injective rows319 · obtain ⟨sorted, σ, rfl⟩ := exists_orderEmbedding_perm_of_injective rows hinj320 rw [orientedMaximalMinor_permute, orientedMaximalMinor_permute,321 orientedMaximalMinor_eq_of_orderEmbedding source target scale hminor sorted]322 ring323 · rw [orientedMaximalMinor_eq_zero_of_not_injective source rows hinj,324 orientedMaximalMinor_eq_zero_of_not_injective target rows hinj, mul_zero]325326/-- Empty determinants equal one, so the zero-dimensional scale equals one. -/327theorem scale_eq_one_of_orientedMaximalMinorsProportional_zero328 {ι : Type u} {R : Type v} [CommRing R]329 (source target : _root_.Matrix ι (Fin 0) R) (scale : R)330 (hminor : OrientedMaximalMinorsProportional source target scale) :331 scale = 1 := by332 have h := hminor Fin.elim0333 simpa [orientedMaximalMinor] using h.symm334335/-- A nonzero chart and nonzero canonical minor scale recover the right factor. -/336theorem mul_chartFactor_eq_of_maximalMinorsProportional337 {n : ℕ} {ι : Type u} {K : Type v} [LinearOrder ι] [Field K]338 (source target : _root_.Matrix ι (Fin n) K) (scale : K)339 (hscale : scale ≠ 0) (hminor : MaximalMinorsProportional source target scale)340 (rows : Fin n → ι) (htarget : orientedMaximalMinor target rows ≠ 0) :341 target * chartFactor target source rows = source :=342 mul_chartFactor_eq_of_orientedMaximalMinorsProportional source target scale hscale343 (orientedMaximalMinorsProportional_of_maximalMinorsProportional344 source target scale hminor) rows htarget345346/-- The recovered factor is a unit when its minor scale is nonzero. -/347theorem isUnit_chartFactor_of_scale_ne_zero348 {n : ℕ} {ι : Type u} {K : Type v} [Field K]349 (target source : _root_.Matrix ι (Fin n) K) (rows : Fin n → ι) (scale : K)350 (htarget : orientedMaximalMinor target rows ≠ 0) (hscale : scale ≠ 0)351 (hbase : orientedMaximalMinor source rows = scale * orientedMaximalMinor target rows) :352 IsUnit (chartFactor target source rows) := by353 apply (_root_.Matrix.isUnit_iff_isUnit_det _).mpr354 rw [det_chartFactor target source rows scale htarget hbase]355 exact isUnit_iff_ne_zero.mpr hscale356357end Matrix358end MathlibAnnex