Theorems · Theorem · operator theory

ContinuousLinearMap.isFredholm_tfae

∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : AddCommGroup E]
  [inst_2 : AddCommGroup F] [inst_3 : Module 𝕜 E] [inst_4 : Module 𝕜 F] [inst_5 : TopologicalSpace E]
  [inst_6 : TopologicalSpace F] [CompleteSpace 𝕜] [IsTopologicalAddGroup E] [ContinuousSMul 𝕜 E]
  [IsTopologicalAddGroup F] [ContinuousSMul 𝕜 F] [T2Space E] [T2Space F] (u : E →L[𝕜] F),
  [u.IsFredholm, ∃ v, (↑v).IsQuasiInverse ↑u,
      ∃ E₁ F₁,
        IsClosed ↑E₁ ∧ IsClosed ↑F₁ ∧ E₁.CoFG ∧ F₁.CoFG ∧ ∃ (h : Set.MapsTo ⇑u ↑E₁ ↑F₁), (u.restrict h).IsInvertible,
      Nonempty u.FredholmPackage].TFAE

Let E, F be two Hausdorff topological vector spaces over a complete NontriviallyNormedField denoted 𝕜, and u : E →L[𝕜] F a continuous linear map. The following conditions are equivalent: 1. u is a Fredholm operator, in the sense of ContinuousLinearMap.IsFredholm. 2. u admits a continuous quasi-inverse, in the sense of LinearMap.IsQuasiInverse. 3. There are closed finite-codimension subspaces E₁ and F₁ of E and F between which u induces an isomorphism. 4. u admits a FredholmPackage. In practice, condition 4 is the "strongest", so you should probably not use it to prove that an operator is Fredholm.

Defined in

Mathlib.Analysis.Normed.Operator.Fredholm.Basic

Cited by

2 results in Mathlib

Foundations

Depth 182 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NontriviallyNormedFieldAddCommGroupAddCommGroupModuleModuleTopologicalSpaceTopologicalSpaceCompleteSpaceIsTopologicalAddGroupContinuousSMulIsTopologicalAddGroupContinuousSMulT2SpaceT2Space