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

source

theorem lift_rank_mul_lift_rank (F : Type u) (K : Type v) (A : Type w) [CommRing F] [Ring K] [AddCommGroup A] [Algebra F K] [Module K A] [Module F A] [IsScalarTower F K A] [StrongRankCondition F] [StrongRankCondition K] [Module.Free F K] [Module.Free K A] :

Cardinal.lift.{w, v} (Module.rank F K) * Cardinal.lift.{v, w} (Module.rank K A) = Cardinal.lift.{v, w} (Module.rank F A)

Tower law: if A is a K-module and K is an extension of F then $\operatorname{rank}_F(A) = \operatorname{rank}_F(K) * \operatorname{rank}_K(A)$.

source

theorem rank_mul_rank (F : Type u) (K : Type v) (A : Type v) [CommRing F] [Ring K] [AddCommGroup A] [Algebra F K] [Module K A] [Module F A] [IsScalarTower F K A] [StrongRankCondition F] [StrongRankCondition K] [Module.Free F K] [Module.Free K A] :

Module.rank F K * Module.rank K A = Module.rank F A

Tower law: if A is a K-module and K is an extension of F then $\operatorname{rank}_F(A) = \operatorname{rank}_F(K) * \operatorname{rank}_K(A)$.

This is a simpler version of lift_rank_mul_lift_rank with K and A in the same universe.

source

theorem FiniteDimensional.finrank_mul_finrank' (F : Type u) (K : Type v) (A : Type w) [CommRing F] [Ring K] [AddCommGroup A] [Algebra F K] [Module K A] [Module F A] [IsScalarTower F K A] [StrongRankCondition F] [StrongRankCondition K] [Module.Free F K] [Module.Free K A] [Module.Finite F K] [Module.Finite K A] :

FiniteDimensional.finrank F K * FiniteDimensional.finrank K A = FiniteDimensional.finrank F A

Tower law: if A is a K-module and K is an extension of F then $\operatorname{rank}_F(A) = \operatorname{rank}_F(K) * \operatorname{rank}_K(A)$.

source

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

FiniteDimensional F A

source

theorem FiniteDimensional.left (F : Type u) [Field F] (K : Type u_1) (L : Type u_2) [Field K] [Algebra F K] [Ring L] [Nontrivial L] [Algebra F L] [Algebra K L] [IsScalarTower F K L] [FiniteDimensional F L] :

FiniteDimensional F K

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

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

Note this cannot be an instance as Lean cannot infer L.

source

theorem FiniteDimensional.right (F : Type u) (K : Type v) (A : Type w) [Field F] [DivisionRing K] [AddCommGroup A] [Algebra F K] [Module K A] [Module F A] [IsScalarTower F K A] [hf : FiniteDimensional F A] :

FiniteDimensional K A

source

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

FiniteDimensional.finrank F K * FiniteDimensional.finrank K A = FiniteDimensional.finrank F A

Tower law: if A is a K-vector space and K is a field extension of F then dim_F(A) = dim_F(K) * dim_K(A).

This is FiniteDimensional.finrank_mul_finrank' with one fewer finiteness assumption.

source

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

IsSimpleOrder (Subalgebra F A)

source

instance LinearMap.finite_dimensional'' (F : Type u) (K : Type v) (V : Type w) [Field F] [Field K] [Algebra F K] [FiniteDimensional F K] [AddCommGroup V] [Module F V] [FiniteDimensional F V] :

FiniteDimensional K (V →ₗ[F] K)

Equations

LinearMap.finite_dimensional'' = LinearMap.finite_dimensional''.proof_1

source

theorem FiniteDimensional.finrank_linear_map' (F : Type u) (K : Type v) (V : Type w) [Field F] [Field K] [Algebra F K] [FiniteDimensional F K] [AddCommGroup V] [Module F V] [FiniteDimensional F V] :

FiniteDimensional.finrank K (V →ₗ[F] K) = FiniteDimensional.finrank F V