English
If 0 → M' → M → M'' → 0 is exact and M' and M'' are finitely generated, then so is M.
Русский
Если последовательность 0 → M' → M → M'' → 0 точна и M' и M'' конечнопорождаются, то и M конечнопорождается.
LaTeX
$$If 0 → M' → M → M'' → 0 is exact and (M') FG and (M'') FG then M FG$$
Lean4
/-- If 0 → M' → M → M'' → 0 is exact and M' and M'' are
finitely generated then so is M. -/
theorem fg_of_fg_map_of_fg_inf_ker (f : M →ₗ[R] P) {s : Submodule R M} (hs1 : (s.map f).FG)
(hs2 : (s ⊓ LinearMap.ker f).FG) : s.FG :=
by
haveI := Classical.decEq R
haveI := Classical.decEq M
haveI := Classical.decEq P
obtain ⟨t1, ht1⟩ := hs1
obtain ⟨t2, ht2⟩ := hs2
have : ∀ y ∈ t1, ∃ x ∈ s, f x = y := by
intro y hy
have : y ∈ s.map f := by
rw [← ht1]
exact subset_span hy
rcases mem_map.1 this with ⟨x, hx1, hx2⟩
exact ⟨x, hx1, hx2⟩
have : ∃ g : P → M, ∀ y ∈ t1, g y ∈ s ∧ f (g y) = y :=
by
choose g hg1 hg2 using this
exists fun y => if H : y ∈ t1 then g y H else 0
intro y H
constructor
· simp only [dif_pos H]
apply hg1
· simp only [dif_pos H]
apply hg2
obtain ⟨g, hg⟩ := this
clear this
exists t1.image g ∪ t2
rw [Finset.coe_union, span_union, Finset.coe_image]
apply le_antisymm
· refine sup_le (span_le.2 <| image_subset_iff.2 ?_) (span_le.2 ?_)
· intro y hy
exact (hg y hy).1
· intro x hx
have : x ∈ span R t2 := subset_span hx
rw [ht2] at this
exact this.1
intro x hx
have : f x ∈ s.map f := by
rw [mem_map]
exact ⟨x, hx, rfl⟩
rw [← ht1, ← Set.image_id (t1 : Set P), Finsupp.mem_span_image_iff_linearCombination] at this
rcases this with ⟨l, hl1, hl2⟩
refine
mem_sup.2
⟨(linearCombination R id).toFun ((lmapDomain R R g : (P →₀ R) → M →₀ R) l), ?_,
x - linearCombination R id ((lmapDomain R R g : (P →₀ R) → M →₀ R) l), ?_, add_sub_cancel _ _⟩
· rw [← Set.image_id (g '' ↑t1), Finsupp.mem_span_image_iff_linearCombination]
refine ⟨_, ?_, rfl⟩
haveI : Inhabited P := ⟨0⟩
rw [← Finsupp.lmapDomain_supported _ _ g, mem_map]
refine ⟨l, hl1, ?_⟩
rfl
rw [ht2, mem_inf]
constructor
· apply s.sub_mem hx
rw [Finsupp.linearCombination_apply, Finsupp.lmapDomain_apply, Finsupp.sum_mapDomain_index]
· refine s.sum_mem ?_
intro y hy
exact s.smul_mem _ (hg y (hl1 hy)).1
· exact zero_smul _
· exact fun _ _ _ => add_smul _ _ _
· rw [LinearMap.mem_ker, f.map_sub, ← hl2]
rw [Finsupp.linearCombination_apply, Finsupp.linearCombination_apply, Finsupp.lmapDomain_apply]
rw [Finsupp.sum_mapDomain_index, Finsupp.sum, Finsupp.sum, map_sum]
· rw [sub_eq_zero]
refine Finset.sum_congr rfl fun y hy => ?_
unfold id
rw [f.map_smul, (hg y (hl1 hy)).2]
· exact zero_smul _
· exact fun _ _ _ => add_smul _ _ _
