Documentation

Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Invertible

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
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
    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