kerι — Mathlib

English

The inclusion map from the kernel into M is the natural inclusion of the Submodule into the ambient module.

Русский

Включение из ядра в M является естественным вложением подпространства в надмодуль.

LaTeX

$$$\ker\iota_\varphi: \ker \varphi \to M$ is the inclusion (Submodule.subtype).$$

Lean4

/-- The inclusion map from the kernel in `TopModuleCat R`. -/
def kerι : ker φ ⟶ M :=
  ofHom ⟨Submodule.subtype _, continuous_subtype_val⟩

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