English
The main equivalence built from a right inverse aligns with the tail decomposition, matching fst to f1 x and snd to x minus f2 (f1 x).
Русский
Главное эквивалентность, построенная из правого обратного, согласуется с разложением по хвосту: первая координата равна f1 x, вторая — x − f2(f1 x).
LaTeX
$$$ e(x) = \langle f_1 x, x - f_2(f_1 x) \rangle $$$
Lean4
/-- 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))`. -/
def equivOfRightInverse (f₁ : M →L[R] M₂) (f₂ : M₂ →L[R] M) (h : Function.RightInverse f₂ f₁) : M ≃L[R] M₂ × ker f₁ :=
equivOfInverse (f₁.prod (f₁.projKerOfRightInverse f₂ h)) (f₂.coprod (ker f₁).subtypeL) (fun x => by simp)
fun ⟨x, y⟩ => by simp [h x]
