CanonicalKummerNorm.lean

theorem norm_prod_apply
    (K S T : Type) [Field K] [CommRing S] [CommRing T]
    [Algebra K S] [Algebra K T]
    [Module.Free K S] [Module.Finite K S]
    [Module.Free K T] [Module.Finite K T]
    (x : S × T) :
    Algebra.norm K x = Algebra.norm K x.1 * Algebra.norm K x.2

theorem adjoinRoot_norm_iff_chosenSimpleKummerNorm_of_irreducible
    (K : Type) [Field K] (n : ℕ+) (hnK : ((n : ℕ) : K) ≠ 0)
    (a b : Kˣ)
    (hirr : Irreducible
      (Polynomial.X ^ (n : ℕ) - Polynomial.C (a : K))) :
    (∃ y : (AdjoinRoot
          (Polynomial.X ^ (n : ℕ) - Polynomial.C (a : K)))ˣ,
        Algebra.norm K
          (y : AdjoinRoot
            (Polynomial.X ^ (n : ℕ) - Polynomial.C (a : K))) = (b : K)) ↔
      ∃ y : (KummerTheory.chosenSimpleKummerExtension K n hnK a)ˣ,
        Algebra.norm K
          (y : KummerTheory.chosenSimpleKummerExtension K n hnK a) = (b : K)

theorem adjoinRoot_decompose_chosenMinpoly
    (K : Type) [Field K] (n : ℕ+) (hnK : ((n : ℕ) : K) ≠ 0)
    (a : Kˣ) :
    let p : Polynomial K := Polynomial.X ^ (n : ℕ) - Polynomial.C (a : K)
    let q : Polynomial K :=
      minpoly K (KummerTheory.chosenSimpleKummerRoot K n hnK a)
    ∃ r : Polynomial K, p = q * r ∧ IsCoprime q r ∧
      Nonempty (AdjoinRoot p ≃ₐ[K] (AdjoinRoot q × AdjoinRoot r)) := by
  let β : SeparableClosure K := KummerTheory.chosenSimpleKummerRoot K n hnK a
  let p : Polynomial K := Polynomial.X ^ (n : ℕ) - Polynomial.C (a : K)
  let q : Polynomial K := minpoly K β
  have hβ : Polynomial.aeval β p = 0 := by
    simp only [p, map_sub, map_pow, Polynomial.aeval_X, Polynomial.aeval_C,
      β, KummerTheory.chosenSimpleKummerRoot_pow, sub_self]
  obtain ⟨r, hr⟩ := minpoly.dvd K β hβ
  have hsep : p.Separable := by
    exact Polynomial.separable_X_pow_sub_C (a : K) hnK (Units.ne_zero a)
  have hcoprime : IsCoprime q r := by
    apply Polynomial.Separable.isCoprime
    rw [← hr]
    exact hsep
  let I : Ideal (Polynomial K) := Ideal.span {q}
  let J : Ideal (Polynomial K) := Ideal.span {r}
  have hIJ : Ideal.span ({p} : Set (Polynomial K)) = I * J := by
    change Ideal.span {p} = Ideal.span {q} * Ideal.span {r}
    rw [Ideal.span_singleton_mul_span_singleton, hr]
  have hIcoprime : IsCoprime I J :=
    (Ideal.isCoprime_span_singleton_iff q r).2 hcoprime
  let eRing : AdjoinRoot p ≃+* (AdjoinRoot q × AdjoinRoot r) :=
    (Ideal.quotEquivOfEq hIJ).trans
      (Ideal.quotientMulEquivQuotientProd I J hIcoprime)
  let e : AdjoinRoot p ≃ₐ[K] (AdjoinRoot q × AdjoinRoot r) :=
    AlgEquiv.ofRingEquiv (f := eRing) (fun _ => rfl)
  exact ⟨r, hr, hcoprime, ⟨e⟩⟩

theorem adjoinRoot_norm_decompose_chosenMinpoly
    (K : Type) [Field K] (n : ℕ+) (hnK : ((n : ℕ) : K) ≠ 0)
    (a : Kˣ) :
    let p : Polynomial K := Polynomial.X ^ (n : ℕ) - Polynomial.C (a : K)
    let E := KummerTheory.chosenSimpleKummerExtension K n hnK a
    ∃ (r : Polynomial K), r.Monic ∧ r ∣ p ∧
      ∃ e : AdjoinRoot p ≃ₐ[K] (E × AdjoinRoot r),
        ∀ y : AdjoinRoot p,
          Algebra.norm K y =
            Algebra.norm K (e y).1 * Algebra.norm K (e y).2 := by
  let β : SeparableClosure K := KummerTheory.chosenSimpleKummerRoot K n hnK a
  let p : Polynomial K := Polynomial.X ^ (n : ℕ) - Polynomial.C (a : K)
  let q : Polynomial K := minpoly K β
  let E := KummerTheory.chosenSimpleKummerExtension K n hnK a
  obtain ⟨r, hr, -, ⟨e₀⟩⟩ :=
    adjoinRoot_decompose_chosenMinpoly K n hnK a
  have hβint : IsIntegral K β := by
    apply IsIntegral.of_pow n.pos
    rw [show β ^ (n : ℕ) = algebraMap K (SeparableClosure K) (a : K) from
      KummerTheory.chosenSimpleKummerRoot_pow K n hnK a]
    exact isIntegral_algebraMap
  let e₁ : AdjoinRoot q ≃ₐ[K] E :=
    IntermediateField.adjoinRootEquivAdjoin K hβint
  let e : AdjoinRoot p ≃ₐ[K] (E × AdjoinRoot r) :=
    e₀.trans (AlgEquiv.prodCongr e₁ AlgEquiv.refl)
  have hpmonic : p.Monic :=
    Polynomial.monic_X_pow_sub_C (a : K) n.pos.ne'
  have hqmonic : q.Monic := minpoly.monic hβint
  have hrmonic : r.Monic := by
    apply hqmonic.of_mul_monic_left
    rw [← hr]
    exact hpmonic
  have : Module.Finite K E :=
    KummerTheory.chosenSimpleKummerExtension_finiteDimensional K n hnK a
  have : Module.Free K (AdjoinRoot r) := hrmonic.free_adjoinRoot
  have : Module.Finite K (AdjoinRoot r) := hrmonic.finite_adjoinRoot
  have hrdiv : r ∣ p := by
    refine ⟨q, ?_⟩
    exact hr.trans (mul_comm q r)
  refine ⟨r, hrmonic, hrdiv, e, ?_⟩
  intro y
  calc
    Algebra.norm K y = Algebra.norm K (e y) :=
      (Algebra.norm_eq_of_algEquiv e y).symm
    _ = Algebra.norm K (e y).1 * Algebra.norm K (e y).2 :=
      norm_prod_apply K E (AdjoinRoot r) (e y)

theorem adjoin_root_eq_top_of_pow_eq
    (K : Type) [Field K] (n : ℕ+) (hnK : ((n : ℕ) : K) ≠ 0)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty) (a : Kˣ)
    (γ : KummerTheory.chosenSimpleKummerExtension K n hnK a)
    (hγ : γ ^ (n : ℕ) =
      algebraMap K (KummerTheory.chosenSimpleKummerExtension K n hnK a) (a : K)) :
    IntermediateField.adjoin K {γ} = ⊤

theorem adjoinRoot_factor_equiv_chosenSimpleKummer
    (K : Type) [Field K] (n : ℕ+) (hnK : ((n : ℕ) : K) ≠ 0)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty) (a : Kˣ)
    (f : Polynomial K) (hfmonic : f.Monic) (hfirr : Irreducible f)
    (hfp : f ∣ Polynomial.X ^ (n : ℕ) - Polynomial.C (a : K)) :
    Nonempty (AdjoinRoot f ≃ₐ[K]
      KummerTheory.chosenSimpleKummerExtension K n hnK a)

theorem adjoinRoot_norm_decompose_coprime
    (K : Type) [Field K] (q r : Polynomial K)
    (hq : q.Monic) (hr : r.Monic) (hqr : IsCoprime q r) :
    ∃ e : AdjoinRoot (q * r) ≃ₐ[K] (AdjoinRoot q × AdjoinRoot r),
      ∀ y : AdjoinRoot (q * r),
        Algebra.norm K y =
          Algebra.norm K (e y).1 * Algebra.norm K (e y).2

theorem adjoinRoot_factor_norm_is_chosenSimpleKummerNorm
    (K : Type) [Field K] (n : ℕ+) (hnK : ((n : ℕ) : K) ≠ 0)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty) (a : Kˣ)
    (f : Polynomial K) (hfmonic : f.Monic)
    (hfp : f ∣ Polynomial.X ^ (n : ℕ) - Polynomial.C (a : K))
    (y : (AdjoinRoot f)ˣ) :
    ∃ z : (KummerTheory.chosenSimpleKummerExtension K n hnK a)ˣ,
      Algebra.norm K (y : AdjoinRoot f) =
        Algebra.norm K
          (z : KummerTheory.chosenSimpleKummerExtension K n hnK a)

theorem adjoinRoot_norm_iff_chosenSimpleKummerNorm
    (K : Type) [Field K] (n : ℕ+) (hnK : ((n : ℕ) : K) ≠ 0)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty) (a b : Kˣ) :
    (∃ y : (AdjoinRoot
          (Polynomial.X ^ (n : ℕ) - Polynomial.C (a : K)))ˣ,
        Algebra.norm K
          (y : AdjoinRoot
            (Polynomial.X ^ (n : ℕ) - Polynomial.C (a : K))) = (b : K)) ↔
      ∃ z : (KummerTheory.chosenSimpleKummerExtension K n hnK a)ˣ,
        Algebra.norm K
          (z : KummerTheory.chosenSimpleKummerExtension K n hnK a) = (b : K)