Mathlib.FieldTheory.Tower

Module docstring

{"# 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

Module.Finite.left theorem

[Nontrivial A] : Module.Finite F K

Full source

/-- 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 left [Nontrivial A] : Module.Finite F K :=
  let ⟨x, hx⟩ := exists_ne (0 : A)
  Module.Finite.of_injective
    (LinearMap.ringLmapEquivSelf K ℕ A |>.symm x |>.restrictScalars F) (smul_left_injective K hx)

Finiteness of $K$ over $F$ in a scalar tower with nontrivial $A$

Informal description

Let $F$, $K$, and $A$ be modules over a semiring such that $A$ is a scalar tower over $F$ and $K$ (i.e., $A$ is an $F$-module and a $K$-module with compatible scalar multiplications). If $A$ is a nontrivial module, then $K$ is finitely generated as an $F$-module.

Module.Finite.right theorem

[hf : Module.Finite F A] : Module.Finite K A

Full source

@[stacks 09G5]
theorem right [hf : Module.Finite F A] : Module.Finite K A :=
  let ⟨⟨b, hb⟩⟩ := hf
  ⟨⟨b, Submodule.restrictScalars_injective F _ _ <| by
    rw [Submodule.restrictScalars_top, eq_top_iff, ← hb, Submodule.span_le]
    exact Submodule.subset_span⟩⟩

Finiteness of scalar tower modules: $A$ finitely generated over $F$ implies $A$ finitely generated over $K$

Informal description

Let $F$, $K$, and $A$ be modules over a semiring such that $A$ is a scalar tower over $F$ and $K$ (i.e., $A$ is an $F$-module and a $K$-module with compatible scalar multiplications). If $A$ is finitely generated as an $F$-module, then $A$ is also finitely generated as a $K$-module.