English
Let f be a semilinear map and S a submodule. Then Injective (f.domRestrict S) holds precisely when S ∩ ker f = ⊥.
Русский
Пусть f — полу-линейное отображение, S — подмодуль. Инъективность ограниченного отображения f на S эквивалентна тому, что пересечение S и ядра f тривиально.
LaTeX
$$$\operatorname{Injective}(f\mathrm{.domRestrict}\,S) \iff S \cap \ker f = \perp$$$
Lean4
@[simp]
theorem injective_domRestrict_iff {f : M →ₛₗ[τ₁₂] M₂} {S : Submodule R M} :
Injective (f.domRestrict S) ↔ S ⊓ LinearMap.ker f = ⊥ :=
by
rw [← LinearMap.ker_eq_bot]
refine ⟨fun h ↦ le_bot_iff.1 ?_, fun h ↦ le_bot_iff.1 ?_⟩
· intro x ⟨hx, h'x⟩
have : ⟨x, hx⟩ ∈ LinearMap.ker (LinearMap.domRestrict f S) := by simpa using h'x
rw [h] at this
simpa [mk_eq_zero] using this
· rintro ⟨x, hx⟩ h'x
have : x ∈ S ⊓ LinearMap.ker f := ⟨hx, h'x⟩
rw [h] at this
simpa [mk_eq_zero] using this
