English
Under assumptions of fg in both A⊂C and B⊂C, there exists a subalgebra B0 of A with FG and such that ⊤ as a submodule of C over B0 is FG.
Русский
При предположении о FG в A⊂C и B⊂C существует подалгебра B0 ⊂ A, FG над A, и ⊤ как подмодуль C над B0 FG.
LaTeX
$$$\\exists B_0 \\leq A,\\; B_0.FG \\land (\\top : Submodule B_0 C).FG$$$
Lean4
theorem exists_subalgebra_of_fg (hAC : (⊤ : Subalgebra A C).FG) (hBC : (⊤ : Submodule B C).FG) :
∃ B₀ : Subalgebra A B, B₀.FG ∧ (⊤ : Submodule B₀ C).FG :=
by
obtain ⟨x, hx⟩ := hAC
obtain ⟨y, hy⟩ := hBC
have := hy
simp_rw [eq_top_iff', mem_span_finset] at this
choose f _ hf using this
classical
let s : Finset B := Finset.image₂ f (x ∪ y * y) y
have hxy : ∀ xi ∈ x, xi ∈ span (Algebra.adjoin A (↑s : Set B)) (↑(insert 1 y : Finset C) : Set C) := fun xi hxi =>
hf xi ▸
sum_mem fun yj hyj =>
smul_mem (span (Algebra.adjoin A (↑s : Set B)) (↑(insert 1 y : Finset C) : Set C))
⟨f xi yj, Algebra.subset_adjoin <| mem_image₂_of_mem (mem_union_left _ hxi) hyj⟩
(subset_span <| mem_insert_of_mem hyj)
have hyy :
span (Algebra.adjoin A (↑s : Set B)) (↑(insert 1 y : Finset C) : Set C) *
span (Algebra.adjoin A (↑s : Set B)) (↑(insert 1 y : Finset C) : Set C) ≤
span (Algebra.adjoin A (↑s : Set B)) (↑(insert 1 y : Finset C) : Set C) :=
by
rw [span_mul_span, span_le, coe_insert]
rintro _ ⟨yi, rfl | hyi, yj, rfl | hyj, rfl⟩ <;> dsimp
· rw [mul_one]
exact subset_span (Set.mem_insert _ _)
· rw [one_mul]
exact subset_span (Set.mem_insert_of_mem _ hyj)
· rw [mul_one]
exact subset_span (Set.mem_insert_of_mem _ hyi)
· rw [← hf (yi * yj)]
exact
SetLike.mem_coe.2
(sum_mem fun yk hyk =>
smul_mem (span (Algebra.adjoin A (↑s : Set B)) (insert 1 ↑y : Set C))
⟨f (yi * yj) yk,
Algebra.subset_adjoin <| mem_image₂_of_mem (mem_union_right _ <| mul_mem_mul hyi hyj) hyk⟩
(subset_span <| Set.mem_insert_of_mem _ hyk : yk ∈ _))
refine ⟨Algebra.adjoin A (↑s : Set B), Subalgebra.fg_adjoin_finset _, insert 1 y, ?_⟩
convert restrictScalars_injective A (Algebra.adjoin A (s : Set B)) C _
rw [restrictScalars_top, eq_top_iff, ← Algebra.top_toSubmodule, ← hx, Algebra.adjoin_eq_span, span_le]
refine fun r hr =>
Submonoid.closure_induction (fun c hc => hxy c hc) (subset_span <| mem_insert_self _ _)
(fun p q _ _ hp hq => hyy <| Submodule.mul_mem_mul hp hq) hr
