Index of continuous linear maps

The index of a continuous linear map is the integer dim ker T − dim coker T. Mathlib already develops the purely algebraic LinearMap.index; this file transfers its elementary API to continuous linear maps. The value is junk when the kernel or cokernel is infinite-dimensional, following Mathlib's convention for LinearMap.index. The definition and its elementary formulas need only algebraic module structures and topologies; continuity hypotheses are confined to the operations that need them.

Main declarations

• ContinuousLinearMap.index: the index of a continuous linear map.
• ContinuousLinearMap.index_eq_finrank_sub: the defining dimension formula.
• ContinuousLinearMap.index_eq_of_finiteDimensional: between finite-dimensional spaces, the index is the dimension of the domain minus the dimension of the codomain.
• ContinuousLinearMap.index_zero: the index of the zero map is the difference of the dimensions.
• ContinuousLinearMap.index_id, ContinuousLinearEquiv.index_eq_zero, and index_eq_zero_of_bijective: identities, continuous linear equivalences, and bijective maps have index zero.
• ContinuousLinearMap.index_smul and index_neg: nonzero rescaling and negation preserve the index.
• ContinuousLinearMap.index_equiv_comp and index_comp_equiv: composition with a continuous linear equivalence preserves the index.
• ContinuousLinearMap.index_of_surjective and index_of_injective: the index in the one-sided cases.
• ContinuousLinearMap.finrank_ker_eq_iff_index_eq and bijective_of_surjective_of_index_eq_zero: index zero detects bijectivity for a surjective map with finite-dimensional kernel.

The sign convention follows McDuff--Salamon, J-holomorphic Curves and Symplectic Topology, Appendix A.1.

noncomputable def ContinuousLinearMap.index {𝕜 : Type u_1} [Ring 𝕜] {E : Type u_2} {F : Type u_3} [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] (T : E →L[𝕜] F) : ℤ

The index of a continuous linear map, dim ker T − dim coker T, defined as the index of the underlying linear map.

Equations

• T.index = (↑T).index

theorem ContinuousLinearMap.index_def {𝕜 : Type u_1} [Ring 𝕜] {E : Type u_2} {F : Type u_3} [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] (T : E →L[𝕜] F) : T.index = (↑T).index

The index as the algebraic index of the underlying linear map.

theorem ContinuousLinearMap.index_eq_finrank_sub {𝕜 : Type u_1} [Ring 𝕜] {E : Type u_2} {F : Type u_3} [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] (T : E →L[𝕜] F) : T.index = ↑(Module.finrank 𝕜 ↥(↑T).ker) - ↑(Module.finrank 𝕜 (F ⧸ (↑T).range))

The index is dim ker T − dim coker T.

@[simp]

theorem ContinuousLinearMap.index_zero {𝕜 : Type u_1} [Ring 𝕜] {E : Type u_2} {F : Type u_3} [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] : index 0 = ↑(Module.finrank 𝕜 E) - ↑(Module.finrank 𝕜 F)

The index of the zero continuous linear map is the dimension of its domain minus the dimension of its codomain.

theorem ContinuousLinearMap.index_of_surjective {𝕜 : Type u_1} [Ring 𝕜] {E : Type u_2} {F : Type u_3} [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] [Nontrivial 𝕜] (T : E →L[𝕜] F) (hT : Function.Surjective ⇑T) : T.index = ↑(Module.finrank 𝕜 ↥(↑T).ker)

A surjective continuous linear map has index the dimension of its kernel.

theorem ContinuousLinearMap.finrank_ker_eq_iff_index_eq {𝕜 : Type u_1} [Ring 𝕜] {E : Type u_2} {F : Type u_3} [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] [Nontrivial 𝕜] {n : ℕ} (T : E →L[𝕜] F) (hT : Function.Surjective ⇑T) : Module.finrank 𝕜 ↥(↑T).ker = n ↔ T.index = ↑n

For a surjective continuous linear map, having index n and having a kernel of dimension n are the same statement.

theorem ContinuousLinearMap.index_of_injective {𝕜 : Type u_1} [Ring 𝕜] {E : Type u_2} {F : Type u_3} [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] [Nontrivial 𝕜] (T : E →L[𝕜] F) (hT : Function.Injective ⇑T) : T.index = -↑(Module.finrank 𝕜 (F ⧸ (↑T).range))

An injective continuous linear map has index the negative of the dimension of its cokernel.

theorem ContinuousLinearMap.index_eq_zero_of_bijective {𝕜 : Type u_1} [Ring 𝕜] {E : Type u_2} {F : Type u_3} [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] (T : E →L[𝕜] F) (hT : Function.Bijective ⇑T) : T.index = 0

A bijective continuous linear map has index zero.

@[simp]

theorem ContinuousLinearMap.index_id {𝕜 : Type u_1} [Ring 𝕜] {E : Type u_2} [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] : (ContinuousLinearMap.id 𝕜 E).index = 0

The identity operator has index 0.

@[simp]

theorem ContinuousLinearEquiv.index_eq_zero {𝕜 : Type u_1} [Ring 𝕜] {E : Type u_2} {F : Type u_3} [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] (e : E ≃L[𝕜] F) : (↑e).index = 0

A continuous linear equivalence has index 0.

@[simp]

theorem ContinuousLinearMap.index_neg {𝕜 : Type u_1} [Ring 𝕜] {E : Type u_2} {F : Type u_3} [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] [IsTopologicalAddGroup F] (T : E →L[𝕜] F) : (-T).index = T.index

The index is unchanged by negation.

@[simp]

theorem ContinuousLinearMap.index_equiv_comp {𝕜 : Type u_1} [Ring 𝕜] {E : Type u_2} {F : Type u_3} {G : Type u_4} [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] [AddCommGroup G] [Module 𝕜 G] [TopologicalSpace G] (T : E →L[𝕜] F) (e : F ≃L[𝕜] G) : (↑e ∘SL T).index = T.index

Postcomposing with a continuous linear equivalence leaves the index unchanged.

@[simp]

theorem ContinuousLinearMap.index_comp_equiv {𝕜 : Type u_1} [Ring 𝕜] {E : Type u_2} {F : Type u_3} {G : Type u_4} [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] [AddCommGroup G] [Module 𝕜 G] [TopologicalSpace G] (T : E →L[𝕜] F) (e : G ≃L[𝕜] E) : (T ∘SL ↑e).index = T.index

Precomposing with a continuous linear equivalence leaves the index unchanged.

theorem ContinuousLinearMap.index_eq_of_finiteDimensional {𝕜 : Type u_1} [DivisionRing 𝕜] {E : Type u_2} {F : Type u_3} [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 F] (T : E →L[𝕜] F) : T.index = ↑(Module.finrank 𝕜 E) - ↑(Module.finrank 𝕜 F)

Between finite-dimensional spaces the index is dim E − dim F, for any operator.

theorem ContinuousLinearMap.bijective_of_surjective_of_index_eq_zero {𝕜 : Type u_1} [DivisionRing 𝕜] {E : Type u_2} {F : Type u_3} [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] (T : E →L[𝕜] F) (hfin : FiniteDimensional 𝕜 ↥(↑T).ker) (hT : Function.Surjective ⇑T) (hindex : T.index = 0) : Function.Bijective ⇑T

A surjective operator of index zero with finite-dimensional kernel is bijective. Only finiteness of the kernel is used, not the full Fredholm property. This is the converse of ContinuousLinearMap.index_eq_zero_of_bijective for a surjective operator.

theorem ContinuousLinearMap.index_smul {𝕜 : Type u_1} [Field 𝕜] {E : Type u_2} {F : Type u_3} [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] [ContinuousConstSMul 𝕜 F] (T : E →L[𝕜] F) {c : 𝕜} (hc : c ≠ 0) : (c • T).index = T.index

The index is unchanged by a nonzero scalar multiple.