Counting the intermediate fields isomorphic to a given field

Let E / K and Ω / K be field extensions. Every K-embedding φ : E →ₐ[K] Ω is an isomorphism onto its image φ.fieldRange, and the intermediate fields of Ω / K arising this way are exactly those K-isomorphic to E. Two embeddings with the same image differ by a unique K-automorphism of E, so the embeddings are partitioned by their images into fibres that are torsors under E ≃ₐ[K] E. Counting gives

#{M : IntermediateField K Ω | M ≃ₐ[K] E} · #Aut_K(E) = #Hom_K(E, Ω).

For a finite separable extension E / K and a separably closed Ω, the right-hand side is [E : K]. This is the form in which Serre's mass formula regroups the totally ramified extensions of a local field inside a separable closure along their isomorphism classes.

Main definitions

• IntermediateField.algHomFieldRangeEquiv M: the K-embeddings of E into Ω with image M are the K-isomorphisms E ≃ₐ[K] M.

Main results

• IntermediateField.ncard_isomorphic_mul_natCard_algEquiv: the number of intermediate fields of Ω / K that are K-isomorphic to E, times the number of K-automorphisms of E, is the number of K-embeddings of E into Ω. No finiteness hypothesis is needed, since Nat.card and Set.ncard take the value 0 on infinite types and sets on both sides at once.
• IntermediateField.ncard_isomorphic_mul_natCard_algEquiv_of_isSepClosed: for E / K finite separable and Ω separably closed, the same product is [E : K].
• IntermediateField.setOf_isomorphic_eq_singleton_of_normal: a normal intermediate field is K-isomorphic to no other intermediate field.

noncomputable def IntermediateField.algHomFieldRangeEquiv {K : Type u_1} {E : Type u_2} {Ω : Type u_3} [Field K] [Field E] [Field Ω] [Algebra K E] [Algebra K Ω] (M : IntermediateField K Ω) : { φ : E →ₐ[K] Ω // φ.fieldRange = M } ≃ E ≃ₐ[K] ↥M

The K-embeddings of E into Ω whose image is the intermediate field M correspond to the K-isomorphisms from E onto M: an embedding is sent to its corestriction, and an isomorphism e to M.val.comp e.

@[simp]

theorem IntermediateField.coe_algHomFieldRangeEquiv_apply {K : Type u_1} {E : Type u_2} {Ω : Type u_3} [Field K] [Field E] [Field Ω] [Algebra K E] [Algebra K Ω] (M : IntermediateField K Ω) (φ : { φ : E →ₐ[K] Ω // φ.fieldRange = M }) (x : E) : ↑((M.algHomFieldRangeEquiv φ) x) = ↑φ x

algHomFieldRangeEquiv corestricts an embedding to its image.

@[simp]

theorem IntermediateField.coe_algHomFieldRangeEquiv_symm_apply {K : Type u_1} {E : Type u_2} {Ω : Type u_3} [Field K] [Field E] [Field Ω] [Algebra K E] [Algebra K Ω] (M : IntermediateField K Ω) (e : E ≃ₐ[K] ↥M) : ↑(M.algHomFieldRangeEquiv.symm e) = M.val.comp ↑e

The inverse of algHomFieldRangeEquiv composes an isomorphism onto M with the inclusion of M.

theorem IntermediateField.ncard_isomorphic_mul_natCard_algEquiv (K : Type u_1) (E : Type u_2) (Ω : Type u_3) [Field K] [Field E] [Field Ω] [Algebra K E] [Algebra K Ω] : {M : IntermediateField K Ω | Nonempty (E ≃ₐ[K] ↥M)}.ncard * Nat.card Gal(E/K) = Nat.card (E →ₐ[K] Ω)

The orbit count for embeddings. The intermediate fields of Ω / K that are K-isomorphic to E, counted with the K-automorphisms of E, account for every K-embedding of E into Ω exactly once: an embedding is determined by its image M together with an isomorphism E ≃ₐ[K] M, and each such M admits exactly #Aut_K(E) of them.

theorem IntermediateField.ncard_isomorphic_mul_natCard_algEquiv_of_isSepClosed (K : Type u_1) (E : Type u_2) (Ω : Type u_3) [Field K] [Field E] [Field Ω] [Algebra K E] [Algebra K Ω] [IsSepClosed Ω] [FiniteDimensional K E] [Algebra.IsSeparable K E] : {M : IntermediateField K Ω | Nonempty (E ≃ₐ[K] ↥M)}.ncard * Nat.card Gal(E/K) = Module.finrank K E

The orbit count in a separably closed field. For a finite separable extension E / K and a separably closed Ω, the intermediate fields of Ω / K that are K-isomorphic to E, counted with the K-automorphisms of E, number [E : K].

theorem IntermediateField.setOf_isomorphic_eq_singleton_of_normal {K : Type u_1} {Ω : Type u_3} [Field K] [Field Ω] [Algebra K Ω] (L : IntermediateField K Ω) [Normal K ↥L] : {M : IntermediateField K Ω | Nonempty (↥L ≃ₐ[K] ↥M)} = {L}

A normal intermediate field is the only intermediate field K-isomorphic to it: every K-embedding of a normal extension into Ω has the same image.