English
The rank of SymmetricAlgebra with a free module M is given by a precise cardinal expression involving rank M and aleph_0.
Русский
Ранг SymmetricAlgebra для свободного модуля M задаётся точным выражением кардинала, зависящим от ранга M и aleph_0.
LaTeX
$$$\operatorname{rank}_R(\operatorname{Sym}_R M) = \operatorname{lift}( \max(\operatorname{rank}_R M, \aleph_0) ).$$$
Lean4
theorem rank_eq [Nontrivial M] [Module.Free R M] :
Module.rank R (SymmetricAlgebra R M) = Cardinal.lift.{uR} (max (Module.rank R M) ℵ₀) :=
by
let ⟨⟨κ, b⟩⟩ := Module.Free.exists_basis (R := R) (M := M)
have : Nonempty κ := Basis.index_nonempty b
have : Nontrivial R := Module.nontrivial R M
rw [(equivMvPolynomial b).toLinearEquiv.rank_eq, MvPolynomial.rank_eq_lift, Cardinal.mk_finsupp_nat,
Basis.mk_eq_rank'' b]
