English
Let M,N be modules with the stated hypotheses, and f: M → N be an injective R-linear map under the rank condition rank_K N ≤ rank_R M. Then the span over K of the range of f is the whole N.
Русский
Пусть M,N — модули с указанными условиями, и f: M → N — инъективное R-обычное отображение при условии, что rank_K N ≤ rank_R M. Тогда область span_K образа f равна всему N.
LaTeX
$$$\operatorname{span}_K(\operatorname{range} f) = \top$$$
Lean4
theorem _root_.Submodule.span_range_eq_top_of_injective_of_rank_le {M N : Type u} [IsDomain R] [IsFractionRing R K]
[AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [Module K N] [IsScalarTower R K N] [Module.Finite K N]
{f : M →ₗ[R] N} (hf : Function.Injective f) (h : Module.rank K N ≤ Module.rank R M) :
Submodule.span K (LinearMap.range f : Set N) = ⊤ :=
by
obtain ⟨s, hs, hli⟩ := exists_set_linearIndependent R M
replace hli := hli.map' f (LinearMap.ker_eq_bot.mpr hf)
rw [LinearIndependent.iff_fractionRing (R := R) (K := K)] at hli
replace hs : Cardinal.mk s = Module.rank K N := le_antisymm (LinearIndependent.cardinal_le_rank hli) (hs ▸ h)
rw [← Module.finrank_eq_rank, Cardinal.mk_eq_nat_iff_fintype] at hs
obtain ⟨hfin, hcard⟩ := hs
have hsubset : Set.range (fun x : s ↦ f x.val) ⊆ (LinearMap.range f : Set N) :=
by
rintro x ⟨a, rfl⟩
simp
rw [eq_top_iff, ← LinearIndependent.span_eq_top_of_card_eq_finrank' hli hcard]
exact Submodule.span_mono hsubset
