English
The underlying Submodule of N'.comap f equals the comap of N' underlying Submodule: (N'.comap f).toSubmodule = (N' : Submodule R M').comap (f).
Русский
Подмодуль обратного образа равен обратному образу подмодуля: (N'.comap f).toSubmodule = (N' : Submodule R M').comap (f).
LaTeX
$$(N'.comap f).toSubmodule = (N' : Submodule R M').comap (f : M →ₗ[R] M')$$
Lean4
/-- A morphism of Lie modules `f : M → M'` pulls back Lie submodules of `M'` to Lie submodules of
`M`. -/
def comap : LieSubmodule R L M :=
{ (N' : Submodule R M').comap (f : M →ₗ[R] M') with
lie_mem := fun {x m} h ↦ by
suffices ⁅x, f m⁆ ∈ N' by simp [this]
apply N'.lie_mem h }
