English
Let f: M → M₂ and g: M₂ → M be σ-linear maps such that f ∘ g = id_{M₂} and g ∘ f = id_M. Then f is an isomorphism of σ-linear spaces, with inverse g.
Русский
Пусть f: M → M₂ и g: M₂ → M линейны по σ и τ так, что f ∘ g = id_{M₂} и g ∘ f = id_M. Тогда f является изоморфизмом σ-линейных пространств, обратный ему — g.
LaTeX
$$$\text{If } f: M \to_{\sigma_{12}} M_2 \text{ and } g: M_2 \to_{\sigma_{21}} M \\text{ satisfy } f \circ g = \mathrm{id}_{M_2} \text{ and } g \circ f = \mathrm{id}_M, \\text{then } M \cong_{\sigma_{12}} M_2.$$$
Lean4
/-- If a linear map has an inverse, it is a linear equivalence. -/
def ofLinear (h₁ : f.comp g = LinearMap.id) (h₂ : g.comp f = LinearMap.id) : M ≃ₛₗ[σ₁₂] M₂ :=
{ f with
invFun := g
left_inv := LinearMap.ext_iff.1 h₂
right_inv := LinearMap.ext_iff.1 h₁ }
