Basic.lean

theorem henselFactorization_map_mul_add_mul
    {R k : Type*} [CommSemiring R] [CommSemiring k] (φ : R →+* k)
    (a b g h : R[X]) :
    (a * g + b * h).map φ = a.map φ * g.map φ + b.map φ * h.map φ

theorem henselFactorization_map_sub_mul
    {R k : Type*} [CommRing R] [CommRing k] (φ : R →+* k)
    (f g h : R[X]) :
    (f - g * h).map φ = f.map φ - g.map φ * h.map φ

theorem henselFactorization_map_mul_sub_self
    {R k : Type*} [CommRing R] [CommRing k] (φ : R →+* k)
    (P F : R[X]) :
    (P * F - F).map φ = P.map φ * F.map φ - F.map φ

theorem henselFactorization_map_mul_sub
    {R k : Type*} [CommRing R] [CommRing k] (φ : R →+* k)
    (g q A : R[X]) :
    (g * q - A).map φ = g.map φ * q.map φ - A.map φ

theorem henselFactorization_map_mul_add_mul_sub
    {R k : Type*} [CommRing R] [CommRing k] (φ : R →+* k)
    (g h q p fn : R[X]) :
    (g * q + h * p - fn).map φ =
      g.map φ * q.map φ + h.map φ * p.map φ - fn.map φ

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

theorem henselFactorization_maximalIdeal_le_span_of_eq
    {R : Type*} [CommRing R] [IsLocalRing R] {π : R}
    (hπ : IsLocalRing.maximalIdeal R = Ideal.span ({π} : Set R)) :
    IsLocalRing.maximalIdeal R ≤ Ideal.span ({π} : Set R)

theorem henselFactorization_principal_maximal_mem_le_of_eq
    {R : Type*} [CommRing R] [IsLocalRing R] {π : R}
    (hπ : IsLocalRing.maximalIdeal R = Ideal.span ({π} : Set R)) :
    π ∈ IsLocalRing.maximalIdeal R ∧
      IsLocalRing.maximalIdeal R ≤ Ideal.span ({π} : Set R)

theorem henselFactorization_exists_polynomial_lift_degree_eq
    {R k : Type*} [CommRing R] [CommRing k] (φ : R →+* k)
    (hφ : Function.Surjective φ) (fbar : k[X]) :
    ∃ f : R[X], f.map φ = fbar ∧ f.degree = fbar.degree

theorem henselFactorization_exists_polynomial_lift_natDegree_eq
    {R k : Type*} [CommRing R] [CommRing k] (φ : R →+* k)
    (hφ : Function.Surjective φ) (fbar : k[X]) :
    ∃ f : R[X], f.map φ = fbar ∧ f.natDegree = fbar.natDegree

theorem henselFactorization_lift_leadingCoeff_isUnit_of_natDegree_eq
    {R : Type*} [CommRing R] [IsLocalRing R]
    {g0 : R[X]} {gbar : (IsLocalRing.ResidueField R)[X]}
    (hg0 : g0.map (IsLocalRing.residue R) = gbar)
    (hdegree : g0.natDegree = gbar.natDegree)
    (hlead : gbar.leadingCoeff ≠ 0) :
    IsUnit g0.leadingCoeff

theorem henselFactorization_monic_normalization_of_unit_leadingCoeff
    {R : Type*} [CommRing R] {g : R[X]} (hunit : IsUnit g.leadingCoeff) :
    ∃ u : Rˣ,
      (u : R) = g.leadingCoeff ∧
        (Polynomial.C ((u⁻¹ : Rˣ) : R) * g).Monic ∧
          (Polynomial.C ((u⁻¹ : Rˣ) : R) * g).degree = g.degree ∧
            (Polynomial.C ((u⁻¹ : Rˣ) : R) * g).natDegree = g.natDegree

theorem henselFactorization_exists_bezout_lifts
    {R k : Type*} [CommRing R] [CommRing k] (φ : R →+* k)
    (hφ : Function.Surjective φ)
    {gbar hbar : k[X]} (hcop : IsCoprime gbar hbar)
    {g0 h0 : R[X]} (hg0 : g0.map φ = gbar) (hh0 : h0.map φ = hbar) :
    ∃ a b : R[X], (a * g0 + b * h0).map φ = 1

theorem henselFactorization_map_eq_zero_iff_coeff_mem_ker
    {R k : Type*} [CommRing R] [CommRing k] (φ : R →+* k) (P : R[X]) :
    P.map φ = 0 ↔ ∀ n : ℕ, P.coeff n ∈ RingHom.ker φ

theorem henselFactorization_map_eq_iff_sub_coeff_mem_ker
    {R k : Type*} [CommRing R] [CommRing k] (φ : R →+* k) (P Q : R[X]) :
    P.map φ = Q.map φ ↔ ∀ n : ℕ, (P - Q).coeff n ∈ RingHom.ker φ

theorem henselFactorization_mem_ker_quotient_mk_iff
    {R : Type*} [CommRing R] (I : Ideal R) (x : R) :
    x ∈ RingHom.ker (Ideal.Quotient.mk I) ↔ x ∈ I

theorem henselFactorization_map_quotient_eq_zero_iff_coeff_mem
    {R : Type*} [CommRing R] (I : Ideal R) (P : R[X]) :
    P.map (Ideal.Quotient.mk I) = 0 ↔ ∀ n : ℕ, P.coeff n ∈ I

theorem henselFactorization_quotient_map_coeff_eq_zero_iff_coeff_mem
    {R : Type*} [CommRing R] (I : Ideal R) (P : R[X]) (n : ℕ) :
    (P.map (Ideal.Quotient.mk I)).coeff n = 0 ↔ P.coeff n ∈ I

theorem henselFactorization_map_quotient_eq_iff_sub_coeff_mem
    {R : Type*} [CommRing R] (I : Ideal R) (P Q : R[X]) :
    P.map (Ideal.Quotient.mk I) = Q.map (Ideal.Quotient.mk I) ↔
      ∀ n : ℕ, (P - Q).coeff n ∈ I

theorem henselFactorization_coeff_mem_ker_sub_mul_of_lifts
    {R k : Type*} [CommRing R] [CommRing k] (φ : R →+* k)
    {f g0 h0 : R[X]} {gbar hbar : k[X]}
    (hfbar : f.map φ = gbar * hbar)
    (hg0 : g0.map φ = gbar) (hh0 : h0.map φ = hbar) :
    ∀ n : ℕ, (f - g0 * h0).coeff n ∈ RingHom.ker φ

theorem henselFactorization_coeff_mem_maximalIdeal_sub_mul_of_residue_lifts
    {R : Type*} [CommRing R] [IsLocalRing R]
    {f g0 h0 : R[X]} {gbar hbar : (IsLocalRing.ResidueField R)[X]}
    (hfbar : f.map (IsLocalRing.residue R) = gbar * hbar)
    (hg0 : g0.map (IsLocalRing.residue R) = gbar)
    (hh0 : h0.map (IsLocalRing.residue R) = hbar) :
    ∀ n : ℕ, (f - g0 * h0).coeff n ∈ IsLocalRing.maximalIdeal R

theorem henselFactorization_coeff_mem_ker_sub_one_of_map_eq_one
    {R k : Type*} [CommRing R] [CommRing k] (φ : R →+* k)
    {P : R[X]} (hP : P.map φ = 1) :
    ∀ n : ℕ, (P - 1).coeff n ∈ RingHom.ker φ

theorem henselFactorization_coeff_mem_maximalIdeal_sub_one_of_bezout_lift
    {R : Type*} [CommRing R] [IsLocalRing R]
    {a b g0 h0 : R[X]}
    (hbez : (a * g0 + b * h0).map (IsLocalRing.residue R) = 1) :
    ∀ n : ℕ, (a * g0 + b * h0 - 1).coeff n ∈
      IsLocalRing.maximalIdeal R

theorem henselFactorization_division_by_monic_degree_lt
    {R : Type*} [CommRing R] [Nontrivial R] (F g : R[X]) (hg : g.Monic) :
    ∃ q p : R[X], F = g * q + p ∧ p.degree < g.degree

theorem henselFactorization_division_by_unit_leading_degree_lt
    {R : Type*} [CommRing R] [Nontrivial R] (F g : R[X])
    (hunit : IsUnit g.leadingCoeff) :
    ∃ q p : R[X], F = g * q + p ∧ p.degree < g.degree

theorem henselFactorization_division_by_lifted_factor_degree_lt
    {R : Type*} [CommRing R] [IsLocalRing R]
    {g0 : R[X]} {gbar : (IsLocalRing.ResidueField R)[X]}
    (hg0 : g0.map (IsLocalRing.residue R) = gbar)
    (hdegree : g0.natDegree = gbar.natDegree)
    (hlead : gbar.leadingCoeff ≠ 0) (F : R[X]) :
    ∃ q p : R[X], F = g0 * q + p ∧ p.degree < g0.degree

theorem henselFactorization_correction_identity_after_division
    {R : Type*} [CommSemiring R] {a b g0 h0 fn q p : R[X]}
    (hdiv : b * fn = g0 * q + p) :
    g0 * (a * fn + h0 * q) + h0 * p = (a * g0 + b * h0) * fn

theorem henselFactorization_correction_congruence_after_division
    {R k : Type*} [CommRing R] [CommRing k] (φ : R →+* k)
    {a b g0 h0 fn q p : R[X]}
    (hbez : (a * g0 + b * h0).map φ = 1)
    (hdiv : b * fn = g0 * q + p) :
    ∀ n : ℕ,
      (g0 * (a * fn + h0 * q) + h0 * p - fn).coeff n ∈ RingHom.ker φ

theorem henselFactorization_correction_congruence_span_singleton_after_division
    {R : Type*} [CommRing R] {π : R}
    {a b g0 h0 fn q p e : R[X]}
    (hbez : a * g0 + b * h0 - 1 = Polynomial.C π * e)
    (hdiv : b * fn = g0 * q + p) :
    ∀ n : ℕ,
      (g0 * (a * fn + h0 * q) + h0 * p - fn).coeff n ∈
        Ideal.span ({π} : Set R)

theorem henselFactorization_correction_mem_maximalIdeal_after_division
    {R : Type*} [CommRing R] [IsLocalRing R]
    {a b g0 h0 fn q p : R[X]}
    (hbez : (a * g0 + b * h0).map (IsLocalRing.residue R) = 1)
    (hdiv : b * fn = g0 * q + p) :
    ∀ n : ℕ,
      (g0 * (a * fn + h0 * q) + h0 * p - fn).coeff n ∈
        IsLocalRing.maximalIdeal R