UniqueExtensionReduction.lean

theorem monic_splits_in_extension_valuationSubring
    {K L : Type*} [Field K] [Field L] [Algebra K L]
    (V : ValuationSubring K) (W : ValuationSubring L)
    [hW : V.valuation.HasExtension W.valuation]
    (F : Polynomial V) (hFmonic : F.Monic)
    (hsplit : (F.map ((algebraMap K L).comp V.subtype)).Splits) :
    (F.map (valuationSubringMapOfHasExtension V W hW)).Splits

theorem monic_eq_prod_monic_irreducible_map_factors
    {K : Type*} [Field K] (V : ValuationSubring K)
    (f : Polynomial V) (hf : f.Monic) :
    ∃ factors : Multiset (Polynomial V),
      (∀ Q ∈ factors, Q.Monic ∧ Irreducible (Q.map V.subtype)) ∧
        factors.prod = f

theorem residueFieldMapOfHasExtension_residue
    {K L : Type*} [Field K] [Field L] [Algebra K L]
    (V : ValuationSubring K) (W : ValuationSubring L)
    (hW : V.valuation.HasExtension W.valuation) (x : V) :
    residueFieldMapOfHasExtension V W hW (IsLocalRing.residue V x) =
      IsLocalRing.residue W (valuationSubringMapOfHasExtension V W hW x)

theorem monic_reduction_splits_in_extension_residueField
    {K L : Type*} [Field K] [Field L] [Algebra K L]
    (V : ValuationSubring K) (W : ValuationSubring L)
    [hW : V.valuation.HasExtension W.valuation]
    (F : Polynomial V) (hFmonic : F.Monic)
    (hsplit : (F.map ((algebraMap K L).comp V.subtype)).Splits) :
    ((F.map (IsLocalRing.residue V)).map
      (residueFieldMapOfHasExtension V W hW)).Splits

theorem residues_of_irreducible_roots_are_conjugate
    {K L : Type*} [Field K] [Field L] [Algebra K L] [Normal K L]
    (V : ValuationSubring K) (W : ValuationSubring L)
    (hW : V.valuation.HasExtension W.valuation)
    (huniq : ∀ W' : ValuationSubring L,
      V.valuation.HasExtension W'.valuation → W' = W)
    (F : Polynomial V)
    (hirr : Irreducible (F.map V.subtype))
    {a b : W}
    (ha : (F.map (valuationSubringMapOfHasExtension V W hW)).eval a = 0)
    (hb : (F.map (valuationSubringMapOfHasExtension V W hW)).eval b = 0) :
    ∃ σ : L ≃ₐ[K] L,
      residueFieldEquivOfUniqueExtension V W hW huniq σ
          (IsLocalRing.residue W b) =
        IsLocalRing.residue W a

theorem irreducible_monic_reduction_coprime_factor_degree_zero
    {K L : Type*} [Field K] [Field L] [Algebra K L]
    (V : ValuationSubring K) (W : ValuationSubring L)
    [hW : V.valuation.HasExtension W.valuation]
    (huniq : ∀ W' : ValuationSubring L,
      V.valuation.HasExtension W'.valuation → W' = W)
    (F : Polynomial V) (hFmonic : F.Monic)
    (hirr : Irreducible (F.map V.subtype))
    [IsSplittingField K L (F.map V.subtype)]
    (gbar hbar : Polynomial (IsLocalRing.ResidueField V))
    (hfactor : F.map (IsLocalRing.residue V) = gbar * hbar)
    (hcoprime : IsCoprime gbar hbar) :
    gbar.natDegree = 0 ∨ hbar.natDegree = 0

theorem irreducible_monic_reduction_dvd_left_or_right_of_coprime
    {K L : Type*} [Field K] [Field L] [Algebra K L]
    (V : ValuationSubring K) (W : ValuationSubring L)
    [hW : V.valuation.HasExtension W.valuation]
    (huniq : ∀ W' : ValuationSubring L,
      V.valuation.HasExtension W'.valuation → W' = W)
    (Q : Polynomial V) (hQmonic : Q.Monic)
    (hQirr : Irreducible (Q.map V.subtype))
    [IsSplittingField K L (Q.map V.subtype)]
    (gbar hbar : Polynomial (IsLocalRing.ResidueField V))
    (hcoprime : IsCoprime gbar hbar)
    (hQdvd : Q.map (IsLocalRing.residue V) ∣ gbar * hbar) :
    Q.map (IsLocalRing.residue V) ∣ gbar ∨
      Q.map (IsLocalRing.residue V) ∣ hbar

theorem partition_monic_irreducible_factors_along_coprime_reduction
    {K : Type u} [Field K] (V : ValuationSubring K)
    (hunique : ∀ (E : Type u) [Field E] [Algebra K E]
      [Algebra.IsAlgebraic K E],
        ∃! W : ValuationSubring E,
          V.valuation.HasExtension W.valuation)
    (factors : Multiset (Polynomial V))
    (hfactors : ∀ Q ∈ factors,
      Q.Monic ∧ Irreducible (Q.map V.subtype))
    (gbar hbar : Polynomial (IsLocalRing.ResidueField V))
    (hgmonic : gbar.Monic) (hhmonic : hbar.Monic)
    (hproduct :
      (factors.map (fun Q => Q.map (IsLocalRing.residue V))).prod =
        gbar * hbar)
    (hcoprime : IsCoprime gbar hbar) :
    ∃ G H : Polynomial V,
      G.Monic ∧ H.Monic ∧ factors.prod = G * H ∧
        G.map (IsLocalRing.residue V) = gbar ∧
          H.map (IsLocalRing.residue V) = hbar := by
  classical
  induction factors using Multiset.induction_on generalizing gbar hbar with
  | empty =>
      have hgh : gbar * hbar = 1 := by simpa using hproduct.symm
      have hgunit : IsUnit gbar :=
        isUnit_iff_exists_inv'.2 ⟨hbar, by simpa [mul_comm] using hgh⟩
      have hhunit : IsUnit hbar :=
        isUnit_iff_exists_inv'.2 ⟨gbar, hgh⟩
      have hg : gbar = 1 := hgmonic.isUnit_iff.1 hgunit
      have hh : hbar = 1 := hhmonic.isUnit_iff.1 hhunit
      subst gbar
      subst hbar
      exact ⟨1, 1, Polynomial.monic_one, Polynomial.monic_one, by simp, by simp, by simp⟩
  | cons Q factors ih =>
      have hQdata : Q.Monic ∧ Irreducible (Q.map V.subtype) :=
        hfactors Q (by simp)
      have htail : ∀ R ∈ factors,
          R.Monic ∧ Irreducible (R.map V.subtype) := by
        intro R hR
        exact hfactors R (by simp [hR])
      let qbar : Polynomial (IsLocalRing.ResidueField V) :=
        Q.map (IsLocalRing.residue V)
      have hQbarMonic : qbar.Monic := hQdata.1.map (IsLocalRing.residue V)
      have hproduct' :
          qbar * (factors.map
            (fun R => R.map (IsLocalRing.residue V))).prod = gbar * hbar := by
        simpa [qbar] using hproduct
      have hQdvd : qbar ∣ gbar * hbar := by
        rw [← hproduct']
        exact dvd_mul_right _ _
      let E : Type u := (Q.map V.subtype).SplittingField
      obtain ⟨W, hW, hWuniq⟩ := hunique E
      let : V.valuation.HasExtension W.valuation := hW
      have hside : qbar ∣ gbar ∨ qbar ∣ hbar :=
        irreducible_monic_reduction_dvd_left_or_right_of_coprime
          V W hWuniq Q hQdata.1 hQdata.2 gbar hbar hcoprime hQdvd
      rcases hside with hQg | hQh
      · obtain ⟨g', hg'⟩ := hQg
        have hg'monic : g'.Monic := by
          apply hQbarMonic.of_mul_monic_left
          rw [← hg']
          exact hgmonic
        have hg'coprime : IsCoprime g' hbar := by
          rcases hcoprime with ⟨A, B, hbez⟩
          refine ⟨A * qbar, B, ?_⟩
          calc
            (A * qbar) * g' + B * hbar =
                A * (qbar * g') + B * hbar := by ring
            _ = A * gbar + B * hbar := by rw [← hg']
            _ = 1 := hbez
        have hrest :
            (factors.map
              (fun R => R.map (IsLocalRing.residue V))).prod =
              g' * hbar := by
          apply mul_left_cancel₀ hQbarMonic.ne_zero
          calc
            qbar * (factors.map
                (fun R => R.map (IsLocalRing.residue V))).prod =
                gbar * hbar := hproduct'
            _ = (qbar * g') * hbar := by rw [← hg']
            _ = qbar * (g' * hbar) := by ring
        obtain ⟨G, H, hGmonic, hHmonic, hfactorGH, hGbar, hHbar⟩ :=
          ih htail g' hbar hg'monic hhmonic hrest hg'coprime
        refine ⟨Q * G, H, hQdata.1.mul hGmonic, hHmonic, ?_, ?_, hHbar⟩
        · simp only [Multiset.prod_cons, hfactorGH]
          ring
        · rw [Polynomial.map_mul, hGbar]
          exact hg'.symm
      · obtain ⟨h', hh'⟩ := hQh
        have hh'monic : h'.Monic := by
          apply hQbarMonic.of_mul_monic_left
          rw [← hh']
          exact hhmonic
        have hh'coprime : IsCoprime gbar h' := by
          rcases hcoprime with ⟨A, B, hbez⟩
          refine ⟨A, B * qbar, ?_⟩
          calc
            A * gbar + (B * qbar) * h' =
                A * gbar + B * (qbar * h') := by ring
            _ = A * gbar + B * hbar := by rw [← hh']
            _ = 1 := hbez
        have hrest :
            (factors.map
              (fun R => R.map (IsLocalRing.residue V))).prod =
              gbar * h' := by
          apply mul_left_cancel₀ hQbarMonic.ne_zero
          calc
            qbar * (factors.map
                (fun R => R.map (IsLocalRing.residue V))).prod =
                gbar * hbar := hproduct'
            _ = gbar * (qbar * h') := by rw [← hh']
            _ = qbar * (gbar * h') := by ring
        obtain ⟨G, H, hGmonic, hHmonic, hfactorGH, hGbar, hHbar⟩ :=
          ih htail gbar h' hgmonic hh'monic hrest hh'coprime
        refine ⟨G, Q * H, hGmonic, hQdata.1.mul hHmonic, ?_, hGbar, ?_⟩
        · simp only [Multiset.prod_cons, hfactorGH]
          ring
        · rw [Polynomial.map_mul, hHbar]
          exact hh'.symm