injective_restrict_iff_disjoint — Mathlib

English

If p ⊆ M is a submodule with f mapping p into p (i.e., hf condition) then the restricted map f.restrict hf is injective if and only if p ∩ ker f = ⊥.

Русский

Пусть p ⊆ M — подмодуль, и f ограничено на p, тогда ограниченное отображение инъективно тогда и только тогда, когда p ∩ ker f тривиально.

LaTeX

$$$\operatorname{Injective}(f\restriction hf) \iff p \cap \ker f = \perp$$$

Lean4

@[simp]
theorem injective_restrict_iff_disjoint {p : Submodule R M} {f : M →ₗ[R] M} (hf : ∀ x ∈ p, f x ∈ p) :
    Injective (f.restrict hf) ↔ Disjoint p (ker f) := by
  rw [← ker_eq_bot, ker_restrict hf, ← ker_domRestrict, ker_eq_bot, injective_domRestrict_iff, disjoint_iff]

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