Number of embeddings of an algebraic extension of infinite separable degree #

Main results #

Field.Emb.cardinal_eq_two_pow_rank : if E/F is an algebraic separable field extension of infinite degree, then #(Field.Emb F E) = 2 ^ Module.rank F E. This is in contrast to the case of finite degree, where #(Field.Emb F E) = Module.rank F E.
Field.Emb.cardinal_eq_two_pow_sepDegree: more generally, if E/F is an algebraic extension of infinite separable degree, then #(Field.Emb F E) = 2 ^ Field.sepDegree F E.

Sketch of the proof #

We use a transfinite recursive construction that is fairly standard in set theory, but the author has not seen similar arguments elsewhere in mathlib, and some parts proved tricky to formalize.

The extension E/F can be filtered by intermediate fields indexed by a well-order: simply put a well-order on a basis of E/F, and at each step, take the smallest basis element that is not contained in the intermediate field generated by all previous elements, so that they generate a strictly larger intermediate field together. This process can extend all the way to the initial ordinal ι of the cardinal Module.rank F E, because the dimension of the subalgebra generated by an infinite set cannot be greater than the cardinality of the set, and in an algebraic extension, any subalgebra is a field. This is proven as Algebra.rank_adjoin_le and used to show leastExt is a total function from ι to itself. It is probably mathematically the most nontrivial part of the whole argument, but turned out easy to formalize and was done the earliest.

Once we have the filtration E⟮<i⟯ for i : ι, we may build an embedding E →ₐ[F] Ē step by step. To extend an embedding E⟮<i⟯ →ₐ[F] Ē to the successor E⟮<i⁺⟯, the number of choices is equal to the (finite) separable degree of E⟮<i⁺⟯ / E⟮<i⟯, which is equal to its rank if E/F is separable. Since each extension is nontrivial, the degree is at least two (two_le_deg) but always finite. Intuitively, these choices multiply together to give the cardinality of Field.Emb F E := (E →ₐ[F] Ē), and since the total times of choices to be made is the length of the filtration #ι, we conclude that 2 ^ #ι ≤ #(Field.Emb F E) ≤ ℵ₀ ^ #ι, but for infinite #ι both sides are equal, so we get an equality #(Field.Emb F E) = 2 ^ #ι = 2 ^ Module.rank F E.

To rigorize the argument we formalize the choice at step i as a bijection F i⁺ ≃ F i × X i, where X i := Field.Emb E⟮<i⟯ E⟮<i⁺⟯, and we formalize the combination of all choices as the Pi type ∀ i : ι, X i. We use transfinite recursion (SuccOrder.prelimitRecOn) to build a bijection Field.Emb F E ≃ ∀ i, X i with the Pi type by successively extending bijections F i ≃ ∀ j : Iio i, X j using the bijections F i⁺ ≃ F i × X i with product types (InverseSystem.piEquivSucc). More details are found in the file about InverseLimit. Since ι is a limit ordinal, Field.Emb F E ≃ (⊤ →ₐ[F] Ē) is not actually one of the F i because ⊤ is not one of the E⟮<i⟯, so we have to adjoin a top element to ι (WithTop ι) to obtain the bijection Field.Emb F E ≃ F ⊤ ≃ ∀ j : Iio ⊤, X j ≃ ∀ i : ι, X i = ∀ i : ι, Field.Emb E⟮<i⟯ E⟮<i⁺⟯. To make this straightforward, it is crucial that (↑i : WithTop ι)⁺ = ↑(i⁺) holds definitionally.

The predicate IsSuccPrelimit allows us to treat limits and the bottom element uniformly, and the only place the bottom element requires special treatment is in equivLim (the bijection between E⟮<i⟯ →ₐ[F] Ē and the inverse limit of E⟮<j⟯ →ₐ[F] Ē over j < i).