English
If a certain finite-generation injectivity condition holds for restricted submodules, then f.rTensor M is injective.
Русский
Если для любых порожденных подмодулей выполняется условие инъективности прообраза через rTensor, то f.rTensor M инъективен.
LaTeX
$$$(\forall N',P', N'\FG, P'\FG, h: N' \le P'.\mathrm{comap}(f), \; (f|_{N'}).\!\!\mathrm{rTensor} M \text{ инъективен}) \Rightarrow (f\;\mathrm{rTensor}\; M)\text{ инъективен}$$$
Lean4
theorem _root_.LinearMap.rTensor_injective_of_fg {f : N →ₗ[R] P}
(h :
∀ (N' : Submodule R N) (P' : Submodule R P),
N'.FG → P'.FG → ∀ h : N' ≤ P'.comap f, Function.Injective ((f.restrict h).rTensor M)) :
Function.Injective (f.rTensor M) := fun x y eq ↦
by
have ⟨N', Nfg, sub⟩ := Submodule.exists_fg_le_subset_range_rTensor_subtype { x, y } (by simp)
obtain ⟨x, rfl⟩ := sub (.inl rfl)
obtain ⟨y, rfl⟩ := sub (.inr rfl)
simp_rw [← rTensor_comp_apply, show f ∘ₗ N'.subtype = (N'.map f).subtype ∘ₗ f.submoduleMap N' from rfl,
rTensor_comp_apply] at eq
have ⟨P', Pfg, le, eq⟩ := (Nfg.map _).exists_rTensor_fg_inclusion_eq eq
simp_rw [← rTensor_comp_apply] at eq
rw [h _ _ Nfg Pfg (map_le_iff_le_comap.mp le) eq]
