Invertibility of continuous linear maps #

In this file, we define the predicate ContinuousLinearMap.IsInvertible, expressing that a given continuous (semi)linear map is the forward direction of a ContinuousLinearEquiv (in other words, it has a continuous inverse).

source

def ContinuousLinearMap.IsInvertible {R : Type u_1} {M : Type u_2} {M₂ : Type u_3} [TopologicalSpace M] [TopologicalSpace M₂] [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid M₂] [Module R M₂] (f : M →L[R] M₂) :

Prop

A continuous linear map is invertible if it is the forward direction of a continuous linear equivalence.

Equations

f.IsInvertible = ∃ (A : M ≃L[R] M₂), ↑A = f

Instances For

source

noncomputable def ContinuousLinearMap.inverse {R : Type u_1} {M : Type u_2} {M₂ : Type u_3} [TopologicalSpace M] [TopologicalSpace M₂] [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid M₂] [Module R M₂] :

(M →L[R] M₂) → M₂ →L[R] M

Introduce a function inverse from M →L[R] M₂ to M₂ →L[R] M, which sends f to f.symm if f is a continuous linear equivalence and to 0 otherwise. This definition is somewhat ad hoc, but one needs a fully (rather than partially) defined inverse function for some purposes, including for calculus.

Equations

f.inverse = if h : f.IsInvertible then ↑(Classical.choose h).symm else 0

Instances For

source

@[simp]

theorem ContinuousLinearMap.isInvertible_equiv {R : Type u_1} {M : Type u_2} {M₂ : Type u_3} [TopologicalSpace M] [TopologicalSpace M₂] [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid M₂] [Module R M₂] {f : M ≃L[R] M₂} :

(↑f).IsInvertible

source

@[simp]

theorem ContinuousLinearMap.inverse_equiv {R : Type u_1} {M : Type u_2} {M₂ : Type u_3} [TopologicalSpace M] [TopologicalSpace M₂] [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid M₂] [Module R M₂] (e : M ≃L[R] M₂) :

(↑e).inverse = ↑e.symm

By definition, if f is invertible then inverse f = f.symm.

source

@[simp]

theorem ContinuousLinearMap.inverse_of_not_isInvertible {R : Type u_1} {M : Type u_2} {M₂ : Type u_3} [TopologicalSpace M] [TopologicalSpace M₂] [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid M₂] [Module R M₂] {f : M →L[R] M₂} (hf : ¬f.IsInvertible) :

f.inverse = 0

By definition, if f is not invertible then inverse f = 0.

source

@[simp]

theorem ContinuousLinearMap.isInvertible_zero_iff {R : Type u_1} {M : Type u_2} {M₂ : Type u_3} [TopologicalSpace M] [TopologicalSpace M₂] [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid M₂] [Module R M₂] :

IsInvertible 0 ↔ Subsingleton M ∧ Subsingleton M₂

source

@[simp]

theorem ContinuousLinearMap.inverse_zero {R : Type u_1} {M : Type u_2} {M₂ : Type u_3} [TopologicalSpace M] [TopologicalSpace M₂] [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid M₂] [Module R M₂] :

inverse 0 = 0

source

theorem ContinuousLinearMap.IsInvertible.comp {R : Type u_1} {M : Type u_2} {M₂ : Type u_3} {M₃ : Type u_4} [TopologicalSpace M] [TopologicalSpace M₂] [TopologicalSpace M₃] [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid M₂] [Module R M₂] [AddCommMonoid M₃] [Module R M₃] {g : M₂ →L[R] M₃} {f : M →L[R] M₂} (hg : g.IsInvertible) (hf : f.IsInvertible) :

(g ∘SL f).IsInvertible

source

theorem ContinuousLinearMap.IsInvertible.of_inverse {R : Type u_1} {M : Type u_2} {M₂ : Type u_3} [TopologicalSpace M] [TopologicalSpace M₂] [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid M₂] [Module R M₂] {f : M →L[R] M₂} {g : M₂ →L[R] M} (hf : f ∘SL g = ContinuousLinearMap.id R M₂) (hg : g ∘SL f = ContinuousLinearMap.id R M) :

f.IsInvertible

source

theorem ContinuousLinearMap.inverse_eq {R : Type u_1} {M : Type u_2} {M₂ : Type u_3} [TopologicalSpace M] [TopologicalSpace M₂] [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid M₂] [Module R M₂] {f : M →L[R] M₂} {g : M₂ →L[R] M} (hf : f ∘SL g = ContinuousLinearMap.id R M₂) (hg : g ∘SL f = ContinuousLinearMap.id R M) :

f.inverse = g

source

theorem ContinuousLinearMap.IsInvertible.inverse_apply_eq {R : Type u_1} {M : Type u_2} {M₂ : Type u_3} [TopologicalSpace M] [TopologicalSpace M₂] [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid M₂] [Module R M₂] {f : M →L[R] M₂} {x : M} {y : M₂} (hf : f.IsInvertible) :

f.inverse y = x ↔ y = f x

source

@[simp]

theorem ContinuousLinearMap.isInvertible_equiv_comp {R : Type u_1} {M : Type u_2} {M₂ : Type u_3} {M₃ : Type u_4} [TopologicalSpace M] [TopologicalSpace M₂] [TopologicalSpace M₃] [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid M₂] [Module R M₂] [AddCommMonoid M₃] [Module R M₃] {e : M₂ ≃L[R] M₃} {f : M →L[R] M₂} :

(↑e ∘SL f).IsInvertible ↔ f.IsInvertible

source

@[simp]

theorem ContinuousLinearMap.isInvertible_comp_equiv {R : Type u_1} {M : Type u_2} {M₂ : Type u_3} {M₃ : Type u_4} [TopologicalSpace M] [TopologicalSpace M₂] [TopologicalSpace M₃] [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid M₂] [Module R M₂] [AddCommMonoid M₃] [Module R M₃] {e : M₃ ≃L[R] M} {f : M →L[R] M₂} :

(f ∘SL ↑e).IsInvertible ↔ f.IsInvertible

source

@[simp]

theorem ContinuousLinearMap.inverse_equiv_comp {R : Type u_1} {M : Type u_2} {M₂ : Type u_3} {M₃ : Type u_4} [TopologicalSpace M] [TopologicalSpace M₂] [TopologicalSpace M₃] [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid M₂] [Module R M₂] [AddCommMonoid M₃] [Module R M₃] {e : M₂ ≃L[R] M₃} {f : M →L[R] M₂} :

(↑e ∘SL f).inverse = f.inverse ∘SL ↑e.symm

source

@[simp]

theorem ContinuousLinearMap.inverse_comp_equiv {R : Type u_1} {M : Type u_2} {M₂ : Type u_3} {M₃ : Type u_4} [TopologicalSpace M] [TopologicalSpace M₂] [TopologicalSpace M₃] [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid M₂] [Module R M₂] [AddCommMonoid M₃] [Module R M₃] {e : M₃ ≃L[R] M} {f : M →L[R] M₂} :

(f ∘SL ↑e).inverse = ↑e.symm ∘SL f.inverse

source

theorem ContinuousLinearMap.IsInvertible.inverse_comp_of_left {R : Type u_1} {M : Type u_2} {M₂ : Type u_3} {M₃ : Type u_4} [TopologicalSpace M] [TopologicalSpace M₂] [TopologicalSpace M₃] [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid M₂] [Module R M₂] [AddCommMonoid M₃] [Module R M₃] {g : M₂ →L[R] M₃} {f : M →L[R] M₂} (hg : g.IsInvertible) :

(g ∘SL f).inverse = f.inverse ∘SL g.inverse

source

theorem ContinuousLinearMap.IsInvertible.inverse_comp_apply_of_left {R : Type u_1} {M : Type u_2} {M₂ : Type u_3} {M₃ : Type u_4} [TopologicalSpace M] [TopologicalSpace M₂] [TopologicalSpace M₃] [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid M₂] [Module R M₂] [AddCommMonoid M₃] [Module R M₃] {g : M₂ →L[R] M₃} {f : M →L[R] M₂} {v : M₃} (hg : g.IsInvertible) :

(g ∘SL f).inverse v = f.inverse (g.inverse v)

source

theorem ContinuousLinearMap.IsInvertible.inverse_comp_of_right {R : Type u_1} {M : Type u_2} {M₂ : Type u_3} {M₃ : Type u_4} [TopologicalSpace M] [TopologicalSpace M₂] [TopologicalSpace M₃] [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid M₂] [Module R M₂] [AddCommMonoid M₃] [Module R M₃] {g : M₂ →L[R] M₃} {f : M →L[R] M₂} (hf : f.IsInvertible) :

(g ∘SL f).inverse = f.inverse ∘SL g.inverse

source

theorem ContinuousLinearMap.IsInvertible.inverse_comp_apply_of_right {R : Type u_1} {M : Type u_2} {M₂ : Type u_3} {M₃ : Type u_4} [TopologicalSpace M] [TopologicalSpace M₂] [TopologicalSpace M₃] [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid M₂] [Module R M₂] [AddCommMonoid M₃] [Module R M₃] {g : M₂ →L[R] M₃} {f : M →L[R] M₂} {v : M₃} (hf : f.IsInvertible) :

(g ∘SL f).inverse v = f.inverse (g.inverse v)

source

@[simp]

theorem ContinuousLinearMap.ringInverse_equiv {R : Type u_1} {M : Type u_2} [TopologicalSpace M] [Semiring R] [AddCommMonoid M] [Module R M] (e : M ≃L[R] M) :

Ring.inverse ↑e = (↑e).inverse

source

theorem ContinuousLinearMap.inverse_eq_ringInverse {R : Type u_1} {M : Type u_2} {M₂ : Type u_3} [TopologicalSpace M] [TopologicalSpace M₂] [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid M₂] [Module R M₂] (e : M ≃L[R] M₂) (f : M →L[R] M₂) :

f.inverse = Ring.inverse (↑e.symm ∘SL f) ∘SL ↑e.symm

The function ContinuousLinearEquiv.inverse can be written in terms of Ring.inverse for the ring of self-maps of the domain.

source

theorem ContinuousLinearMap.ringInverse_eq_inverse {R : Type u_1} {M : Type u_2} [TopologicalSpace M] [Semiring R] [AddCommMonoid M] [Module R M] :

Ring.inverse = inverse

source

@[simp]

theorem ContinuousLinearMap.inverse_id {R : Type u_1} {M : Type u_2} [TopologicalSpace M] [Semiring R] [AddCommMonoid M] [Module R M] :

(ContinuousLinearMap.id R M).inverse = ContinuousLinearMap.id R M

source

@[simp]

theorem ContinuousLinearMap.IsInvertible.self_comp_inverse {R : Type u_1} {M : Type u_2} {M₂ : Type u_3} [TopologicalSpace M] [TopologicalSpace M₂] [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid M₂] [Module R M₂] {f : M →L[R] M₂} (hf : f.IsInvertible) :

f ∘SL f.inverse = ContinuousLinearMap.id R M₂

source

@[simp]

theorem ContinuousLinearMap.IsInvertible.self_apply_inverse {R : Type u_1} {M : Type u_2} {M₂ : Type u_3} [TopologicalSpace M] [TopologicalSpace M₂] [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid M₂] [Module R M₂] {f : M →L[R] M₂} (hf : f.IsInvertible) (y : M₂) :

f (f.inverse y) = y

source

@[simp]

theorem ContinuousLinearMap.IsInvertible.inverse_comp_self {R : Type u_1} {M : Type u_2} {M₂ : Type u_3} [TopologicalSpace M] [TopologicalSpace M₂] [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid M₂] [Module R M₂] {f : M →L[R] M₂} (hf : f.IsInvertible) :

f.inverse ∘SL f = ContinuousLinearMap.id R M

source

@[simp]

theorem ContinuousLinearMap.IsInvertible.inverse_apply_self {R : Type u_1} {M : Type u_2} {M₂ : Type u_3} [TopologicalSpace M] [TopologicalSpace M₂] [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid M₂] [Module R M₂] {f : M →L[R] M₂} (hf : f.IsInvertible) (y : M) :

f.inverse (f y) = y

source

theorem ContinuousLinearMap.IsInvertible.bijective {R : Type u_1} {M : Type u_2} {M₂ : Type u_3} [TopologicalSpace M] [TopologicalSpace M₂] [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid M₂] [Module R M₂] {f : M →L[R] M₂} (hf : f.IsInvertible) :

Function.Bijective ⇑f

source

theorem ContinuousLinearMap.IsInvertible.injective {R : Type u_1} {M : Type u_2} {M₂ : Type u_3} [TopologicalSpace M] [TopologicalSpace M₂] [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid M₂] [Module R M₂] {f : M →L[R] M₂} (hf : f.IsInvertible) :

Function.Injective ⇑f

source

theorem ContinuousLinearMap.IsInvertible.surjective {R : Type u_1} {M : Type u_2} {M₂ : Type u_3} [TopologicalSpace M] [TopologicalSpace M₂] [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid M₂] [Module R M₂] {f : M →L[R] M₂} (hf : f.IsInvertible) :

Function.Surjective ⇑f

source

theorem ContinuousLinearMap.IsInvertible.inverse {R : Type u_1} {M : Type u_2} {M₂ : Type u_3} [TopologicalSpace M] [TopologicalSpace M₂] [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid M₂] [Module R M₂] {f : M →L[R] M₂} (hf : f.IsInvertible) :

f.inverse.IsInvertible

source

@[simp]

theorem ContinuousLinearMap.IsInvertible.inverse_inverse {R : Type u_1} {M : Type u_2} {M₂ : Type u_3} [TopologicalSpace M] [TopologicalSpace M₂] [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid M₂] [Module R M₂] {f : M →L[R] M₂} (hf : f.IsInvertible) :

f.inverse.inverse = f

source

theorem ContinuousLinearMap.IsInvertible.of_isInvertible_inverse {R : Type u_1} {M : Type u_2} {M₂ : Type u_3} [TopologicalSpace M] [TopologicalSpace M₂] [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid M₂] [Module R M₂] {f : M →L[R] M₂} (hf : f.inverse.IsInvertible) :

f.IsInvertible

source

@[simp]

theorem ContinuousLinearMap.isInvertible_inverse_iff {R : Type u_1} {M : Type u_2} {M₂ : Type u_3} [TopologicalSpace M] [TopologicalSpace M₂] [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid M₂] [Module R M₂] {f : M →L[R] M₂} :

f.inverse.IsInvertible ↔ f.IsInvertible

Documentation

Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Invertible

Invertibility of continuous linear maps #