comap_toSubmodule — Mathlib

English

For a LieHom f: L → L' and a LieIdeal J ⊆ L', the LieSubmodule toSubmodule of comap f J equals the comap of the submodule J.

Русский

Пусть f: L → L' — гомоморфизм Ли и J ⊆ L' — Ли-идеал. Тогда LieSubmodule.toSubmodule(comap f J) = (LieSubmodule.toSubmodule J).comap f.

LaTeX

$$$\\mathrm{LieSubmodule}.toSubmodule(\\mathrm{comap}\\ f\\ J) = (\\mathrm{LieSubmodule}.toSubmodule J).comap(f) $$$

Lean4

@[simp]
theorem comap_toSubmodule :
    (LieSubmodule.toSubmodule (comap f J)) = (LieSubmodule.toSubmodule J).comap (f : L →ₗ[R] L') :=
  rfl

Похожие утверждения