Complex rank in finite-dimensional coordinate spaces

This file defines the complex rank of a continuous complex-linear map and the standard rank-r coordinate map from ℂⁿ to ℂᵐ. The latter is a total definition for arbitrary n, m, and r; its rank is exactly r when r ≤ n and r ≤ m.

noncomputable def LocalComplexGeometry.complexRank {n m : ℕ} (A : ComplexEuclidean n →L[ℂ] ComplexEuclidean m) : ℕ

The complex dimension of the range of a continuous complex-linear map.

Equations

• LocalComplexGeometry.complexRank A = Module.finrank ℂ ↥(↑A).range

theorem LocalComplexGeometry.complexRank_le_source {n m : ℕ} (A : ComplexEuclidean n →L[ℂ] ComplexEuclidean m) : complexRank A ≤ n

Complex rank is bounded by the dimension of the source.

theorem LocalComplexGeometry.complexRank_le_target {n m : ℕ} (A : ComplexEuclidean n →L[ℂ] ComplexEuclidean m) : complexRank A ≤ m

Complex rank is bounded by the dimension of the target.

noncomputable def LocalComplexGeometry.standardRankContinuousLinearMap (n m r : ℕ) : ComplexEuclidean n →L[ℂ] ComplexEuclidean m

The standard rank map: retain a coordinate precisely when its index is available in the source and is strictly less than r, and put zero elsewhere.

Equations

• LocalComplexGeometry.standardRankContinuousLinearMap n m r = ContinuousLinearMap.pi fun (j : Fin m) => if h : ↑j < n ∧ ↑j < r then ContinuousLinearMap.proj ⟨↑j, ⋯⟩ else 0

noncomputable def LocalComplexGeometry.standardRankMap (n m r : ℕ) : ComplexEuclidean n → ComplexEuclidean m

The underlying function of standardRankContinuousLinearMap.

Equations

• LocalComplexGeometry.standardRankMap n m r = ⇑(LocalComplexGeometry.standardRankContinuousLinearMap n m r)

@[simp]

theorem LocalComplexGeometry.standardRankContinuousLinearMap_apply (n m r : ℕ) (x : ComplexEuclidean n) (j : Fin m) : (standardRankContinuousLinearMap n m r) x j = if h : ↑j < n ∧ ↑j < r then x ⟨↑j, ⋯⟩ else 0

@[simp]

theorem LocalComplexGeometry.standardRankMap_apply (n m r : ℕ) (x : ComplexEuclidean n) (j : Fin m) : standardRankMap n m r x j = if h : ↑j < n ∧ ↑j < r then x ⟨↑j, ⋯⟩ else 0

noncomputable def LocalComplexGeometry.takeFirstContinuousLinearMap {n r : ℕ} (hrn : r ≤ n) : ComplexEuclidean n →L[ℂ] ComplexEuclidean r

Restrict a coordinate vector to its first r coordinates.

Equations

• LocalComplexGeometry.takeFirstContinuousLinearMap hrn = ContinuousLinearMap.pi fun (j : Fin r) => ContinuousLinearMap.proj (Fin.castLE hrn j)

@[simp]

theorem LocalComplexGeometry.takeFirstContinuousLinearMap_apply {n r : ℕ} (hrn : r ≤ n) (x : ComplexEuclidean n) (j : Fin r) : (takeFirstContinuousLinearMap hrn) x j = x (Fin.castLE hrn j)

noncomputable def LocalComplexGeometry.includeFirstContinuousLinearMap (m r : ℕ) : ComplexEuclidean r →L[ℂ] ComplexEuclidean m

Extend an r-tuple by zero to an m-tuple.

Equations

• LocalComplexGeometry.includeFirstContinuousLinearMap m r = ContinuousLinearMap.pi fun (j : Fin m) => if h : ↑j < r then ContinuousLinearMap.proj ⟨↑j, h⟩ else 0

@[simp]

theorem LocalComplexGeometry.includeFirstContinuousLinearMap_apply (m r : ℕ) (x : ComplexEuclidean r) (j : Fin m) : (includeFirstContinuousLinearMap m r) x j = if h : ↑j < r then x ⟨↑j, h⟩ else 0

theorem LocalComplexGeometry.takeFirstContinuousLinearMap_surjective {n r : ℕ} (hrn : r ≤ n) : Function.Surjective ⇑(takeFirstContinuousLinearMap hrn)

Restriction to the first r coordinates is onto when r ≤ n.

theorem LocalComplexGeometry.includeFirstContinuousLinearMap_injective {m r : ℕ} (hrm : r ≤ m) : Function.Injective ⇑(includeFirstContinuousLinearMap m r)

Zero-extension of the first r coordinates is injective when r ≤ m.

theorem LocalComplexGeometry.standardRankContinuousLinearMap_eq_comp {n m r : ℕ} (hrn : r ≤ n) : standardRankContinuousLinearMap n m r = includeFirstContinuousLinearMap m r ∘SL takeFirstContinuousLinearMap hrn

Under r ≤ n, the standard map factors as restriction to ℂʳ followed by zero-extension.

theorem LocalComplexGeometry.complexRank_standardRankContinuousLinearMap {n m r : ℕ} (hrn : r ≤ n) (hrm : r ≤ m) : complexRank (standardRankContinuousLinearMap n m r) = r

The standard coordinate map has complex rank r whenever r fits in both source and target. This includes the zero-dimensional cases.

@[simp]

theorem LocalComplexGeometry.fderiv_standardRankMap (n m r : ℕ) (x : ComplexEuclidean n) : fderiv ℂ (standardRankMap n m r) x = standardRankContinuousLinearMap n m r

The Fréchet derivative of the standard coordinate map is the standard continuous linear map itself.

theorem LocalComplexGeometry.complexRank_fderiv_standardRankMap {n m r : ℕ} (hrn : r ≤ n) (hrm : r ≤ m) (x : ComplexEuclidean n) : complexRank (fderiv ℂ (standardRankMap n m r) x) = r

Pointwise formulation of the exact-rank calculation.