Truncation.lean

def henselFactorization_lowPart {R : Type*} [Semiring R] (N : ℕ) (P : R[X]) : R[X]

theorem henselFactorization_lowPart_coeff_of_le
    {R : Type*} [Semiring R] {N n : ℕ} (P : R[X]) (hn : n ≤ N) :
    (henselFactorization_lowPart N P).coeff n = P.coeff n

theorem henselFactorization_lowPart_coeff_eq_zero_of_lt
    {R : Type*} [Semiring R] {N n : ℕ} (P : R[X]) (hn : N < n) :
    (henselFactorization_lowPart N P).coeff n = 0

theorem henselFactorization_lowPart_natDegree_le
    {R : Type*} [Semiring R] (N : ℕ) (P : R[X]) :
    (henselFactorization_lowPart N P).natDegree ≤ N

theorem henselFactorization_lowPart_map_eq_of_high_coeff_mem_ker
    {R k : Type*} [CommRing R] [CommRing k] (φ : R →+* k)
    (N : ℕ) (P : R[X])
    (hhigh : ∀ n : ℕ, N < n → P.coeff n ∈ RingHom.ker φ) :
    (henselFactorization_lowPart N P).map φ = P.map φ

theorem henselFactorization_lowPart_residue_map_eq_of_high_coeff_mem_maximalIdeal
    {R : Type*} [CommRing R] [IsLocalRing R] (N : ℕ) (P : R[X])
    (hhigh : ∀ n : ℕ, N < n → P.coeff n ∈ IsLocalRing.maximalIdeal R) :
    (henselFactorization_lowPart N P).map (IsLocalRing.residue R) =
      P.map (IsLocalRing.residue R)

theorem henselFactorization_correction_after_lowPart_ker
    {R k : Type*} [CommRing R] [CommRing k] (φ : R →+* k)
    {g0 h0 fn p Q : R[X]} (N : ℕ)
    (hcorr :
      ∀ n : ℕ, (g0 * Q + h0 * p - fn).coeff n ∈ RingHom.ker φ)
    (hhigh : ∀ n : ℕ, N < n → Q.coeff n ∈ RingHom.ker φ) :
    (henselFactorization_lowPart N Q).natDegree ≤ N ∧
      ∀ n : ℕ,
        (g0 * henselFactorization_lowPart N Q + h0 * p - fn).coeff n ∈
          RingHom.ker φ

theorem henselFactorization_correction_after_lowPart_ideal
    {R : Type*} [CommRing R] {I : Ideal R}
    {g0 h0 fn p Q : R[X]} (N : ℕ)
    (hcorr :
      ∀ n : ℕ, (g0 * Q + h0 * p - fn).coeff n ∈ I)
    (hhigh : ∀ n : ℕ, N < n → Q.coeff n ∈ I) :
    (henselFactorization_lowPart N Q).natDegree ≤ N ∧
      ∀ n : ℕ,
        (g0 * henselFactorization_lowPart N Q + h0 * p - fn).coeff n ∈ I

theorem henselFactorization_correction_after_lowPart_span_singleton
    {R : Type*} [CommRing R] {π : R}
    {g0 h0 fn p Q : R[X]} (N : ℕ)
    (hcorr :
      ∀ n : ℕ, (g0 * Q + h0 * p - fn).coeff n ∈
        Ideal.span ({π} : Set R))
    (hhigh : ∀ n : ℕ, N < n → Q.coeff n ∈
      Ideal.span ({π} : Set R)) :
    (henselFactorization_lowPart N Q).natDegree ≤ N ∧
      ∀ n : ℕ,
        (g0 * henselFactorization_lowPart N Q + h0 * p - fn).coeff n ∈
          Ideal.span ({π} : Set R)

theorem henselFactorization_natDegree_right_le_tsub_of_mul_natDegree_le
    {k : Type*} [Field k] {g Q : k[X]} {m d : ℕ}
    (hgdeg : g.natDegree = m) (hg : g ≠ 0)
    (hprod : (g * Q).natDegree ≤ d) :
    Q.natDegree ≤ d - m

theorem henselFactorization_natDegree_right_le_tsub_of_unit_leading_mul_natDegree_le
    {R : Type*} [CommRing R] {g Q : R[X]} {m d : ℕ}
    (hgunit : IsUnit g.leadingCoeff) (hgdeg : g.natDegree = m)
    (hprod : (g * Q).natDegree ≤ d) :
    Q.natDegree ≤ d - m

theorem henselFactorization_map_unit_leadingCoeff_natDegree_eq
    {R S : Type*} [CommRing R] [CommRing S] [Nontrivial S]
    (φ : R →+* S) {g : R[X]} {m : ℕ}
    (hgunit : IsUnit g.leadingCoeff) (hgdeg : g.natDegree = m) :
    IsUnit (g.map φ).leadingCoeff ∧ (g.map φ).natDegree = m

theorem henselFactorization_quotient_unit_leadingCoeff_natDegree_eq
    {R : Type*} [CommRing R] {I : Ideal R} [Nontrivial (R ⧸ I)]
    {g : R[X]} {m : ℕ}
    (hgunit : IsUnit g.leadingCoeff) (hgdeg : g.natDegree = m) :
    IsUnit (g.map (Ideal.Quotient.mk I)).leadingCoeff ∧
      (g.map (Ideal.Quotient.mk I)).natDegree = m

theorem henselFactorization_span_singleton_quotient_nontrivial_of_mem_maximalIdeal
    {R : Type*} [CommRing R] [IsLocalRing R] {π : R}
    (hπ : π ∈ IsLocalRing.maximalIdeal R) :
    Nontrivial (R ⧸ Ideal.span ({π} : Set R))

theorem henselFactorization_span_singleton_quotient_unit_leadingCoeff_natDegree_eq
    {R : Type*} [CommRing R] [IsLocalRing R] {π : R}
    {g : R[X]} {m : ℕ}
    (hπ : π ∈ IsLocalRing.maximalIdeal R)
    (hgunit : IsUnit g.leadingCoeff) (hgdeg : g.natDegree = m) :
    IsUnit
        ((g.map (Ideal.Quotient.mk (Ideal.span ({π} : Set R)))).leadingCoeff) ∧
      (g.map (Ideal.Quotient.mk (Ideal.span ({π} : Set R)))).natDegree = m

theorem henselFactorization_residue_sub_mul_natDegree_le
    {R : Type*} [CommRing R] [IsLocalRing R]
    {fn h0 P : R[X]} {a b d : ℕ}
    (hfn : (fn.map (IsLocalRing.residue R)).natDegree ≤ d)
    (hh0 : (h0.map (IsLocalRing.residue R)).natDegree ≤ a)
    (hP : (P.map (IsLocalRing.residue R)).natDegree ≤ b)
    (hab : a + b ≤ d) :
    ((fn - h0 * P).map (IsLocalRing.residue R)).natDegree ≤ d

theorem henselFactorization_map_sub_mul_natDegree_le_of_degree_bounds
    {R S : Type*} [CommRing R] [CommRing S] (φ : R →+* S)
    {fn h0 P : R[X]} {a b d : ℕ}
    (hfn : fn.natDegree ≤ d)
    (hh0 : h0.natDegree ≤ a)
    (hP : P.natDegree ≤ b)
    (hab : a + b ≤ d) :
    ((fn - h0 * P).map φ).natDegree ≤ d

theorem henselFactorization_span_singleton_quotient_sub_mul_natDegree_le_of_degree_bounds
    {R : Type*} [CommRing R] {π : R}
    {fn h0 P : R[X]} {a b d : ℕ}
    (hfn : fn.natDegree ≤ d)
    (hh0 : h0.natDegree ≤ a)
    (hP : P.natDegree ≤ b)
    (hab : a + b ≤ d) :
    ((fn - h0 * P).map
      (Ideal.Quotient.mk (Ideal.span ({π} : Set R)))).natDegree ≤ d

theorem henselFactorization_product_congruence_of_correction
    {R : Type*} [CommRing R] [IsLocalRing R]
    {g0 h0 fn p Q : R[X]}
    (hcorr :
      ∀ n : ℕ, (g0 * Q + h0 * p - fn).coeff n ∈ IsLocalRing.maximalIdeal R) :
    ∀ n : ℕ, (g0 * Q - (fn - h0 * p)).coeff n ∈
      IsLocalRing.maximalIdeal R

theorem henselFactorization_high_coeff_mem_maximalIdeal_of_product_congruence_degree
    {R : Type*} [CommRing R] [IsLocalRing R]
    {g0 Q A : R[X]} {m d : ℕ}
    (hgdeg : (g0.map (IsLocalRing.residue R)).natDegree = m)
    (hg : g0.map (IsLocalRing.residue R) ≠ 0)
    (hcong : ∀ n : ℕ, (g0 * Q - A).coeff n ∈ IsLocalRing.maximalIdeal R)
    (hAdeg : (A.map (IsLocalRing.residue R)).natDegree ≤ d) :
    ∀ n : ℕ, d - m < n → Q.coeff n ∈ IsLocalRing.maximalIdeal R

theorem henselFactorization_high_coeff_mem_span_singleton_of_product_congruence_degree
    {R : Type*} [CommRing R] {π : R}
    {g0 Q A : R[X]} {m d : ℕ}
    (hgunit :
      IsUnit
        ((g0.map (Ideal.Quotient.mk (Ideal.span ({π} : Set R)))).leadingCoeff))
    (hgdeg :
      (g0.map (Ideal.Quotient.mk (Ideal.span ({π} : Set R)))).natDegree = m)
    (hcong : ∀ n : ℕ, (g0 * Q - A).coeff n ∈
      Ideal.span ({π} : Set R))
    (hAdeg :
      (A.map (Ideal.Quotient.mk (Ideal.span ({π} : Set R)))).natDegree ≤ d) :
    ∀ n : ℕ, d - m < n → Q.coeff n ∈ Ideal.span ({π} : Set R)

theorem henselFactorization_high_coeff_mem_maximalIdeal_of_correction_degree
    {R : Type*} [CommRing R] [IsLocalRing R]
    {g0 h0 fn p Q : R[X]} {m d : ℕ}
    (hgdeg : (g0.map (IsLocalRing.residue R)).natDegree = m)
    (hg : g0.map (IsLocalRing.residue R) ≠ 0)
    (hcorr :
      ∀ n : ℕ, (g0 * Q + h0 * p - fn).coeff n ∈
        IsLocalRing.maximalIdeal R)
    (hAdeg : ((fn - h0 * p).map (IsLocalRing.residue R)).natDegree ≤ d) :
    ∀ n : ℕ, d - m < n → Q.coeff n ∈ IsLocalRing.maximalIdeal R

theorem henselFactorization_high_coeff_mem_span_singleton_of_correction_degree
    {R : Type*} [CommRing R] {π : R}
    {g0 h0 fn p Q : R[X]} {m d : ℕ}
    (hgunit :
      IsUnit
        ((g0.map (Ideal.Quotient.mk (Ideal.span ({π} : Set R)))).leadingCoeff))
    (hgdeg :
      (g0.map (Ideal.Quotient.mk (Ideal.span ({π} : Set R)))).natDegree = m)
    (hcorr :
      ∀ n : ℕ, (g0 * Q + h0 * p - fn).coeff n ∈
        Ideal.span ({π} : Set R))
    (hAdeg :
      ((fn - h0 * p).map
        (Ideal.Quotient.mk (Ideal.span ({π} : Set R)))).natDegree ≤ d) :
    ∀ n : ℕ, d - m < n → Q.coeff n ∈ Ideal.span ({π} : Set R)

theorem henselFactorization_correction_after_degree_truncation_span_singleton
    {R : Type*} [CommRing R] {π : R}
    {g0 h0 fn p Q : R[X]} {m d : ℕ}
    (hgunit :
      IsUnit
        ((g0.map (Ideal.Quotient.mk (Ideal.span ({π} : Set R)))).leadingCoeff))
    (hgdeg :
      (g0.map (Ideal.Quotient.mk (Ideal.span ({π} : Set R)))).natDegree = m)
    (hcorr :
      ∀ n : ℕ, (g0 * Q + h0 * p - fn).coeff n ∈
        Ideal.span ({π} : Set R))
    (hAdeg :
      ((fn - h0 * p).map
        (Ideal.Quotient.mk (Ideal.span ({π} : Set R)))).natDegree ≤ d) :
    (henselFactorization_lowPart (d - m) Q).natDegree ≤ d - m ∧
      ∀ n : ℕ,
        (g0 * henselFactorization_lowPart (d - m) Q + h0 * p - fn).coeff n ∈
          Ideal.span ({π} : Set R)

theorem henselFactorization_correction_after_division_degree_truncation_span_singleton
    {R : Type*} [CommRing R] [IsLocalRing R] {π : R}
    {a b g0 h0 fn q p e : R[X]} {m d : ℕ}
    (hπ : π ∈ IsLocalRing.maximalIdeal R)
    (hgunit : IsUnit g0.leadingCoeff)
    (hg0nat : g0.natDegree = m)
    (hbezFactor : a * g0 + b * h0 - 1 = Polynomial.C π * e)
    (hdiv : b * fn = g0 * q + p)
    (hfn : fn.natDegree ≤ d)
    (hh0 : h0.natDegree ≤ d - m)
    (hp : p.natDegree ≤ m)
    (hmd : m ≤ d) :
    (henselFactorization_lowPart (d - m) (a * fn + h0 * q)).natDegree ≤ d - m ∧
      ∀ n : ℕ,
        (g0 * henselFactorization_lowPart (d - m) (a * fn + h0 * q) +
            h0 * p - fn).coeff n ∈ Ideal.span ({π} : Set R)

theorem henselFactorization_correction_after_lowPart
    {R : Type*} [CommRing R] [IsLocalRing R]
    {g0 h0 fn p Q : R[X]} (N : ℕ)
    (hcorr :
      ∀ n : ℕ, (g0 * Q + h0 * p - fn).coeff n ∈ IsLocalRing.maximalIdeal R)
    (hhigh : ∀ n : ℕ, N < n → Q.coeff n ∈ IsLocalRing.maximalIdeal R) :
    (henselFactorization_lowPart N Q).natDegree ≤ N ∧
      ∀ n : ℕ,
        (g0 * henselFactorization_lowPart N Q + h0 * p - fn).coeff n ∈
          IsLocalRing.maximalIdeal R

theorem henselFactorization_correction_after_degree_truncation
    {R : Type*} [CommRing R] [IsLocalRing R]
    {g0 h0 fn p Q : R[X]} {m d : ℕ}
    (hgdeg : (g0.map (IsLocalRing.residue R)).natDegree = m)
    (hg : g0.map (IsLocalRing.residue R) ≠ 0)
    (hcorr :
      ∀ n : ℕ, (g0 * Q + h0 * p - fn).coeff n ∈
        IsLocalRing.maximalIdeal R)
    (hAdeg : ((fn - h0 * p).map (IsLocalRing.residue R)).natDegree ≤ d) :
    (henselFactorization_lowPart (d - m) Q).natDegree ≤ d - m ∧
      ∀ n : ℕ,
        (g0 * henselFactorization_lowPart (d - m) Q + h0 * p - fn).coeff n ∈
          IsLocalRing.maximalIdeal R

theorem henselFactorization_correction_after_division_degree_truncation
    {R : Type*} [CommRing R] [IsLocalRing R]
    {a b g0 h0 fn q p : R[X]} {m d : ℕ}
    (hgdeg : (g0.map (IsLocalRing.residue R)).natDegree = m)
    (hg : g0.map (IsLocalRing.residue R) ≠ 0)
    (hbez : (a * g0 + b * h0).map (IsLocalRing.residue R) = 1)
    (hdiv : b * fn = g0 * q + p)
    (hfn : (fn.map (IsLocalRing.residue R)).natDegree ≤ d)
    (hh0 : (h0.map (IsLocalRing.residue R)).natDegree ≤ d - m)
    (hp : (p.map (IsLocalRing.residue R)).natDegree ≤ m)
    (hmd : m ≤ d) :
    (henselFactorization_lowPart (d - m) (a * fn + h0 * q)).natDegree ≤ d - m ∧
      ∀ n : ℕ,
        (g0 * henselFactorization_lowPart (d - m) (a * fn + h0 * q) +
            h0 * p - fn).coeff n ∈ IsLocalRing.maximalIdeal R

theorem henselFactorization_correction_congruence_replace_initial_factors
    {R : Type*} [CommRing R] [IsLocalRing R]
    {g0 h0 g h fn p q : R[X]}
    (hg : ∀ n : ℕ, (g - g0).coeff n ∈ IsLocalRing.maximalIdeal R)
    (hh : ∀ n : ℕ, (h - h0).coeff n ∈ IsLocalRing.maximalIdeal R)
    (hcorr :
      ∀ n : ℕ, (g0 * q + h0 * p - fn).coeff n ∈
        IsLocalRing.maximalIdeal R) :
    ∀ n : ℕ, (g * q + h * p - fn).coeff n ∈
      IsLocalRing.maximalIdeal R

theorem henselFactorization_correction_congruence_replace_initial_factors_span_singleton
    {R : Type*} [CommRing R] {π : R}
    {g0 h0 g h fn p q : R[X]}
    (hg : ∀ n : ℕ, (g - g0).coeff n ∈ Ideal.span ({π} : Set R))
    (hh : ∀ n : ℕ, (h - h0).coeff n ∈ Ideal.span ({π} : Set R))
    (hcorr :
      ∀ n : ℕ, (g0 * q + h0 * p - fn).coeff n ∈
        Ideal.span ({π} : Set R)) :
    ∀ n : ℕ, (g * q + h * p - fn).coeff n ∈
      Ideal.span ({π} : Set R)