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 vector spaces, where L is not necessarily a field, but just a vector space over K.

Implementation notes

We prove two versions, since there are two notions of dimensions: vector_space.dim which gives the dimension of an arbitrary vector space as a cardinal, and finite_dimensional.findim which gives the dimension of a finitely-dimensional vector space as a natural number.

Tags

tower law

source

theorem dim_mul_dim' (F : Type u) (K : Type v) (A : Type w) [field F] [field K] [add_comm_group A] [algebra F K] [vector_space K A] [vector_space F A] [is_scalar_tower F K A] :

((vector_space.dim F K).lift) * (vector_space.dim K A).lift = (vector_space.dim F A).lift

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).

source

theorem dim_mul_dim (F : Type u) (K A : Type v) [field F] [field K] [add_comm_group A] [algebra F K] [vector_space K A] [vector_space F A] [is_scalar_tower F K A] :

(vector_space.dim F K) * vector_space.dim K A = vector_space.dim 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).

source

theorem finite_dimensional.trans (F : Type u) (K : Type v) (A : Type w) [field F] [field K] [add_comm_group A] [algebra F K] [vector_space K A] [vector_space F A] [is_scalar_tower F K A] [finite_dimensional F K] [finite_dimensional K A] :

finite_dimensional F A

source

theorem finite_dimensional.right (F : Type u) (K : Type v) (A : Type w) [field F] [field K] [add_comm_group A] [algebra F K] [vector_space K A] [vector_space F A] [is_scalar_tower F K A] [hf : finite_dimensional F A] :

finite_dimensional K A

source

theorem finite_dimensional.findim_mul_findim (F : Type u) (K : Type v) (A : Type w) [field F] [field K] [add_comm_group A] [algebra F K] [vector_space K A] [vector_space F A] [is_scalar_tower F K A] [finite_dimensional F K] [finite_dimensional K A] :

(finite_dimensional.findim F K) * finite_dimensional.findim K A = finite_dimensional.findim F A

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

source

@[instance]

def finite_dimensional.linear_map (F : Type u) (V : Type v) (W : Type w) [field F] [add_comm_group V] [vector_space F V] [add_comm_group W] [vector_space F W] [finite_dimensional F V] [finite_dimensional F W] :

finite_dimensional F (V →ₗ[F] W)

source

theorem finite_dimensional.findim_linear_map (F : Type u) (V : Type v) (W : Type w) [field F] [add_comm_group V] [vector_space F V] [add_comm_group W] [vector_space F W] [finite_dimensional F V] [finite_dimensional F W] :

finite_dimensional.findim F (V →ₗ[F] W) = (finite_dimensional.findim F V) * finite_dimensional.findim F W

source

@[instance]

def finite_dimensional.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] [vector_space F V] [finite_dimensional F V] :

finite_dimensional K (V →ₗ[F] K)

source

theorem finite_dimensional.findim_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] [vector_space F V] [finite_dimensional F V] :

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