ker_codRestrict — Mathlib

English

Let f: M1 →SL[σ12] M2 be a continuous semilinear map and p ⊆ M2 a submodule such that f(x) ∈ p for all x ∈ M1. Then restricting the codomain of f to p does not change its kernel; i.e., ker(f codRestrict p h) = ker f.

Русский

Пусть f: M1 →SL[σ12] M2 — непрерывно-линейное отображение; пусть p ⊆ M2 — подмодуль и f(x) ∈ p для всех x в M1. Тогда ядро отображения f, ограниченного по codomain к p, равно ядру f: ker(f codRestrict p h) = ker f.

LaTeX

$$$\ker (f \operatorname{codRestrict} p h) = \ker f,$$$

Lean4

@[simp]
theorem ker_codRestrict (f : M₁ →SL[σ₁₂] M₂) (p : Submodule R₂ M₂) (h : ∀ x, f x ∈ p) :
    ker (f.codRestrict p h) = ker f :=
  (f : M₁ →ₛₗ[σ₁₂] M₂).ker_codRestrict p h

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