English
The inverse (as a Lie module morphism) of a bijective Lie module morphism is a Lie module morphism.
Русский
Обратное по отношению к биективному морфизму Ли-модуля является морфизмом Ли-модуля.
LaTeX
$$def inverse (f : M →ₗ⁅R,L⁆ N) (g : N → M) (h₁ : Function.LeftInverse g f) (h₂ : Function.RightInverse g f) : N →ₗ⁅R,L⁆ M := ...$$
Lean4
/-- The inverse of a bijective morphism of Lie modules is a morphism of Lie modules. -/
def inverse (f : M →ₗ⁅R,L⁆ N) (g : N → M) (h₁ : Function.LeftInverse g f) (h₂ : Function.RightInverse g f) :
N →ₗ⁅R,L⁆ M :=
{ LinearMap.inverse f.toLinearMap g h₁ h₂ with
map_lie' := by
intro x n
calc
g ⁅x, n⁆ = g ⁅x, f (g n)⁆ := by rw [h₂]
_ = g (f ⁅x, g n⁆) := by rw [map_lie]
_ = ⁅x, g n⁆ := h₁ _ }
