Theorems · Definition · functional analysis

ContinuousLinearEquiv.equivOfRightInverse

{R : Type u_1} →
  [inst : Ring R] →
    {M : Type u_3} →
      [inst_1 : TopologicalSpace M] →
        [inst_2 : AddCommGroup M] →
          [inst_3 : Module R M] →
            {M₂ : Type u_4} →
              [inst_4 : TopologicalSpace M₂] →
                [inst_5 : AddCommGroup M₂] →
                  [inst_6 : Module R M₂] →
                    [IsTopologicalAddGroup M] →
                      (f₁ : M →L[R] M₂) → (f₂ : M₂ →L[R] M) → Function.RightInverse ⇑f₂ ⇑f₁ → M ≃L[R] M₂ × ↥(↑f₁).ker

A pair of continuous linear maps such that f₁ ∘ f₂ = id generates a continuous linear equivalence e between M and M₂ × f₁.ker such that (e x).2 = x for x ∈ f₁.ker, (e x).1 = f₁ x, and (e (f₂ y)).2 = 0. The map is given by e x = (f₁ x, x - f₂ (f₁ x)).

Defined in

Mathlib.Topology.Algebra.Module.Equiv

Cited by

5 results in Mathlib

Foundations

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

Assumes

RingTopologicalSpaceAddCommGroupModuleTopologicalSpaceAddCommGroupModuleIsTopologicalAddGroup