English
If the underlying submodule of a subalgebra S is finitely generated, then S is finitely generated.
Русский
Если порождение подмодуля для S конечнопорожденно, то и S конечнопорождена.
LaTeX
$$$(S.toSubmodule).FG \\rightarrow S.FG$$$
Lean4
theorem fg_trans (h1 : (adjoin R s).toSubmodule.FG) (h2 : (adjoin (adjoin R s) t).toSubmodule.FG) :
(adjoin R (s ∪ t)).toSubmodule.FG := by
rcases fg_def.1 h1 with ⟨p, hp, hp'⟩
rcases fg_def.1 h2 with ⟨q, hq, hq'⟩
refine fg_def.2 ⟨p * q, hp.mul hq, le_antisymm ?_ ?_⟩
· rw [span_le, Set.mul_subset_iff]
intro x hx y hy
change x * y ∈ adjoin R (s ∪ t)
refine Subalgebra.mul_mem _ ?_ ?_
· have : x ∈ Subalgebra.toSubmodule (adjoin R s) := by
rw [← hp']
exact subset_span hx
exact adjoin_mono Set.subset_union_left this
have : y ∈ Subalgebra.toSubmodule (adjoin (adjoin R s) t) :=
by
rw [← hq']
exact subset_span hy
change y ∈ adjoin R (s ∪ t)
rwa [adjoin_union_eq_adjoin_adjoin]
· intro r hr
change r ∈ adjoin R (s ∪ t) at hr
rw [adjoin_union_eq_adjoin_adjoin] at hr
change r ∈ Subalgebra.toSubmodule (adjoin (adjoin R s) t) at hr
rw [← hq', ← Set.image_id q, Finsupp.mem_span_image_iff_linearCombination (adjoin R s)] at hr
rcases hr with ⟨l, hlq, rfl⟩
have := @Finsupp.linearCombination_apply A A (adjoin R s)
rw [this, Finsupp.sum]
refine sum_mem ?_
intro z hz
change (l z).1 * _ ∈ _
have : (l z).1 ∈ Subalgebra.toSubmodule (adjoin R s) := (l z).2
rw [← hp', ← Set.image_id p, Finsupp.mem_span_image_iff_linearCombination R] at this
rcases this with ⟨l2, hlp, hl⟩
have := @Finsupp.linearCombination_apply A A R
rw [this] at hl
rw [← hl, Finsupp.sum_mul]
refine sum_mem ?_
intro t ht
change _ * _ ∈ _
rw [smul_mul_assoc]
refine smul_mem _ _ ?_
exact subset_span ⟨t, hlp ht, z, hlq hz, rfl⟩
