PrimitiveFactorization.lean

def PrimitiveIrreducibleReductionProperty
    {K : Type*} [Field K] (V : ValuationSubring K) : Prop

theorem primitiveIrreducibleReduction_dvd_left_or_right_of_coprime
    {K : Type*} [Field K] (V : ValuationSubring K)
    (hproperty : PrimitiveIrreducibleReductionProperty V)
    (Q : Polynomial V) (hQprim : Q.IsPrimitive)
    (hQirr : Irreducible (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_primitive_irreducible_factors_along_coprime_reduction
    {K : Type*} [Field K] (V : ValuationSubring K)
    (hproperty : PrimitiveIrreducibleReductionProperty V)
    (factors : Multiset (Polynomial V))
    (hfactors : ∀ Q ∈ factors,
      Q.IsPrimitive ∧ Irreducible (Q.map V.subtype))
    (gbar hbar : Polynomial (IsLocalRing.ResidueField V))
    (hproduct :
      (factors.map (fun Q => Q.map (IsLocalRing.residue V))).prod =
        gbar * hbar)
    (hcoprime : IsCoprime gbar hbar) :
    ∃ G H : Polynomial V,
      factors.prod = G * H ∧
        G.map (IsLocalRing.residue V) = gbar ∧
          H.map (IsLocalRing.residue V) = hbar ∧
            G.natDegree = gbar.natDegree := 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⟩
      obtain ⟨c, hcunit, hcg⟩ := Polynomial.isUnit_iff.mp hgunit
      obtain ⟨a, ha⟩ := Ideal.Quotient.mk_surjective c
      have hares : IsLocalRing.residue V a = c := ha
      have haunit : IsUnit a :=
        (IsLocalRing.residue_ne_zero_iff_isUnit a).1
          (by simpa [hares] using hcunit.ne_zero)
      obtain ⟨ua, hua⟩ := haunit
      let G : Polynomial V := Polynomial.C a
      let H : Polynomial V := Polynomial.C (ua⁻¹ : Vˣ)
      have hGH : G * H = 1 := by
        change Polynomial.C a * Polynomial.C ((ua⁻¹ : Vˣ) : V) =
          Polynomial.C 1
        rw [← Polynomial.C_mul]
        congr 1
        rw [← hua]
        exact Units.mul_inv ua
      have hGmap : G.map (IsLocalRing.residue V) = gbar := by
        simpa [G, hares] using hcg
      have hHmap : H.map (IsLocalRing.residue V) = hbar := by
        apply mul_left_cancel₀ hgunit.ne_zero
        calc
          gbar * H.map (IsLocalRing.residue V) =
              G.map (IsLocalRing.residue V) *
                H.map (IsLocalRing.residue V) := by rw [hGmap]
          _ = (G * H).map (IsLocalRing.residue V) := by
            rw [Polynomial.map_mul]
          _ = 1 := by simp [hGH]
          _ = gbar * hbar := hgh.symm
      have hGunit : IsUnit G := by
        dsimp [G]
        rw [← hua]
        exact Polynomial.isUnit_C.mpr ua.isUnit
      refine ⟨G, H, ?_, hGmap, hHmap, ?_⟩
      · simpa using hGH.symm
      · rw [Polynomial.natDegree_eq_zero_of_isUnit hGunit,
          Polynomial.natDegree_eq_zero_of_isUnit hgunit]
  | cons Q factors ih =>
      have hQdata : Q.IsPrimitive ∧ Irreducible (Q.map V.subtype) :=
        hfactors Q (by simp)
      have htail : ∀ R ∈ factors,
          R.IsPrimitive ∧ 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 hQbar0 : qbar ≠ 0 :=
        polynomial_residue_ne_zero_of_isPrimitive V hQdata.1
      have hdegreeData := (hproperty Q hQdata.1 hQdata.2).1
      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 _ _
      have hside :
          (qbar.natDegree = Q.natDegree ∧ qbar ∣ gbar) ∨
            qbar ∣ hbar := by
        rcases hdegreeData with hqconst | hqfull
        · right
          have hqunit : IsUnit qbar := by
            rw [Polynomial.isUnit_iff_degree_eq_zero,
              Polynomial.degree_eq_natDegree hQbar0, hqconst]
            rfl
          exact hqunit.dvd
        · rcases
            primitiveIrreducibleReduction_dvd_left_or_right_of_coprime
              V hproperty Q hQdata.1 hQdata.2 gbar hbar hcoprime hQdvd with
            hQg | hQh
          · exact Or.inl ⟨hqfull, hQg⟩
          · exact Or.inr hQh
      rcases hside with ⟨hQdegree, hQg⟩ | hQh
      · obtain ⟨g', hg'⟩ := hQg
        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₀ hQbar0
          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, hfactorGH, hGbar, hHbar, hGdegree⟩ :=
          ih htail g' hbar hrest hg'coprime
        have hQ0 : Q ≠ 0 := hQdata.1.ne_zero
        have hg'0 : g' ≠ 0 := by
          have hrest0 :
              (factors.map
                (fun R => R.map (IsLocalRing.residue V))).prod ≠ 0 :=
            Multiset.prod_ne_zero (by
              intro hzeroMem
              rcases Multiset.mem_map.mp hzeroMem with ⟨R, hR, hRzero⟩
              exact
                (polynomial_residue_ne_zero_of_isPrimitive V (htail R hR).1)
                  hRzero)
          have hmul0 : g' * hbar ≠ 0 := by
            rw [← hrest]
            exact hrest0
          exact left_ne_zero_of_mul hmul0
        have hG0 : G ≠ 0 := by
          intro hzero
          rw [hzero] at hGbar
          exact hg'0 (by simpa using hGbar.symm)
        refine ⟨Q * G, H, ?_, ?_, hHbar, ?_⟩
        · simp only [Multiset.prod_cons, hfactorGH]
          ring
        · rw [Polynomial.map_mul, hGbar]
          exact hg'.symm
        · rw [Polynomial.natDegree_mul hQ0 hG0]
          calc
            Q.natDegree + G.natDegree =
                qbar.natDegree + g'.natDegree := by
              rw [hQdegree, hGdegree]
            _ = (qbar * g').natDegree :=
              (Polynomial.natDegree_mul hQbar0 hg'0).symm
            _ = gbar.natDegree := by rw [← hg']
      · obtain ⟨h', hh'⟩ := hQh
        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₀ hQbar0
          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, hfactorGH, hGbar, hHbar, hGdegree⟩ :=
          ih htail gbar h' hrest hh'coprime
        refine ⟨G, Q * H, ?_, hGbar, ?_, hGdegree⟩
        · simp only [Multiset.prod_cons, hfactorGH]
          ring
        · rw [Polynomial.map_mul, hHbar]
          exact hh'.symm

theorem henselFactorization_of_primitiveIrreducibleReductionProperty
    {K : Type*} [Field K] (V : ValuationSubring K)
    (hproperty : PrimitiveIrreducibleReductionProperty V) :
    HenselFactorizationProperty V