English
Ring inverse of a linear map can be expressed via conjugation by a linear equivalence: inverse f = Ring.inverse((e.symm ∘ f)) ∘ e.symm.
Русский
Кольцевое обратное к отображению выражается через сопряжение линейным эквивалентом: обратная $f$ равна кольцевому обратному от $e^{-1} f$ затем $e^{-1}$.
LaTeX
$$inverse f = Ring.inverse ((e.symm : M_2 →L[R] M) .comp f) ∘L e.symm$$
Lean4
/-- The function `ContinuousLinearEquiv.inverse` can be written in terms of `Ring.inverse` for the
ring of self-maps of the domain. -/
theorem inverse_eq_ringInverse (e : M ≃L[R] M₂) (f : M →L[R] M₂) :
inverse f = Ring.inverse ((e.symm : M₂ →L[R] M).comp f) ∘L e.symm :=
by
by_cases h₁ : f.IsInvertible
· obtain ⟨e', he'⟩ := h₁
rw [← he']
change _ = Ring.inverse (e'.trans e.symm : M →L[R] M) ∘L (e.symm : M₂ →L[R] M)
ext
simp
· suffices ¬IsUnit ((e.symm : M₂ →L[R] M).comp f) by simp [this, h₁]
contrapose! h₁
rcases h₁ with ⟨F, hF⟩
use (ContinuousLinearEquiv.unitsEquiv _ _ F).trans e
ext
dsimp
rw [hF]
simp
