English
If two families s and t of a type A are finitely generated (as submodules) after adjoin operations, then the adjoin of their union s ∪ t is finitely generated.
Русский
Если s и t задают финитно порожденные подалгебры через адъюнкцию, то адъюнкция s ∪ t порождается конечным числом элементов.
LaTeX
$$$\\text{Let } (adjoin_R s).\\toSubmodule.FG \\text{ and } (adjoin_(adjoin_R s) t).\\toSubmodule.FG, \\text{ then } (adjoin_R (s \\cup t)).toSubmodule.FG$$$
Lean4
/-- If `A` and `B` are subalgebras of a commutative `R`-algebra `S`, both of them are
free `R`-algebras, then the rank of the rank of the subalgebra generated by `A` and `B`
over `R` is less than or equal to the product of that of `A` and `B`. -/
theorem rank_sup_le_of_free : Module.rank R ↥(A ⊔ B) ≤ Module.rank R A * Module.rank R B :=
by
obtain ⟨ιA, bA⟩ := Free.exists_basis (R := R) (M := A)
obtain ⟨ιB, bB⟩ := Free.exists_basis (R := R) (M := B)
have h := Algebra.adjoin_union_coe_submodule R (A : Set S) (B : Set S)
rw [A.adjoin_eq_span_basis R bA, B.adjoin_eq_span_basis R bB, ← Algebra.sup_def, Submodule.span_mul_span] at h
change Module.rank R ↥(toSubmodule (A ⊔ B)) ≤ _
rw [h, ← bA.mk_eq_rank'', ← bB.mk_eq_rank'']
refine (rank_span_le _).trans Cardinal.mk_mul_le |>.trans ?_
gcongr <;> exact Cardinal.mk_range_le
