# Finiteness of `IsScalarTower` #

We prove that given `IsScalarTower F K A`, if `A` is finite as a module over `F` then `A` is finite over `K`, and (as long as `A` is Noetherian over `F` and we have `NoZeroSMulDivisors K A`) `K` is finite over `F`.

In particular these conditions hold when `A`, `F`, and `K` are fields.

The formulas for the dimensions are given elsewhere by `Module.finrank_mul_finrank`.

## Tags #

tower law

source
theorem Module.Finite.left (F : Type u) (K : Type v) (A : Type w) [Ring F] [Ring K] [Module F K] [AddCommGroup A] [Module K A] [NoZeroSMulDivisors K A] [Module F A] [IsNoetherian F A] [IsScalarTower F K A] [Nontrivial A] :
Module.Finite F K

In a tower of field extensions `A / K / F`, if `A / F` is finite, so is `K / F`.

(In fact, it suffices that `A` is a nontrivial ring.)

Note this cannot be an instance as Lean cannot infer `A`.

source
theorem Module.Finite.right (F : Type u) (K : Type v) (A : Type w) [Semiring F] [Semiring K] [Module F K] [AddCommMonoid A] [Module K A] [Module F A] [IsScalarTower F K A] [hf : Module.Finite F A] :
Module.Finite K A

Stacks Tag 09G5

source
theorem FiniteDimensional.left (F : Type u) (K : Type v) (A : Type w) [Ring F] [Ring K] [Module F K] [AddCommGroup A] [Module K A] [NoZeroSMulDivisors K A] [Module F A] [IsNoetherian F A] [IsScalarTower F K A] [Nontrivial A] :
Module.Finite F K

Alias of `Module.Finite.left`.

In a tower of field extensions `A / K / F`, if `A / F` is finite, so is `K / F`.

(In fact, it suffices that `A` is a nontrivial ring.)

Note this cannot be an instance as Lean cannot infer `A`.

source
theorem FiniteDimensional.right (F : Type u) (K : Type v) (A : Type w) [Semiring F] [Semiring K] [Module F K] [AddCommMonoid A] [Module K A] [Module F A] [IsScalarTower F K A] [hf : Module.Finite F A] :
Module.Finite K A

Alias of `Module.Finite.right`.

Stacks Tag 09G5