Degree for compositum of fields

Stream: Is there code for X?

[Dion Leijnse]

Let L1 and L2 be two intermediate fields of a field extension K/k. Assume that L1 is algebraic over k. The compositum of L1 and L2 is given by L1 ⊔ L2, and I am trying to prove that the degrees satisfy [L1 ⊔ L2 : L1] ≤ [L1 : k]. I am trying to prove this by using IntermediateField.adjoin_rank_le_of_isAlgebraic_right, but I am stuck on the following sorry:

import Mathlib


variable {k K : Type} [Field k] [Field K] [Algebra k K]
variable (L1 L2 : IntermediateField k K)

instance : Module L1 (L1 ⊔ L2 : IntermediateField k K) := RingHom.toModule
    (IntermediateField.inclusion le_sup_left).toRingHom

lemma compositum_deg_le (L1 L2 : IntermediateField k K) (hAlg : Algebra.IsAlgebraic k L2) :
    Module.rank L1 (L1 ⊔ L2 : IntermediateField k K) ≤ Module.rank k L2 := by
  let isom : (L1 ⊔ L2 : IntermediateField k K) ≃ₗ[L1]
      (IntermediateField.adjoin L1 (L2 : Set K)) := by

    -- simp only [IntermediateField.sup_def]
    -- rw [← IntermediateField.adjoin_adjoin_left]
    sorry
  have hRankEq : Module.rank L1 (L1 ⊔ L2 : IntermediateField k K) =
      Module.rank L1 (IntermediateField.adjoin L1 (L2 : Set K)) := LinearEquiv.rank_eq isom
  rw [hRankEq]
  exact IntermediateField.adjoin_rank_le_of_isAlgebraic_right _ _

The problem while proving this sorry is that there are some results that seem useful, at least set-theoretically I should be able to get there by using IntermediateField.sup_def, IntermediateField.adjoin_adjoin_left and Algebra.adjoin_eq. However, this chain of equalities does not work well with the structure as an L1-module, and I haven't been able to get this to work. Is there an easy way to prove this?

[Junyan Xu]

This works:

  let isom : (L1 ⊔ L2 : IntermediateField k K) ≃ₗ[L1]
      (IntermediateField.adjoin L1 (L2 : Set K)) :=
    { __ := Equiv.setCongr <| by
        ext; simp only [IntermediateField.sup_def]
        rw [← IntermediateField.restrictScalars_adjoin]
        rfl -- or simp_rw [SetLike.mem_coe, IntermediateField.mem_restrictScalars]
      map_add' _ _ := rfl
      map_smul' _ _ := rfl }

[Dion Leijnse]

Thanks!