Documentation

LeanPool.LocalComplexGeometry.Analytic.ConstantRankLinear

Linear algebra for the constant-rank theorem #

The lemmas here isolate the finite-dimensional arguments used in the analytic constant-rank proof: invariance of range dimension under injective/surjective composition, a vertical-kernel criterion, and canonical product coordinates on Fin (r + k) → ℂ.

source
noncomputable def LocalComplexGeometry.complexLinearRank {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℂ E] [NormedAddCommGroup F] [NormedSpace ℂ F] (A : E →L[ℂ] F) :
ℕ

Range dimension for a continuous complex-linear map between arbitrary complex normed spaces.

Equations
Instances For
    source
    @[simp]
    theorem LocalComplexGeometry.complexLinearRank_eq_complexRank {n m : ℕ} (A : ComplexEuclidean n →L[ℂ] ComplexEuclidean m) :
    complexLinearRank A = complexRank A
    source
    theorem LocalComplexGeometry.complexLinearRank_comp_of_surjective_right {E : Type u_1} {F : Type u_2} {G : Type u_3} [NormedAddCommGroup E] [NormedSpace ℂ E] [NormedAddCommGroup F] [NormedSpace ℂ F] [NormedAddCommGroup G] [NormedSpace ℂ G] (A : F →L[ℂ] G) (B : E →L[ℂ] F) (hB : Function.Surjective ⇑B) :
    complexLinearRank (A ∘SL B) = complexLinearRank A

    Surjective precomposition does not change range dimension.

    source
    theorem LocalComplexGeometry.complexLinearRank_comp_of_injective_left {E : Type u_1} {F : Type u_2} {G : Type u_3} [NormedAddCommGroup E] [NormedSpace ℂ E] [FiniteDimensional ℂ E] [NormedAddCommGroup F] [NormedSpace ℂ F] [NormedAddCommGroup G] [NormedSpace ℂ G] (B : F →L[ℂ] G) (A : E →L[ℂ] F) (hB : Function.Injective ⇑B) :
    complexLinearRank (B ∘SL A) = complexLinearRank A

    Injective postcomposition does not change range dimension.

    source
    theorem LocalComplexGeometry.apply_zero_prod_eq_zero_of_rank_eq {U : Type u_1} {V : Type u_2} {W : Type u_3} [NormedAddCommGroup U] [NormedSpace ℂ U] [FiniteDimensional ℂ U] [NormedAddCommGroup V] [NormedSpace ℂ V] [FiniteDimensional ℂ V] [NormedAddCommGroup W] [NormedSpace ℂ W] (B : U × V →L[ℂ] U × W) (hfst : ContinuousLinearMap.fst ℂ U W ∘SL B = ContinuousLinearMap.fst ℂ U V) (hrank : complexLinearRank B = Module.finrank ℂ U) (v : V) :
    B (0, v) = 0

    If the first component of B : U × V → U × W is the first projection and B has the minimal possible rank dim U, then every vertical vector is killed by B.

    source
    def LocalComplexGeometry.finProdContinuousLinearEquiv (r k : ℕ) :
    (ComplexEuclidean r × ComplexEuclidean k) ≃L[ℂ] ComplexEuclidean (r + k)

    Canonically concatenate an r-tuple and a k-tuple.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem LocalComplexGeometry.finProdContinuousLinearEquiv_apply_castAdd (r k : ℕ) (x : ComplexEuclidean r × ComplexEuclidean k) (i : Fin r) :
      (finProdContinuousLinearEquiv r k) x (Fin.castAdd k i) = x.1 i
      source
      @[simp]
      theorem LocalComplexGeometry.finProdContinuousLinearEquiv_apply_natAdd (r k : ℕ) (x : ComplexEuclidean r × ComplexEuclidean k) (i : Fin k) :
      (finProdContinuousLinearEquiv r k) x (Fin.natAdd r i) = x.2 i
      source
      @[simp]
      theorem LocalComplexGeometry.finProdContinuousLinearEquiv_symm_fst_apply (r k : ℕ) (x : ComplexEuclidean (r + k)) (i : Fin r) :
      ((finProdContinuousLinearEquiv r k).symm x).1 i = x (Fin.castAdd k i)
      source
      @[simp]
      theorem LocalComplexGeometry.finProdContinuousLinearEquiv_symm_snd_apply (r k : ℕ) (x : ComplexEuclidean (r + k)) (i : Fin k) :
      ((finProdContinuousLinearEquiv r k).symm x).2 i = x (Fin.natAdd r i)
      source
      theorem LocalComplexGeometry.finProd_fst_zero_eq_standardRankMap (r n' m' : ℕ) (x : ComplexEuclidean (r + n')) :
      (finProdContinuousLinearEquiv r m') (((finProdContinuousLinearEquiv r n').symm x).1, 0) = standardRankMap (r + n') (r + m') r x

      Concatenating the first block of a vector with a zero block is precisely the standard rank map.

      source
      theorem LocalComplexGeometry.productEquiv_fst_zero_eq_standardRankMap {U : Type u_1} {V : Type u_2} {W : Type u_3} [NormedAddCommGroup U] [NormedSpace ℂ U] [NormedAddCommGroup V] [NormedSpace ℂ V] [NormedAddCommGroup W] [NormedSpace ℂ W] (r n' m' : ℕ) (eU : U ≃L[ℂ] ComplexEuclidean r) (eV : V ≃L[ℂ] ComplexEuclidean n') (eW : W ≃L[ℂ] ComplexEuclidean m') (x : ComplexEuclidean (r + n')) :
      ((eU.prodCongr eW).trans (finProdContinuousLinearEquiv r m')) ((((eU.prodCongr eV).trans (finProdContinuousLinearEquiv r n')).symm x).1, 0) = standardRankMap (r + n') (r + m') r x

      The preceding coordinate calculation after arbitrary linear coordinate choices on the three factors. The same equivalence is used on the rank factor in source and target.