Tower of field extensions

In this file we prove the tower law for arbitrary extensions and finite extensions. Suppose L is a field extension of K and K is a field extension of F. Then [L:F] = [L:K] [K:F] where [E₁:E₂] means the E₂-dimension of E₁.

In fact we generalize it to rings and modules, where L is not necessarily a field, but just a free module over K.

Implementation notes

We prove two versions, since there are two notions of dimensions: Module.rank which gives the dimension of an arbitrary vector space as a cardinal, and FiniteDimensional.finrank which gives the dimension of a finite-dimensional vector space as a natural number.

Tags

tower law

theorem FiniteDimensional.trans (F : Type u) (K : Type v) (A : Type w) [DivisionRing F] [DivisionRing K] [AddCommGroup A] [Module F K] [Module K A] [Module F A] [IsScalarTower F K A] [FiniteDimensional F K] [FiniteDimensional K A] : FiniteDimensional F A

theorem FiniteDimensional.left (F : Type u) (K : Type v) (A : Type w) [DivisionRing F] [DivisionRing K] [AddCommGroup A] [Module F K] [Module K A] [Module F A] [IsScalarTower F K A] [Nontrivial A] [FiniteDimensional F A] : FiniteDimensional 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 FiniteDimensional.right (F : Type u) (K : Type v) (A : Type w) [DivisionRing F] [DivisionRing K] [AddCommGroup A] [Module F K] [Module K A] [Module F A] [IsScalarTower F K A] [hf : FiniteDimensional F A] : FiniteDimensional K A

theorem FiniteDimensional.Subalgebra.isSimpleOrder_of_finrank_prime (F : Type u_1) (A : Type u_2) [Field F] [Ring A] [IsDomain A] [Algebra F A] (hp : Nat.Prime (FiniteDimensional.finrank F A)) : IsSimpleOrder (Subalgebra F A)

@[deprecated FiniteDimensional.finrank_linearMap_self]

theorem FiniteDimensional.finrank_linear_map' (R : Type u) (S : Type u') (M : Type v) [Ring R] [Ring S] [AddCommGroup M] [Module R M] [Module.Free R M] [Module.Finite R M] [StrongRankCondition R] [StrongRankCondition S] [Module R S] [SMulCommClass R S S] : FiniteDimensional.finrank S (M →ₗ[R] S) = FiniteDimensional.finrank R M

Alias of FiniteDimensional.finrank_linearMap_self.