Homotopy invariance of the Fredholm index

TheoremFredholm index is constant on preconnected families#✓fully proved

The Fredholm index is constant along a continuous family of Fredholm operators indexed by a preconnected set, because the index is locally constant (Mathlib) and takes values in the discrete space ℤ.

theorem index_eq_of_preconnected {X : Type*} [TopologicalSpace X] {s : Set X}
    (hs : IsPreconnected s) {γ : X → E →L[𝕜] F} (hγ : ContinuousOn γ s)
    {x y : X} (hx : x ∈ s) (hy : y ∈ s)
    (hfred : ∀ z ∈ s, (γ z).IsFredholm) : (γ x).index = (γ y).index

Used by 1

Used byFredholm index is constant along a path continuous on (0, 1)

TheoremFredholm index is constant along a path continuous on (0, 1)#✓fully proved

The Fredholm index is constant along a continuous path of Fredholm operators on [0, 1].

theorem index_eq_of_continuousOn_Icc {γ : ℝ → E →L[𝕜] F}
    (hγ : ContinuousOn γ (Icc (0 : ℝ) 1))
    (hfred : ∀ t ∈ Icc (0 : ℝ) 1, (γ t).IsFredholm) :
    (γ 0).index = (γ 1).index

Uses 1 · Used by 1

Proof usesFredholm index is constant on preconnected families

Used byFredholm index is constant along a globally continuous path

TheoremFredholm index is constant along a globally continuous path#✓fully proved

The Fredholm index is constant along a globally continuous path of Fredholm operators on [0, 1].

theorem index_eq_of_continuous_path {γ : ℝ → E →L[𝕜] F} (hγ : Continuous γ)
    (hfred : ∀ t ∈ Icc (0 : ℝ) 1, (γ t).IsFredholm) :
    (γ 0).index = (γ 1).index

Uses 1 · Used by 2

Proof usesFredholm index is constant along a path continuous on (0, 1)

Used byFinite-rank perturbation preserves the Fredholm index · Shifted unilateral shift has index \(-1\) inside the unit disk

TheoremRank-one operators have finite range#✓fully proved

A rank-one operator has finite range.

theorem hasFiniteRange_smulRight {𝕜 E F : Type*} [NontriviallyNormedField 𝕜]
    [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedSpace 𝕜 E] [NormedSpace 𝕜 F]
    {c : E →L[𝕜] 𝕜} {y : F} :
    (c.smulRight y).toLinearMap.HasFiniteRange

TheoremFinite-rank perturbation preserves the Fredholm index#✓fully proved

Adding a finite-rank operator does not change the Fredholm index. The proof follows the segment T + t • F, t ∈ [0, 1], which is a continuous path of Fredholm operators.

theorem index_add_hasFiniteRange {T G : E →L[𝕜] F} (hT : T.IsFredholm)
    (hG : G.toLinearMap.HasFiniteRange) : (T + G).index = T.index

Uses 1 · Used by 2

Proof usesFredholm index is constant along a globally continuous path

Used byLeft finite-rank perturbation preserves the Fredholm index · Subtracting a finite-rank operator preserves the Fredholm index

TheoremLeft finite-rank perturbation preserves the Fredholm index#✓fully proved

Adding a finite-rank operator on the left does not change the Fredholm index.

theorem index_hasFiniteRange_add {T G : E →L[𝕜] F} (hT : T.IsFredholm)
    (hG : G.toLinearMap.HasFiniteRange) : (G + T).index = T.index

Uses 1

Proof usesFinite-rank perturbation preserves the Fredholm index

TheoremSubtracting a finite-rank operator preserves the Fredholm index#✓fully proved

Subtracting a finite-rank operator does not change the Fredholm index.

theorem index_sub_hasFiniteRange {T G : E →L[𝕜] F} (hT : T.IsFredholm)
    (hG : G.toLinearMap.HasFiniteRange) : (T - G).index = T.index

Uses 1

Proof usesFinite-rank perturbation preserves the Fredholm index

7 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.