English
Let f: M →ₛₗ[σ] M2 and g: M2 → M. If g is both a left inverse and a right inverse of f, then g is σ'-linear.
Русский
Пусть f: M →ₛₗ[σ] M2 — линейное отображение, g: M2 → M. Если g является одновременно левой и правой обратной к f, то g является σ'-линейной (то есть линейным относительно σ').
LaTeX
$$$\\text{If } h_1:\\text{LeftInverse } g f \\text{ and } h_2:\\text{RightInverse } g f,\\ then } g \\in \\operatorname{Hom}_{\\sigma'}(M_2,M).$$$
Lean4
/-- If a function `g` is a left and right inverse of a linear map `f`, then `g` is linear itself. -/
def inverse (f : M →ₛₗ[σ] M₂) (g : M₂ → M) (h₁ : LeftInverse g f) (h₂ : RightInverse g f) : M₂ →ₛₗ[σ'] M :=
by
dsimp [LeftInverse, Function.RightInverse] at h₁ h₂
exact
{ toFun := g
map_add' := fun x y ↦ by rw [← h₁ (g (x + y)), ← h₁ (g x + g y)]; simp [h₂]
map_smul' := fun a b ↦ by
rw [← h₁ (g (a • b)), ← h₁ (σ' a • g b)]
simp [h₂] }
