Invertibility of continuous linear maps: persistence and products

The totalized inverse of a continuous linear map is zero when the map is not invertible. Consequently, convergence of inverse maps to any nonzero map forces eventual invertibility. The inverse of an invertible map also suffices, including on trivial spaces. These results apply without completeness or continuity of the original family, and are useful when differentiating inverse families.

The file also records that the product f.prodMap g of two continuous linear maps is invertible exactly when both factors are, which is how block-diagonal second derivatives on a product space are shown to be invertible.

theorem ContinuousLinearMap.eventually_isInvertible_of_tendsto_inverse {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {ι : Type u_4} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [IsTopologicalAddGroup E] [T2Space E] [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] [ContinuousSMul 𝕜 F] {A : ι → E →L[𝕜] F} {B : F →L[𝕜] E} {l : Filter ι} (h : Filter.Tendsto (fun (i : ι) => (A i).inverse) l (nhds B)) (hB : B ≠ 0) : ∀ᶠ (i : ι) in l, (A i).IsInvertible

If the inverses of a family converge to a nonzero map, then the family is eventually invertible. Convergence uses the topology of bounded convergence; neither completeness nor convergence of the original family is required.

theorem ContinuousLinearMap.IsInvertible.eventually_of_tendsto_inverse {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {ι : Type u_4} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [IsTopologicalAddGroup E] [T2Space E] [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] [ContinuousSMul 𝕜 F] {A : ι → E →L[𝕜] F} {B : E →L[𝕜] F} (hB : B.IsInvertible) {l : Filter ι} (h : Filter.Tendsto (fun (i : ι) => (A i).inverse) l (nhds B.inverse)) : ∀ᶠ (i : ι) in l, (A i).IsInvertible

If the inverses of a family converge to the inverse of an invertible map, then the family is eventually invertible. Convergence uses the topology of bounded convergence; neither completeness nor convergence of the original family is required.

@[simp]

theorem ContinuousLinearMap.isInvertible_prodMap_iff {R : Type u_5} {M₁ : Type u_6} {M₂ : Type u_7} {M₃ : Type u_8} {M₄ : Type u_9} [Semiring R] [TopologicalSpace M₁] [AddCommMonoid M₁] [Module R M₁] [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R M₂] [TopologicalSpace M₃] [AddCommMonoid M₃] [Module R M₃] [TopologicalSpace M₄] [AddCommMonoid M₄] [Module R M₄] {f : M₁ →L[R] M₂} {g : M₃ →L[R] M₄} : (f.prodMap g).IsInvertible ↔ f.IsInvertible ∧ g.IsInvertible

The product f.prodMap g of two continuous linear maps is invertible exactly when both factors are.