English
The underlying linear map of the maxTrivLinearMapEquivLieModuleHom is just the given linear map.
Русский
Пониженное линейное отображение maxTrivLinearMapEquivLieModuleHom равно данному линейному отображению.
LaTeX
$$$\\text{coe}_{\\text{maxTrivLinearMapEquivLieModuleHom}} = \\text{identity on the underlying linear map}$$$
Lean4
/-- A linear map between two Lie modules is a morphism of Lie modules iff the Lie algebra action
on it is trivial. -/
def maxTrivLinearMapEquivLieModuleHom : maxTrivSubmodule R L (M →ₗ[R] N) ≃ₗ[R] M →ₗ⁅R,L⁆ N
where
toFun
f :=
{ toLinearMap := f.val
map_lie' := fun {x m} =>
by
have hf : ⁅x, f.val⁆ m = 0 := by rw [f.property x, LinearMap.zero_apply]
rw [LieHom.lie_apply, sub_eq_zero, ← LinearMap.toFun_eq_coe] at hf; exact hf.symm }
map_add' f g := by ext; simp
map_smul' F G := by ext; simp
invFun F := ⟨F, fun x => by ext; simp⟩
left_inv f := by simp
right_inv F := by simp
