Field.lean

theorem left_finrank_mul_compositum_finrank
    (L K' : IntermediateField K Ω) :
    Module.finrank K L *
        Module.finrank L
          (IntermediateField.extendScalars (show L ≤ L ⊔ K' from le_sup_left)) =
      Module.finrank K (L ⊔ K' : IntermediateField K Ω) := by
  have h := IntermediateField.finrank_bot_mul_relfinrank
    (show L ≤ L ⊔ K' from le_sup_left)
  simpa [IntermediateField.relfinrank_eq_finrank_of_le
    (show L ≤ L ⊔ K' from le_sup_left)] using h

theorem finiteDimensional_compositum_over_right
    (L K' : IntermediateField K Ω)
    [FiniteDimensional K L] [FiniteDimensional K K'] :
    FiniteDimensional K'
      (IntermediateField.extendScalars (show K' ≤ L ⊔ K' from le_sup_right)) := by
  apply FiniteDimensional.of_finrank_pos
  have hformula :=
    DiscreteValuationField.FieldCompositum.right_finrank_mul_compositum_finrank
      (K := K) (Ω := Ω) L K'
  have hsup_pos : 0 < Module.finrank K (L ⊔ K' : IntermediateField K Ω) := by
    let : FiniteDimensional K (L ⊔ K' : IntermediateField K Ω) :=
      IntermediateField.finiteDimensional_sup L K'
    exact Module.finrank_pos
  rw [← hformula] at hsup_pos
  exact Nat.pos_of_mul_pos_left hsup_pos

theorem finiteDimensional_sup_over_right
    (L K' : IntermediateField K Ω)
    [FiniteDimensional K L] [FiniteDimensional K K'] :
    FiniteDimensional K' (L ⊔ K' : IntermediateField K Ω)

theorem sup_finrank_over_left_le_right
    (L K' : IntermediateField K Ω)
    [FiniteDimensional K L] [FiniteDimensional K K'] :
    Module.finrank L (L ⊔ K' : IntermediateField K Ω) ≤
      Module.finrank K K'

theorem relfinrank_intersection_square
    (L K' : IntermediateField K Ω) :
    (L ⊓ K').relfinrank K' * K'.relfinrank (L ⊔ K') =
      (L ⊓ K').relfinrank L * L.relfinrank (L ⊔ K')

theorem relfinrank_intersection_extendScalars_square
    (L K' : IntermediateField K Ω) :
    (L ⊓ K').relfinrank K' *
        Module.finrank K'
          (IntermediateField.extendScalars (show K' ≤ L ⊔ K' from le_sup_right)) =
      (L ⊓ K').relfinrank L *
        Module.finrank L
          (IntermediateField.extendScalars (show L ≤ L ⊔ K' from le_sup_left)) := by
  rw [← IntermediateField.relfinrank_eq_finrank_of_le
      (show K' ≤ L ⊔ K' from le_sup_right),
    ← IntermediateField.relfinrank_eq_finrank_of_le
      (show L ≤ L ⊔ K' from le_sup_left)]
  exact relfinrank_intersection_square L K'

theorem compositum_finrank_over_right_dvd_intersection_product
    (L K' : IntermediateField K Ω) :
    Module.finrank K'
        (IntermediateField.extendScalars (show K' ≤ L ⊔ K' from le_sup_right)) ∣
      (L ⊓ K').relfinrank L *
        Module.finrank L
          (IntermediateField.extendScalars (show L ≤ L ⊔ K' from le_sup_left)) := by
  exact dvd_of_mul_left_eq _
    (relfinrank_intersection_extendScalars_square L K')

theorem compositum_finrank_over_left_dvd_intersection_product
    (L K' : IntermediateField K Ω) :
    Module.finrank L
        (IntermediateField.extendScalars (show L ≤ L ⊔ K' from le_sup_left)) ∣
      (L ⊓ K').relfinrank K' *
        Module.finrank K'
          (IntermediateField.extendScalars (show K' ≤ L ⊔ K' from le_sup_right)) := by
  exact dvd_of_mul_left_eq _
    (relfinrank_intersection_extendScalars_square L K').symm

theorem sup_finrank_over_right_dvd_intersection_product
    (L K' : IntermediateField K Ω) :
    Module.finrank K' (L ⊔ K' : IntermediateField K Ω) ∣
      (L ⊓ K').relfinrank L *
        Module.finrank L (L ⊔ K' : IntermediateField K Ω)

theorem sup_finrank_over_left_eq_right_of_finrank_coprime
    (L K' : IntermediateField K Ω)
    [FiniteDimensional K L] [FiniteDimensional K K']
    (hcop : Nat.Coprime (Module.finrank K L) (Module.finrank K K')) :
    Module.finrank L (L ⊔ K' : IntermediateField K Ω) =
      Module.finrank K K'

theorem isSeparable_compositum_over_right
    (L K' : IntermediateField K Ω)
    [Algebra.IsSeparable K L] [Algebra.IsSeparable K K'] :
    Algebra.IsSeparable K'
      (IntermediateField.extendScalars (show K' ≤ L ⊔ K' from le_sup_right)) := by
  have : Algebra.IsSeparable K
      (IntermediateField.extendScalars (show K' ≤ L ⊔ K' from le_sup_right)) := by
    change Algebra.IsSeparable K
      ((IntermediateField.extendScalars
        (show K' ≤ L ⊔ K' from le_sup_right)).restrictScalars K)
    rw [IntermediateField.extendScalars_restrictScalars]
    infer_instance
  exact Algebra.isSeparable_tower_top_of_isSeparable K K'
    (IntermediateField.extendScalars (show K' ≤ L ⊔ K' from le_sup_right))

theorem isSeparable_compositum_over_left
    (L K' : IntermediateField K Ω)
    [Algebra.IsSeparable K L] [Algebra.IsSeparable K K'] :
    Algebra.IsSeparable L
      (IntermediateField.extendScalars (show L ≤ L ⊔ K' from le_sup_left)) := by
  have : Algebra.IsSeparable K
      (IntermediateField.extendScalars (show L ≤ L ⊔ K' from le_sup_left)) := by
    change Algebra.IsSeparable K
      ((IntermediateField.extendScalars
        (show L ≤ L ⊔ K' from le_sup_left)).restrictScalars K)
    rw [IntermediateField.extendScalars_restrictScalars]
    infer_instance
  exact Algebra.isSeparable_tower_top_of_isSeparable K L
    (IntermediateField.extendScalars (show L ≤ L ⊔ K' from le_sup_left))

theorem isSeparable_sup_over_right
    (L K' : IntermediateField K Ω)
    [Algebra.IsSeparable K L] [Algebra.IsSeparable K K'] :
    Algebra.IsSeparable K' (L ⊔ K' : IntermediateField K Ω)

theorem isSeparable_sup_over_left
    (L K' : IntermediateField K Ω)
    [Algebra.IsSeparable K L] [Algebra.IsSeparable K K'] :
    Algebra.IsSeparable L (L ⊔ K' : IntermediateField K Ω)