English
For a commutative ring R, a ring S, and an algebra structure, the rank of the subalgebra adjoin_R s is bounded by the maximum of the size of s and aleph0.
Русский
Для кольца R, кольца S и структуры алгебры, ранг подалгебры adjoin_R s не превосходит max(#s, aleph_0).
LaTeX
$$$\\operatorname{Module.rank}_R(\\operatorname{adjoin}_R s) \\le \\max\\#s \\aleph_0$$$
Lean4
theorem rank_adjoin_le {R : Type u} {S : Type v} [CommRing R] [Ring S] [Algebra R S] (s : Set S) :
Module.rank R (adjoin R s) ≤ max #s ℵ₀ :=
by
rw [adjoin_eq_range_freeAlgebra_lift]
cases subsingleton_or_nontrivial R
· rw [rank_subsingleton]; exact one_le_aleph0.trans (le_max_right _ _)
rw [← lift_le.{max u v}]
refine (lift_rank_range_le (FreeAlgebra.lift R ((↑) : s → S)).toLinearMap).trans ?_
rw [FreeAlgebra.rank_eq, lift_id'.{v, u}, lift_umax.{v, u}, lift_le, max_comm]
exact mk_list_le_max _
