Separable extensions over separably closed fields

TheoremNumber of embeddings into a separably closed field#✓fully proved

Let \(L/K\) be a finite separable field extension and let \(\Omega\) be a separably closed field that is a \(K\)-algebra. Then the number of \(K\)-algebra homomorphisms \(L \to \Omega\) equals the degree \([L : K]\).

theorem algHom_card_eq_finrank_of_isSepClosed :
    Fintype.card (L →ₐ[K] Ω) = Module.finrank K L

Used by 2

Used byEmbeddings evaluated on a basis · Dimensions of the two sides of the splitting

DefinitionEvaluation of embeddings at an element#✓fully proved

Let \(L/K\) be a finite separable field extension, let \(\Omega\) be a separably closed field that is a \(K\)-algebra, and write \(\mathrm{Hom}_K(L, \Omega)\) for the set of \(K\)-algebra homomorphisms \(L \to \Omega\). The evaluation map is the \(K\)-algebra homomorphism from \(L\) to the algebra of functions \(\mathrm{Hom}_K(L, \Omega) \to \Omega\) sending \(l \in L\) to the function \(\sigma \mapsto \sigma(l)\).

def sepClosedEvalAlgHom : L →ₐ[K] ((L →ₐ[K] Ω) → Ω) where
  toFun l σ := σ l
  map_one' := by ext; simp
  map_mul' := by intros; ext; simp
  map_zero' := by ext; simp
  map_add' := by intros; ext; simp
  commutes' := by intro r; ext σ; simp

Used by 1

Used byEvaluation map on the base change to a separably closed field

DefinitionEvaluation map on the base change to a separably closed field#✓fully proved

Let \(L / K\) be a finite separable field extension and let \(\Omega\) be a separably closed field extension of \(K\). This is the homomorphism of \(\Omega\)-algebras from \(\Omega \otimes_K L\) to the algebra of functions from the set of \(K\)-algebra homomorphisms \(L \to \Omega\) to \(\Omega\), which sends each pure tensor \(\omega \otimes l\) to the function \(\sigma \mapsto \omega \, \sigma(l)\).

def sepClosedTensorHom : (Ω ⊗[K] L) →ₐ[Ω] ((L →ₐ[K] Ω) → Ω) :=
  Algebra.TensorProduct.productLeftAlgHom (Algebra.ofId Ω _)
    (sepClosedEvalAlgHom K L Ω)

Uses 1 · Used by 4

Statement usesEvaluation of embeddings at an element

Used bySplitting of a separable extension over a separably closed field · Bijectivity of the evaluation homomorphism · Injectivity of the evaluation homomorphism · Surjectivity of the evaluation homomorphism

TheoremDedekind independence of embeddings#✓fully proved

Let \(K\), \(L\) and \(\Omega\) be fields such that \(L\) and \(\Omega\) are \(K\)-algebras. Then the \(K\)-algebra homomorphisms \(L \to \Omega\), viewed as functions \(L \to \Omega\), are linearly independent over \(\Omega\).

This is an instance of Dedekind's theorem on the linear independence of characters.

theorem algHom_linearIndependent :
    LinearIndependent Ω (fun (σ : L →ₐ[K] Ω) (l : L) => σ l)

Used by 1

Used byEmbeddings evaluated on a basis

TheoremEmbeddings evaluated on a basis#✓fully proved

Let \(L/K\) be a finite separable field extension of degree \(n\), let \(\Omega\) be a separably closed field that is a \(K\)-algebra, and write \(\mathrm{Hom}_K(L, \Omega)\) for the set of \(K\)-algebra homomorphisms \(L \to \Omega\). Let \(b_1, \dots, b_n\) be a fixed basis of \(L\) over \(K\) (one particular basis chosen once and for all, not an arbitrary one). Then the \(n\) functions \(\mathrm{Hom}_K(L, \Omega) \to \Omega\) given by \(\varphi \mapsto \varphi(b_i)\), for \(i = 1, \dots, n\), are linearly independent over \(\Omega\).

theorem column_functions_linearIndependent :
    LinearIndependent Ω
      (fun (i : Fin (Module.finrank K L)) (φ : L →ₐ[K] Ω) =>
        φ (Module.finBasis K L i))

Uses 2 · Used by 1

Proof usesNumber of embeddings into a separably closed field · Dedekind independence of embeddings

Used byInjectivity of the evaluation homomorphism

TheoremInjectivity of the evaluation homomorphism#✓fully proved

Let \(L/K\) be a finite separable field extension, let \(\Omega\) be a separably closed field that is a \(K\)-algebra, and write \(\mathrm{Hom}_K(L, \Omega)\) for the set of \(K\)-algebra homomorphisms \(L \to \Omega\). Then the evaluation homomorphism of \(\Omega\)-algebras from \(\Omega \otimes_K L\) to the algebra of functions \(\mathrm{Hom}_K(L, \Omega) \to \Omega\), which sends \(\omega \otimes l\) to the function \(\sigma \mapsto \omega\, \sigma(l)\), is injective.

theorem sepClosedTensorHom_injective :
    Function.Injective (sepClosedTensorHom K L Ω)

Uses 2 · Used by 2

Statement usesEvaluation map on the base change to a separably closed field

Proof usesEmbeddings evaluated on a basis

Used byBijectivity of the evaluation homomorphism · Surjectivity of the evaluation homomorphism

TheoremDimensions of the two sides of the splitting#✓fully proved

Let \(L/K\) be a finite separable field extension, let \(\Omega\) be a separably closed field that is a \(K\)-algebra, and write \(\mathrm{Hom}_K(L, \Omega)\) for the set of \(K\)-algebra homomorphisms \(L \to \Omega\). Then the base change \(\Omega \otimes_K L\) and the space of functions \(\mathrm{Hom}_K(L, \Omega) \to \Omega\) have the same dimension as vector spaces over \(\Omega\).

Both dimensions equal the degree \([L : K]\).

theorem finrank_tensor_eq_finrank_pi_of_isSepClosed :
    Module.finrank Ω (Ω ⊗[K] L) = Module.finrank Ω ((L →ₐ[K] Ω) → Ω)

Uses 1 · Used by 1

Proof usesNumber of embeddings into a separably closed field

Used bySurjectivity of the evaluation homomorphism

TheoremSurjectivity of the evaluation homomorphism#✓fully proved

Let \(L/K\) be a finite separable field extension, let \(\Omega\) be a separably closed field that is a \(K\)-algebra, and write \(\mathrm{Hom}_K(L, \Omega)\) for the set of \(K\)-algebra homomorphisms \(L \to \Omega\). Then the evaluation homomorphism of \(\Omega\)-algebras from \(\Omega \otimes_K L\) to the algebra of functions \(\mathrm{Hom}_K(L, \Omega) \to \Omega\), which sends \(\omega \otimes l\) to the function \(\sigma \mapsto \omega\, \sigma(l)\), is surjective.

This follows from injectivity, since both sides have dimension \([L : K]\) over \(\Omega\).

theorem sepClosedTensorHom_surjective :
    Function.Surjective (sepClosedTensorHom K L Ω)

Uses 3 · Used by 1

Statement usesEvaluation map on the base change to a separably closed field

Proof usesDimensions of the two sides of the splitting · Injectivity of the evaluation homomorphism

Used byBijectivity of the evaluation homomorphism

TheoremBijectivity of the evaluation homomorphism#✓fully proved

Let \(L/K\) be a finite separable field extension, let \(\Omega\) be a separably closed field that is a \(K\)-algebra, and write \(\mathrm{Hom}_K(L, \Omega)\) for the set of \(K\)-algebra homomorphisms \(L \to \Omega\). Then the evaluation homomorphism of \(\Omega\)-algebras from \(\Omega \otimes_K L\) to the algebra of functions \(\mathrm{Hom}_K(L, \Omega) \to \Omega\), which sends \(\omega \otimes l\) to the function \(\sigma \mapsto \omega\, \sigma(l)\), is bijective.

theorem sepClosedTensorHom_bijective :
    Function.Bijective (sepClosedTensorHom K L Ω)

Uses 3 · Used by 1

Statement usesEvaluation map on the base change to a separably closed field

Proof usesInjectivity of the evaluation homomorphism · Surjectivity of the evaluation homomorphism

Used bySplitting of a separable extension over a separably closed field

DefinitionSplitting of a separable extension over a separably closed field#✓fully proved

Let \(L/K\) be a finite separable field extension, let \(\Omega\) be a separably closed field that is a \(K\)-algebra, and write \(\mathrm{Hom}_K(L, \Omega)\) for the set of \(K\)-algebra homomorphisms \(L \to \Omega\). The splitting isomorphism is the isomorphism of \(\Omega\)-algebras from \(\Omega \otimes_K L\) onto the algebra \(\Omega^{\mathrm{Hom}_K(L, \Omega)}\) of functions \(\mathrm{Hom}_K(L, \Omega) \to \Omega\) given by the evaluation homomorphism, which sends \(\omega \otimes l\) to the function \(\sigma \mapsto \omega\, \sigma(l)\) and is bijective.

noncomputable def sepClosedAlgEquiv : (Ω ⊗[K] L) ≃ₐ[Ω] ((L →ₐ[K] Ω) → Ω) :=
  AlgEquiv.ofBijective (sepClosedTensorHom K L Ω)
    (sepClosedTensorHom_bijective K L Ω)

Sources

• ATLAS NumberTheoryI Proposition 4.43, field case; the book states it for finite étale \(K\)-algebras.

Uses 2 · Used by 1

Statement usesEvaluation map on the base change to a separably closed field · Bijectivity of the evaluation homomorphism

Used byThe splitting isomorphism on pure tensors

TheoremThe splitting isomorphism on pure tensors#✓fully proved

Let \(L/K\) be a finite separable field extension, let \(\Omega\) be a separably closed field that is a \(K\)-algebra, and write \(\mathrm{Hom}_K(L, \Omega)\) for the set of \(K\)-algebra homomorphisms \(L \to \Omega\). For all \(\omega \in \Omega\) and \(l \in L\), the splitting isomorphism from \(\Omega \otimes_K L\) onto the algebra \(\Omega^{\mathrm{Hom}_K(L, \Omega)}\) of functions \(\mathrm{Hom}_K(L, \Omega) \to \Omega\) sends \(\omega \otimes l\) to the function \(\sigma \mapsto \omega\, \sigma(l)\).

theorem sepClosedAlgEquiv_apply (ω : Ω) (l : L) :
    sepClosedAlgEquiv K L Ω (ω ⊗ₜ[K] l) = fun σ => ω * σ l

Uses 1

Statement usesSplitting of a separable extension over a separably closed field

11 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.