The dimension of a base change

A module specified as a base change of a finite module is finite. If the module being extended is free and both semirings satisfy the strong rank condition, then the two modules have the same natural-number rank (Module.finrank), including when their rank is infinite and finrank is zero. Both statements are about Mathlib's IsBaseChange predicate rather than about the concrete tensor product S ⊗[R] M, so they apply to a model of the base change that is not literally a tensor product — the situation the IsBaseChange interface exists to serve.

Mathlib proves the corresponding facts for the concrete tensor product (Module.finrank_baseChange and the Module.Finite instance on S ⊗[R] M); transporting them along IsBaseChange.equiv : S ⊗[R] M ≃ₗ[S] N is all that is needed.

theorem IsBaseChange.finite {R : Type u_1} {S : Type u_2} {M : Type u_3} {N : Type u_4} [CommSemiring R] [CommSemiring S] [Algebra R S] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [Module S N] [IsScalarTower R S N] {f : M →ₗ[R] N} (hf : IsBaseChange S f) [Module.Finite R M] : Module.Finite S N

A base change of a finite module is a finite module.

theorem IsBaseChange.finrank_eq_of_free {R : Type u_1} {S : Type u_2} {M : Type u_3} {N : Type u_4} [CommSemiring R] [CommSemiring S] [Algebra R S] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [Module S N] [IsScalarTower R S N] {f : M →ₗ[R] N} (hf : IsBaseChange S f) [StrongRankCondition R] [StrongRankCondition S] [Module.Free R M] : Module.finrank S N = Module.finrank R M

A base change of a free module preserves Module.finrank when the source and target semirings satisfy the strong rank condition. No finite-generation assumption is needed.