|
| 1 | +/- |
| 2 | +Copyright (c) 2026 Weiyi Wang. All rights reserved. |
| 3 | +Released under Apache 2.0 license as described in the file LICENSE. |
| 4 | +Authors: Weiyi Wang |
| 5 | +-/ |
| 6 | +module |
| 7 | + |
| 8 | +public import Mathlib.Analysis.InnerProductSpace.Adjoint |
| 9 | +public import Mathlib.Analysis.InnerProductSpace.GramMatrix |
| 10 | +import Mathlib.Analysis.Matrix.Order |
| 11 | + |
| 12 | +/-! |
| 13 | +# Normed determinant of a linear map |
| 14 | +
|
| 15 | +Given a rectangular matrix $T$, it is common to talk about $\sqrt{det(T^{H}T)}$, where $T^{H}$ is |
| 16 | +the conjugate transpose of $T$, as a generalization to the determinant of a square matrix. It is the |
| 17 | +$m$-dimensional volume factor for $\mathbb{R}^m \to \mathbb{R}^n$. It is given various names in |
| 18 | +literature: |
| 19 | +* "Jacobian" (definition 3.4 of [lawrenceronald2025]), in the context of volume factor |
| 20 | + for non-linear map. However, we choose to reserve this name for the matrix consists of |
| 21 | + derivatives. |
| 22 | +* "Gram determinant", which is already used by `Matrix.gram`, and it is often referring to the |
| 23 | + $det(T^{H}T)$ without the square root. |
| 24 | +* "Nonnegative determinant" (definition 1 of [haruoyoshiohidetoki2006]). |
| 25 | +
|
| 26 | +Without a standardized name, we give a descriptive name `LinearMap.normDet` to reflect its |
| 27 | +definition and show that it is a generalization of `‖(f : LinearMap 𝕜 U U).det‖` |
| 28 | +(See `LinearMap.normDet_eq_norm_det`). We also construct this on linear maps between inner product |
| 29 | +spaces instead of matrices, and allow the codomain to have infinite dimension. |
| 30 | +
|
| 31 | +## Main definition |
| 32 | +* `LinearMap.normDet` : the norm determinant of a linear map. |
| 33 | +
|
| 34 | +## Main result |
| 35 | +* `ContinuousLinearMap.normDet_sq` and `LinearMap.normDet_sq`: The square of `f.normDet` |
| 36 | + equals to the determinant of `f.adjoint ∘ₗ f`. |
| 37 | +
|
| 38 | +## TODO |
| 39 | +
|
| 40 | +Show that `LinearMap.normDet` is the product of all singular values of the map. |
| 41 | +-/ |
| 42 | + |
| 43 | +public section |
| 44 | + |
| 45 | +namespace LinearMap |
| 46 | + |
| 47 | +variable {𝕜 U V : Type*} [RCLike 𝕜] [NormedAddCommGroup U] [InnerProductSpace 𝕜 U] |
| 48 | + [FiniteDimensional 𝕜 U] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] |
| 49 | + |
| 50 | +open Classical in |
| 51 | +/-- |
| 52 | +The norm determinant of a linear map `f : U →ₗ[𝕜] V` is defined as the norm of the determinant of |
| 53 | +the square matrix from `U →ₗ[𝕜] f.range` using a pair of orthonormal basis of equal dimensions. |
| 54 | +(See `LinearMap.normDet_eq` for using arbitrary orthonormal basis) |
| 55 | +
|
| 56 | +If such basis doesn't exist (i.e. the map is not injective), the norm determinant is zero. |
| 57 | +(See `LinearMap.normDet_eq_zero_iff_ker_ne_bot`) |
| 58 | +-/ |
| 59 | +noncomputable def normDet (f : U →ₗ[𝕜] V) : ℝ := |
| 60 | + if h : Nonempty (OrthonormalBasis (Fin (Module.finrank 𝕜 U)) 𝕜 f.range) then |
| 61 | + ‖(f.rangeRestrict.toMatrix (stdOrthonormalBasis 𝕜 U).toBasis h.some.toBasis).det‖ |
| 62 | + else |
| 63 | + 0 |
| 64 | + |
| 65 | +theorem normDet_nonneg (f : U →ₗ[𝕜] V) : 0 ≤ f.normDet := by |
| 66 | + unfold normDet |
| 67 | + split <;> simp |
| 68 | + |
| 69 | +/-- |
| 70 | +`LinearMap.normDet` is well-defined under any pair of orthonormal basis. |
| 71 | +-/ |
| 72 | +theorem normDet_eq {ι : Type*} [Fintype ι] [DecidableEq ι] (f : U →ₗ[𝕜] V) |
| 73 | + (bu : OrthonormalBasis ι 𝕜 U) (bv : OrthonormalBasis ι 𝕜 f.range) : |
| 74 | + f.normDet = ‖(f.rangeRestrict.toMatrix bu.toBasis bv.toBasis).det‖ := by |
| 75 | + have hrank : Module.finrank 𝕜 U = Module.finrank 𝕜 f.range := by |
| 76 | + rw [Module.finrank_eq_nat_card_basis bu.toBasis, Module.finrank_eq_nat_card_basis bv.toBasis] |
| 77 | + have h : Nonempty (OrthonormalBasis (Fin (Module.finrank 𝕜 U)) 𝕜 f.range) := by |
| 78 | + rw [hrank] |
| 79 | + exact ⟨stdOrthonormalBasis 𝕜 f.range⟩ |
| 80 | + simp only [normDet, h, ↓reduceDIte] |
| 81 | + rw [← basis_toMatrix_mul_linearMap_toMatrix_mul_basis_toMatrix (stdOrthonormalBasis 𝕜 U).toBasis |
| 82 | + bu.toBasis h.some.toBasis bv.toBasis] |
| 83 | + have h1 : bu.toBasis.toMatrix (stdOrthonormalBasis 𝕜 U).toBasis * |
| 84 | + (stdOrthonormalBasis 𝕜 U).toBasis.toMatrix bu.toBasis = 1 := |
| 85 | + Module.Basis.toMatrix_mul_toMatrix_flip _ _ |
| 86 | + have h2 : (stdOrthonormalBasis 𝕜 U).toBasis.toMatrix bu.toBasis * |
| 87 | + bu.toBasis.toMatrix (stdOrthonormalBasis 𝕜 U).toBasis = 1 := |
| 88 | + Module.Basis.toMatrix_mul_toMatrix_flip _ _ |
| 89 | + rw [← Matrix.det_comm' h1 h2, ← Matrix.mul_assoc, Matrix.det_mul, norm_mul] |
| 90 | + suffices ‖(bu.toBasis.toMatrix (stdOrthonormalBasis 𝕜 U).toBasis * |
| 91 | + h.some.toBasis.toMatrix ⇑bv.toBasis).det‖ = 1 by |
| 92 | + rw [this] |
| 93 | + simp |
| 94 | + apply CStarRing.norm_of_mem_unitary |
| 95 | + apply Matrix.det_of_mem_unitary |
| 96 | + rw [Matrix.mem_unitaryGroup_iff, Matrix.star_eq_conjTranspose, Matrix.conjTranspose_mul, |
| 97 | + ← Matrix.mul_assoc, Matrix.mul_assoc (bu.toBasis.toMatrix (stdOrthonormalBasis 𝕜 U).toBasis)] |
| 98 | + simp |
| 99 | + |
| 100 | +/-- |
| 101 | +`LinearMap.normDet` vanishes iff the map is not injective. |
| 102 | +-/ |
| 103 | +theorem normDet_eq_zero_iff_ker_ne_bot (f : U →ₗ[𝕜] V) : |
| 104 | + f.normDet = 0 ↔ f.ker ≠ ⊥ where |
| 105 | + mp h := by |
| 106 | + contrapose! h |
| 107 | + let g : U ≃ₗ[𝕜] f.range := LinearEquiv.ofBijective f.rangeRestrict |
| 108 | + ⟨by simpa using ker_eq_bot.mp h, f.surjective_rangeRestrict⟩ |
| 109 | + let bu := stdOrthonormalBasis 𝕜 U |
| 110 | + let bv := g.finrank_eq.symm ▸ stdOrthonormalBasis 𝕜 f.range |
| 111 | + rw [f.normDet_eq bu bv, norm_eq_zero.ne] |
| 112 | + suffices (f.rangeRestrict.adjoint.toMatrix bv.toBasis bu.toBasis).det * |
| 113 | + (f.rangeRestrict.toMatrix bu.toBasis bv.toBasis).det ≠ 0 by |
| 114 | + simpa [toMatrix_adjoint, Matrix.det_conjTranspose] using this |
| 115 | + simpa [← Matrix.det_mul, ← LinearMap.toMatrix_comp, det_eq_zero_iff_ker_ne_bot, |
| 116 | + LinearMap.ker_adjoint_comp_self] using h |
| 117 | + mpr h := by |
| 118 | + suffices ¬ Nonempty (OrthonormalBasis (Fin (Module.finrank 𝕜 U)) 𝕜 f.range) by |
| 119 | + simp [normDet, this] |
| 120 | + contrapose! h |
| 121 | + obtain ⟨b⟩ := h |
| 122 | + have hrank : Module.finrank 𝕜 f.range = Module.finrank 𝕜 U := by |
| 123 | + simpa using Module.finrank_eq_card_basis b.toBasis |
| 124 | + simpa [hrank] using f.finrank_range_add_finrank_ker |
| 125 | + |
| 126 | +/-- |
| 127 | +`LinearMap.normDet` equals to the norm of `LinearMap.det` for an endomorphism. |
| 128 | +-/ |
| 129 | +theorem normDet_eq_norm_det (f : U →ₗ[𝕜] U) : f.normDet = ‖f.det‖ := by |
| 130 | + by_cases h : f.range = ⊤ |
| 131 | + · let bv : OrthonormalBasis (Fin (Module.finrank 𝕜 U)) 𝕜 f.range := |
| 132 | + (stdOrthonormalBasis 𝕜 U).map (LinearIsometryEquiv.ofTop U _ h).symm |
| 133 | + rw [normDet_eq f (stdOrthonormalBasis 𝕜 U) bv] |
| 134 | + simp [bv, toMatrix_map_right] |
| 135 | + · have hb : ¬ Nonempty (OrthonormalBasis (Fin (Module.finrank 𝕜 U)) 𝕜 f.range) := by |
| 136 | + contrapose! h |
| 137 | + obtain ⟨b⟩ := h |
| 138 | + apply Submodule.eq_top_of_finrank_eq |
| 139 | + conv_lhs => rw [Module.finrank_eq_nat_card_basis b.toBasis] |
| 140 | + conv_rhs => rw [Module.finrank_eq_nat_card_basis (stdOrthonormalBasis 𝕜 U).toBasis] |
| 141 | + suffices f.det = 0 by |
| 142 | + simp [this, normDet, hb] |
| 143 | + simpa [det_eq_zero_iff_ker_ne_bot] using ker_eq_bot_iff_range_eq_top.not.mpr h |
| 144 | + |
| 145 | +/-- |
| 146 | +`LinearMap.normDet` of a linear isometry is 1. |
| 147 | +-/ |
| 148 | +theorem _root_.LinearIsometry.normDet_eq_one (f : U →ₗᵢ[𝕜] V) : f.toLinearMap.normDet = 1 := by |
| 149 | + have hrank : Module.finrank 𝕜 U = Module.finrank 𝕜 f.range := |
| 150 | + f.equivRange.toLinearEquiv.finrank_eq |
| 151 | + let b := (stdOrthonormalBasis 𝕜 f.toLinearMap.range) |
| 152 | + rw [← hrank] at b |
| 153 | + rw [normDet_eq _ (stdOrthonormalBasis 𝕜 U) b] |
| 154 | + apply CStarRing.norm_of_mem_unitary |
| 155 | + exact Matrix.det_of_mem_unitary <| (f.equivRange).toMatrix_mem_unitaryGroup _ _ |
| 156 | + |
| 157 | +set_option backward.isDefEq.respectTransparency false in |
| 158 | +/-- |
| 159 | +The square of `f.normDet` equals to the determinant of `f.adjoint ∘L f`. |
| 160 | +-/ |
| 161 | +theorem _root_.ContinuousLinearMap.normDet_sq [CompleteSpace V] (f : U →L[𝕜] V) : |
| 162 | + haveI : CompleteSpace U := FiniteDimensional.complete 𝕜 U |
| 163 | + ↑(f.normDet ^ 2) = (f.adjoint ∘L f).det := by |
| 164 | + have : CompleteSpace U := FiniteDimensional.complete 𝕜 U |
| 165 | + have : CompleteSpace f.range := FiniteDimensional.complete 𝕜 f.range |
| 166 | + let bu := stdOrthonormalBasis 𝕜 U |
| 167 | + classical |
| 168 | + by_cases hrank : Module.finrank 𝕜 U = Module.finrank 𝕜 f.range |
| 169 | + · let b : OrthonormalBasis (Fin (Module.finrank 𝕜 U)) 𝕜 f.range := |
| 170 | + (stdOrthonormalBasis 𝕜 f.range).reindex (by |
| 171 | + rw [← hrank, Module.finrank_eq_card_basis bu.toBasis]) |
| 172 | + have hf : f = f.range.subtypeₗᵢ.toContinuousLinearMap ∘L f.rangeRestrict := rfl |
| 173 | + conv_rhs => rw [hf] |
| 174 | + rw [ContinuousLinearMap.adjoint_comp, ← ContinuousLinearMap.comp_assoc, |
| 175 | + ContinuousLinearMap.comp_assoc (ContinuousLinearMap.adjoint _)] |
| 176 | + suffices f.range.subtypeₗᵢ.toContinuousLinearMap.adjoint ∘L |
| 177 | + f.range.subtypeₗᵢ.toContinuousLinearMap = ContinuousLinearMap.id 𝕜 _ by |
| 178 | + rw [this, ContinuousLinearMap.comp_id, ContinuousLinearMap.det, ContinuousLinearMap.coe_comp, |
| 179 | + ← det_toMatrix bu.toBasis, toMatrix_comp bu.toBasis b.toBasis bu.toBasis] |
| 180 | + rw [show (ContinuousLinearMap.adjoint f.rangeRestrict).toLinearMap = |
| 181 | + f.rangeRestrict.toLinearMap.adjoint by rfl] |
| 182 | + rw [toMatrix_adjoint] |
| 183 | + simp [f.toLinearMap.normDet_eq bu b, RCLike.conj_mul] |
| 184 | + exact f.range.subtypeₗᵢ.adjoint_comp_self |
| 185 | + · have hb : ¬ Nonempty (OrthonormalBasis (Fin (Module.finrank 𝕜 U)) 𝕜 f.range) := by |
| 186 | + contrapose! hrank with h |
| 187 | + obtain ⟨bv⟩ := h |
| 188 | + rw [Module.finrank_eq_card_basis bu.toBasis, Module.finrank_eq_card_basis bv.toBasis] |
| 189 | + trans 0 |
| 190 | + · simp [normDet, hb] |
| 191 | + symm |
| 192 | + rw [det_eq_zero_iff_ker_ne_bot, ContinuousLinearMap.ker_adjoint_comp_self] |
| 193 | + contrapose! hrank |
| 194 | + exact (finrank_range_of_inj <| ker_eq_bot.mp hrank).symm |
| 195 | + |
| 196 | +/-- |
| 197 | +The square of `f.normDet` equals to the determinant of `f.adjoint ∘ₗ f` when the codomain is finite |
| 198 | +dimensional. |
| 199 | +-/ |
| 200 | +theorem normDet_sq [FiniteDimensional 𝕜 V] (f : U →ₗ[𝕜] V) : |
| 201 | + ↑(f.normDet ^ 2) = (f.adjoint ∘ₗ f).det := by |
| 202 | + have : CompleteSpace V := FiniteDimensional.complete 𝕜 V |
| 203 | + exact f.toContinuousLinearMap.normDet_sq |
| 204 | + |
| 205 | +theorem normDet_sq_eq_det_gram {ι : Type*} [Fintype ι] [DecidableEq ι] (f : U →ₗ[𝕜] V) |
| 206 | + (b : OrthonormalBasis ι 𝕜 U) : |
| 207 | + ↑(f.normDet ^ 2) = (Matrix.gram 𝕜 (f <| b ·)).det := by |
| 208 | + change ↑(f.normDet ^ 2) = (Matrix.gram 𝕜 (f.rangeRestrict <| b ·)).det |
| 209 | + open ComplexOrder in |
| 210 | + by_cases hrank : Module.finrank 𝕜 U = Module.finrank 𝕜 f.range |
| 211 | + · let bv : OrthonormalBasis ι 𝕜 f.range := (stdOrthonormalBasis 𝕜 f.range).reindex |
| 212 | + (Fintype.equivFinOfCardEq (by rw [← Module.finrank_eq_card_basis b.toBasis, hrank])).symm |
| 213 | + rw [Matrix.gram_eq_conjTranspose_mul bv, Matrix.det_mul, Matrix.det_conjTranspose] |
| 214 | + rw [RCLike.star_def, RCLike.conj_mul] |
| 215 | + rw [f.normDet_eq b bv] |
| 216 | + simp only [map_pow] |
| 217 | + congr |
| 218 | + ext i j |
| 219 | + simp [LinearMap.toMatrix_apply] |
| 220 | + · have hb : ¬ Nonempty (OrthonormalBasis (Fin (Module.finrank 𝕜 U)) 𝕜 f.range) := by |
| 221 | + contrapose! hrank with h |
| 222 | + obtain ⟨bv⟩ := h |
| 223 | + simp [Module.finrank_eq_card_basis bv.toBasis] |
| 224 | + symm |
| 225 | + suffices (Matrix.gram 𝕜 (f.rangeRestrict <| b ·)).det = 0 by |
| 226 | + simpa [normDet, hb] |
| 227 | + contrapose! hrank with h0 |
| 228 | + obtain hindep := Matrix.linearIndependent_of_det_gram_ne_zero h0 |
| 229 | + apply le_antisymm ?_ (finrank_range_le f) |
| 230 | + rw [Module.finrank_eq_card_basis b.toBasis] |
| 231 | + exact hindep.fintype_card_le_finrank |
| 232 | + |
| 233 | +end LinearMap |
0 commit comments