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

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.

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

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.

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.