import PaperX.AuxiliaryCyclotomicBaseChange

/-! Auxiliary cyclic cyclotomic extensions over arbitrary number fields. -/
set_option autoImplicit false
noncomputable section
namespace PaperX.AuxiliaryCyclotomicGeneralBase
open IntermediateField AuxiliaryCyclotomicDisjoint AuxiliaryCyclotomicExistence
  AuxiliaryCyclotomicBaseChange

variable (M : Type*) [Field M] [CharZero M] [IsAlgClosed M]
  [Algebra.IsAlgebraic ℚ M]

omit [Algebra.IsAlgebraic ℚ M] in
/-- The base change of a prime cyclotomic field is generated by an actual
primitive root of unity in the same ambient algebraic closure. -/
theorem compositumOver_primeCyclotomic (K : IntermediateField ℚ M) (p : Nat.Primes) :
    ∃ z : M, IsPrimitiveRoot z (p : ℕ) ∧
      compositumOver K (primeCyclotomicPart M p) = IntermediateField.adjoin K {z} := by
  let : NeZero (p : ℕ) := ⟨p.property.ne_zero⟩
  let z : M := Classical.choose (HasEnoughRootsOfUnity.exists_primitiveRoot M (p : ℕ))
  have hz : IsPrimitiveRoot z (p : ℕ) :=
    Classical.choose_spec (HasEnoughRootsOfUnity.exists_primitiveRoot M (p : ℕ))
  refine ⟨z, hz, ?_⟩
  rw [compositumOver_eq_adjoin]
  change IntermediateField.adjoin K (IntermediateField.adjoin ℚ {z} : Set M) = _
  exact IntermediateField.adjoin_adjoin_right (F := K) (K := ℚ) (S := ({z} : Set M))

/-- The needed auxiliary cyclic degree-n extension exists over any number field K
inside L. It is disjoint from L over K and lies in K(zeta_q) for an actual prime q.
No auxiliary extension or disjointness is supplied in the hypotheses. -/
theorem exists_cyclic_cyclotomic_disjoint_over
    (K L : IntermediateField ℚ M) [NumberField K] [NumberField L]
    (hKL : K ≤ L) (n : ℕ) [NeZero n] (forbidden : Finset ℕ) (bound : ℕ) :
    ∃ p : Nat.Primes, ∃ z : M, ∃ B : IntermediateField K M,
      bound < (p : ℕ) ∧ (p : ℕ) ∉ forbidden ∧ IsPrimitiveRoot z (p : ℕ) ∧
      B ≤ IntermediateField.adjoin K {z} ∧ Module.finrank K B = n ∧
      IsGalois K B ∧ IsCyclic Gal(B/K) ∧
      B.LinearDisjoint (IntermediateField.extendScalars hKL) := by
  obtain ⟨p, A, hp, hpnot, hA, hdeg, hgal, hcyc, hdis⟩ :=
    exists_cyclic_cyclotomic_disjoint M L n forbidden bound
  have : FiniteDimensional ℚ A :=
    Module.finite_of_finrank_pos (by rw [hdeg]; exact NeZero.pos n)
  obtain ⟨z, hz, hfield⟩ := compositumOver_primeCyclotomic M K p
  let B := compositumOver K A
  have hB : B ≤ compositumOver K (primeCyclotomicPart M p) := by
    simp only [B, compositumOver_eq_adjoin]
    exact IntermediateField.adjoin.mono K _ _ hA
  refine ⟨p, z, B, hp, hpnot, hz, hfield ▸ hB, ?_, ?_, ?_, ?_⟩
  · exact (compositumOver_finrank K A (hdis.of_le_right hKL)).trans hdeg
  · exact compositumOver_isGalois K A
  · exact compositumOver_isCyclic K A
  · exact compositumOver_linearDisjoint K A L hKL hdis

end PaperX.AuxiliaryCyclotomicGeneralBase