AdicLimits.lean

def henselFactorization_adicCoeffCauchy
    {R : Type*} [CommRing R] (I : Ideal R) (x : ℕ → R) : Prop

theorem henselFactorization_coeff_adicCoeffCauchy_of_sub_coeff_mem
    {R : Type*} [CommRing R] (I : Ideal R) {Pseq : ℕ → R[X]}
    (hsub :
      ∀ {M N : ℕ}, M ≤ N → ∀ i : ℕ,
        (Pseq N - Pseq M).coeff i ∈ I ^ (M + 1))
    (i : ℕ) :
    henselFactorization_adicCoeffCauchy I (fun N : ℕ => (Pseq N).coeff i) := by
  intro M N hMN
  simpa [henselFactorization_adicCoeffCauchy, Polynomial.coeff_sub] using hsub hMN i

theorem henselFactorization_adicCoeffCauchy_isAdicCauchy
    {R : Type*} [CommRing R] (I : Ideal R) {x : ℕ → R}
    (hx : henselFactorization_adicCoeffCauchy I x) :
    AdicCompletion.IsAdicCauchy I R x

theorem henselFactorization_exists_adicCoeffLimit
    {R : Type*} [CommRing R] (I : Ideal R) [IsPrecomplete I R]
    {x : ℕ → R}
    (hx : henselFactorization_adicCoeffCauchy I x) :
    ∃ L : R, ∀ n : ℕ, x n - L ∈ I ^ n

def henselFactorization_polyOfLimitCoeffs
    {R : Type*} [Semiring R] (N : ℕ) (c : ℕ → R) : R[X]

theorem henselFactorization_polyOfLimitCoeffs_coeff_of_le
    {R : Type*} [Semiring R] {N n : ℕ} (c : ℕ → R) (hn : n ≤ N) :
    (henselFactorization_polyOfLimitCoeffs N c).coeff n = c n

theorem henselFactorization_polyOfLimitCoeffs_coeff_eq_zero_of_lt
    {R : Type*} [Semiring R] {N n : ℕ} (c : ℕ → R) (hn : N < n) :
    (henselFactorization_polyOfLimitCoeffs N c).coeff n = 0

theorem henselFactorization_polyOfLimitCoeffs_natDegree_le
    {R : Type*} [Semiring R] (N : ℕ) (c : ℕ → R) :
    (henselFactorization_polyOfLimitCoeffs N c).natDegree ≤ N

theorem henselFactorization_exists_limitPolynomial_of_bounded_coeffLimits
    {R : Type*} [CommRing R] (I : Ideal R) [IsPrecomplete I R]
    {N : ℕ} {Pseq : ℕ → R[X]}
    (hdeg : ∀ n : ℕ, (Pseq n).natDegree ≤ N)
    (hcauchy :
      ∀ i : ℕ, henselFactorization_adicCoeffCauchy I
        (fun n : ℕ => (Pseq n).coeff i)) :
    ∃ P : R[X], P.natDegree ≤ N ∧
      ∀ n i : ℕ, (Pseq n - P).coeff i ∈ I ^ n := by
  classical
  let L : ℕ → R :=
    fun i =>
      Classical.choose
        (henselFactorization_exists_adicCoeffLimit (I := I) (hcauchy i))
  let P : R[X] := henselFactorization_polyOfLimitCoeffs N L
  refine ⟨P, henselFactorization_polyOfLimitCoeffs_natDegree_le N L, ?_⟩
  intro n i
  by_cases hi : i ≤ N
  · have hlim :=
      Classical.choose_spec
        (henselFactorization_exists_adicCoeffLimit (I := I) (hcauchy i)) n
    simpa [P, L, Polynomial.coeff_sub,
      henselFactorization_polyOfLimitCoeffs_coeff_of_le (c := L) hi] using hlim
  · have hlt : N < i := Nat.lt_of_not_ge hi
    have hseq : (Pseq n).coeff i = 0 :=
      Polynomial.coeff_eq_zero_of_natDegree_lt
        (lt_of_le_of_lt (hdeg n) hlt)
    have hP : P.coeff i = 0 :=
      henselFactorization_polyOfLimitCoeffs_coeff_eq_zero_of_lt (c := L) hlt
    simp [Polynomial.coeff_sub, hseq, hP]

theorem henselFactorization_mul_left_coeff_mem_ideal
    {R : Type*} [CommRing R] (I : Ideal R) {A B : R[X]}
    (hA : ∀ i : ℕ, A.coeff i ∈ I) :
    ∀ i : ℕ, (A * B).coeff i ∈ I

theorem henselFactorization_mul_right_coeff_mem_ideal
    {R : Type*} [CommRing R] (I : Ideal R) {A B : R[X]}
    (hB : ∀ i : ℕ, B.coeff i ∈ I) :
    ∀ i : ℕ, (A * B).coeff i ∈ I

theorem henselFactorization_mul_sub_mul_coeff_mem_of_coeff_mem
    {R : Type*} [CommRing R] (I : Ideal R) {A A' B B' : R[X]}
    (hA : ∀ i : ℕ, (A - A').coeff i ∈ I)
    (hB : ∀ i : ℕ, (B - B').coeff i ∈ I) :
    ∀ i : ℕ, (A * B - A' * B').coeff i ∈ I

theorem henselFactorization_limit_factor_coeff_mem_of_approximants
    {R : Type*} [CommRing R] (I : Ideal R)
    {f G H Gn Hn : R[X]}
    (herr : ∀ i : ℕ, (f - Gn * Hn).coeff i ∈ I)
    (hG : ∀ i : ℕ, (Gn - G).coeff i ∈ I)
    (hH : ∀ i : ℕ, (Hn - H).coeff i ∈ I) :
    ∀ i : ℕ, (f - G * H).coeff i ∈ I

theorem henselFactorization_polynomial_eq_zero_of_coeff_mem_all_powers
    {R : Type*} [CommRing R] (I : Ideal R) [IsHausdorff I R]
    {P : R[X]}
    (hP : ∀ n i : ℕ, P.coeff i ∈ I ^ n) :
    P = 0

theorem henselFactorization_limit_factor_eq_of_approximants
    {R : Type*} [CommRing R] (I : Ideal R) [IsHausdorff I R]
    {f G H : R[X]} {Gseq Hseq : ℕ → R[X]}
    (herr : ∀ n i : ℕ, (f - Gseq n * Hseq n).coeff i ∈ I ^ n)
    (hG : ∀ n i : ℕ, (Gseq n - G).coeff i ∈ I ^ n)
    (hH : ∀ n i : ℕ, (Hseq n - H).coeff i ∈ I ^ n) :
    f = G * H

theorem henselFactorization_limit_reduction_of_approx_reduction
    {R : Type*} [CommRing R] (I : Ideal R)
    {P P0 : R[X]} {Pseq : ℕ → R[X]}
    (hlim : ∀ n i : ℕ, (Pseq n - P).coeff i ∈ I ^ n)
    (hred : ∀ n i : ℕ, (Pseq n - P0).coeff i ∈ I) :
    ∀ i : ℕ, (P - P0).coeff i ∈ I

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

theorem henselFactorization_residue_map_eq_of_sub_coeff_mem_maximalIdeal
    {R : Type*} [CommRing R] [IsLocalRing R] {P Q : R[X]}
    (hcoeff : ∀ i : ℕ, (P - Q).coeff i ∈ IsLocalRing.maximalIdeal R) :
    P.map (IsLocalRing.residue R) = Q.map (IsLocalRing.residue R)