Tower of field extensions #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 finite_dimensional.finrank which gives the dimension of a finitely-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) [comm_ring F] [ring K] [add_comm_group A] [algebra F K] [module K A] [module F A] [is_scalar_tower F K A] [strong_rank_condition F] [strong_rank_condition K] [module.free F K] [module.free K A] :

(module.rank F K).lift * (module.rank K A).lift = (module.rank F A).lift

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 A : Type v) [comm_ring F] [ring K] [add_comm_group A] [algebra F K] [module K A] [module F A] [is_scalar_tower F K A] [strong_rank_condition F] [strong_rank_condition 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 finite_dimensional.finrank_mul_finrank' (F : Type u) (K : Type v) (A : Type w) [comm_ring F] [ring K] [add_comm_group A] [algebra F K] [module K A] [module F A] [is_scalar_tower F K A] [strong_rank_condition F] [strong_rank_condition K] [module.free F K] [module.free K A] [nontrivial K] [module.finite F K] [module.finite K A] :

finite_dimensional.finrank F K * finite_dimensional.finrank K A = finite_dimensional.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 finite_dimensional.trans (F : Type u) (K : Type v) (A : Type w) [field F] [division_ring K] [add_comm_group A] [algebra F K] [module K A] [module F A] [is_scalar_tower F K A] [finite_dimensional F K] [finite_dimensional K A] :

finite_dimensional F A

source

theorem finite_dimensional.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] [is_scalar_tower F K L] [finite_dimensional F L] :

finite_dimensional 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 finite_dimensional.right (F : Type u) (K : Type v) (A : Type w) [field F] [division_ring K] [add_comm_group A] [algebra F K] [module K A] [module F A] [is_scalar_tower F K A] [hf : finite_dimensional F A] :

finite_dimensional K A

source

theorem finite_dimensional.finrank_mul_finrank (F : Type u) (K : Type v) (A : Type w) [field F] [division_ring K] [add_comm_group A] [algebra F K] [module K A] [module F A] [is_scalar_tower F K A] [finite_dimensional F K] :

finite_dimensional.finrank F K * finite_dimensional.finrank K A = finite_dimensional.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 finite_dimensional.finrank_mul_finrank' with one fewer finiteness assumption.

source

theorem finite_dimensional.subalgebra.is_simple_order_of_finrank_prime (F : Type u) [field F] (A : Type u_1) [ring A] [is_domain A] [algebra F A] (hp : nat.prime (finite_dimensional.finrank F A)) :

is_simple_order (subalgebra F A)

source

@[protected, instance]

def linear_map.finite_dimensional'' (F : Type u) (K : Type v) (V : Type w) [field F] [field K] [algebra F K] [finite_dimensional F K] [add_comm_group V] [module F V] [finite_dimensional F V] :

finite_dimensional K (V →ₗ[F] K)

source

theorem finite_dimensional.finrank_linear_map' (F : Type u) (K : Type v) (V : Type w) [field F] [field K] [algebra F K] [finite_dimensional F K] [add_comm_group V] [module F V] [finite_dimensional F V] :

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