theorem SomeLocalRings.exists_R_pow_X_add {𝕜 : Type u_1} [Field 𝕜] (Q : Polynomial 𝕜) (n : ℕ) : ∃ (R : Polynomial 𝕜), (Polynomial.X + Q) ^ n = Polynomial.X ^ n + ↑n * Polynomial.X ^ (n - 1) * Q + R * Q ^ 2

Expand (X + Q)^n to first order in Q, with a remainder divisible by Q^2.

theorem SomeLocalRings.exists_R_monomial_comp_X_add {𝕜 : Type u_1} [Field 𝕜] (Q : Polynomial 𝕜) (a : 𝕜) (n : ℕ) : ∃ (R : Polynomial 𝕜), ((Polynomial.monomial n) a).comp (Polynomial.X + Q) = (Polynomial.monomial n) a + Polynomial.derivative ((Polynomial.monomial n) a) * Q + R * Q ^ 2

Expand a monomial composed with X + Q to first order in Q.

theorem SomeLocalRings.comp_X_add_taylor1_add {𝕜 : Type u_1} [Field 𝕜] {Q P₁ P₂ : Polynomial 𝕜} (h₁ : ∃ (R : Polynomial 𝕜), P₁.comp (Polynomial.X + Q) = P₁ + Polynomial.derivative P₁ * Q + R * Q ^ 2) (h₂ : ∃ (R : Polynomial 𝕜), P₂.comp (Polynomial.X + Q) = P₂ + Polynomial.derivative P₂ * Q + R * Q ^ 2) : ∃ (R : Polynomial 𝕜), (P₁ + P₂).comp (Polynomial.X + Q) = P₁ + P₂ + Polynomial.derivative (P₁ + P₂) * Q + R * Q ^ 2

The first-order expansion property is preserved under addition (for fixed Q).

theorem SomeLocalRings.polynomial_comp_X_add_eq_add_derivative_mul_add_mul_sq {𝕜 : Type u_1} [Field 𝕜] (P Q : Polynomial 𝕜) : ∃ (R : Polynomial 𝕜), P.comp (Polynomial.X + Q) = P + Polynomial.derivative P * Q + R * Q ^ 2

Lemma 1.1. Let 𝕜 be a field and P be an irreducible polynomial over 𝕜. For Q ∈ 𝕜[X], we have P(X + Q(X)) = P(X) + P'(X) Q(X) + R(X) Q(X)^2 for some R ∈ 𝕜[X].

theorem SomeLocalRings.exists_R_pow_add {𝕜 : Type u_1} [Field 𝕜] (U Q : Polynomial 𝕜) (n : ℕ) : ∃ (R : Polynomial 𝕜), (U + Q) ^ n = U ^ n + ↑n * U ^ (n - 1) * Q + R * Q ^ 2

Expand (U + Q)^n to first order in Q, with a remainder divisible by Q^2.

theorem SomeLocalRings.exists_R_monomial_comp_add {𝕜 : Type u_1} [Field 𝕜] (U Q : Polynomial 𝕜) (a : 𝕜) (n : ℕ) : ∃ (R : Polynomial 𝕜), ((Polynomial.monomial n) a).comp (U + Q) = ((Polynomial.monomial n) a).comp U + (Polynomial.derivative ((Polynomial.monomial n) a)).comp U * Q + R * Q ^ 2

Expand a monomial composed with U + Q to first order in Q.

theorem SomeLocalRings.comp_add_taylor1_add {𝕜 : Type u_1} [Field 𝕜] {U Q P₁ P₂ : Polynomial 𝕜} (h₁ : ∃ (R : Polynomial 𝕜), P₁.comp (U + Q) = P₁.comp U + (Polynomial.derivative P₁).comp U * Q + R * Q ^ 2) (h₂ : ∃ (R : Polynomial 𝕜), P₂.comp (U + Q) = P₂.comp U + (Polynomial.derivative P₂).comp U * Q + R * Q ^ 2) : ∃ (R : Polynomial 𝕜), (P₁ + P₂).comp (U + Q) = (P₁ + P₂).comp U + (Polynomial.derivative (P₁ + P₂)).comp U * Q + R * Q ^ 2

The first-order expansion property is preserved under addition (for fixed U and Q).

theorem SomeLocalRings.polynomial_comp_add_eq_add_derivative_comp_mul_add_mul_sq {𝕜 : Type u_1} [Field 𝕜] (P U Q : Polynomial 𝕜) : ∃ (R : Polynomial 𝕜), P.comp (U + Q) = P.comp U + (Polynomial.derivative P).comp U * Q + R * Q ^ 2

A first-order Taylor expansion of P.comp around an arbitrary center U.

theorem SomeLocalRings.mk_derivative_ne_zero_mod_irreducible {𝕜 : Type u_1} [Field 𝕜] (P : Polynomial 𝕜) (hP : Irreducible P) (hP' : Polynomial.derivative P ≠ 0) : (AdjoinRoot.mk P) (Polynomial.derivative P) ≠ 0

If P is irreducible and P' ≠ 0, then the class of P' in 𝕜[X]/(P) is nonzero.

theorem SomeLocalRings.mk_comp_eq_mk_of_dvd_sub {𝕜 : Type u_1} [Field 𝕜] (P f U : Polynomial 𝕜) (hUX : P ∣ U - Polynomial.X) : (AdjoinRoot.mk P) (f.comp U) = (AdjoinRoot.mk P) f

If P ∣ U - X, then composing a polynomial with U does not change its class in 𝕜[X]/(P).

theorem SomeLocalRings.exists_S_kill_Rn_mod_P {𝕜 : Type u_1} [Field 𝕜] (P U Rn : Polynomial 𝕜) (hP : Irreducible P) (hP' : Polynomial.derivative P ≠ 0) (hUX : P ∣ U - Polynomial.X) : ∃ (S : Polynomial 𝕜), P ∣ Rn + (Polynomial.derivative P).comp U * S

Given U ≡ X (mod P), choose S so that Rn + (P' ∘ U) * S ≡ 0 (mod P).

This uses that 𝕜[X]/(P) is a field (since P is irreducible) and that P' is nonzero mod P.

theorem SomeLocalRings.hensel_step {𝕜 : Type u_1} [Field 𝕜] (P U Rn : Polynomial 𝕜) (n : ℕ) (hP : Irreducible P) (hP' : Polynomial.derivative P ≠ 0) (hUX : P ∣ U - Polynomial.X) (hcomp : P.comp U = Rn * P ^ (n + 1)) : ∃ (S : Polynomial 𝕜) (Rn1 : Polynomial 𝕜), P.comp (U + S * P ^ (n + 1)) = Rn1 * P ^ (n + 2)

One Hensel-style lifting step: if P.comp U is divisible by P^(n+1) and U ≡ X (mod P), then we can adjust U by S * P^(n+1) so that P.comp becomes divisible by P^(n+2).

structure SomeLocalRings.LiftState {𝕜 : Type u_1} [Field 𝕜] (P : Polynomial 𝕜) (n : ℕ) : Type u_1

State used to build the sequences in Lemma 1.2 by recursion on n.

• U : Polynomial 𝕜
• R : Polynomial 𝕜
• q : Polynomial 𝕜
• hcomp : P.comp self.U = self.R * P ^ (n + 1)
• hmod : P ∣ self.U - Polynomial.X

theorem SomeLocalRings.exists_polynomial_sequences_comp_X_add_sum_mul_pow_eq_mul_pow {𝕜 : Type u_1} [Field 𝕜] (P : Polynomial 𝕜) (hP : Irreducible P) (hP' : Polynomial.derivative P ≠ 0) : ∃ (Q : ℕ → Polynomial 𝕜) (R : ℕ → Polynomial 𝕜), ∀ (k : ℕ), P.comp (Polynomial.X + ∑ i ∈ Finset.range k, Q (i + 1) * P ^ (i + 1)) = R k * P ^ (k + 1)

Lemma 1.2. Let 𝕜 be a field and P be an irreducible polynomial over 𝕜. If P' ≠ 0, then there exists an infinite sequence of pairs of polynomials (Q₀, R₀), (Q₁, R₁), … such that for all k ≥ 0, P(X + ∑_{i=1}^k Qᵢ(X) * P(X)^i) = Rₖ(X) * P(X)^(k+1).

theorem SomeLocalRings.aeval_mk_eq_mk_comp {𝕜 : Type u_1} [Field 𝕜] (f U p : Polynomial 𝕜) : (Polynomial.aeval ((AdjoinRoot.mk f) U)) p = (AdjoinRoot.mk f) (p.comp U)

Evaluating a polynomial p at mk f U in AdjoinRoot f corresponds to taking p.comp U modulo f.

theorem SomeLocalRings.prop1_3_comp_eq_mul_pow {𝕜 : Type u_1} [Field 𝕜] (P : Polynomial 𝕜) (Q R : ℕ → Polynomial 𝕜) (k : ℕ) (hk : 1 ≤ k) (hQR : ∀ (n : ℕ), P.comp (Polynomial.X + ∑ i ∈ Finset.range n, Q (i + 1) * P ^ (i + 1)) = R n * P ^ (n + 1)) : P.comp (Polynomial.X + ∑ i ∈ Finset.range (k - 1), Q (i + 1) * P ^ (i + 1)) = R (k - 1) * P ^ k

For U := X + ∑ i < k - 1, Q (i+1) * P^(i+1), Lemma 1.2 gives P.comp U = R (k-1) * P^k.

theorem SomeLocalRings.prop1_3_dvd_sub_X {𝕜 : Type u_1} [Field 𝕜] (P : Polynomial 𝕜) (Q : ℕ → Polynomial 𝕜) (n : ℕ) : P ∣ Polynomial.X + ∑ i ∈ Finset.range n, Q (i + 1) * P ^ (i + 1) - Polynomial.X

The polynomial X + ∑ i < n, Q (i+1) * P^(i+1) is congruent to X modulo P.

theorem SomeLocalRings.prop1_3_aeval_root_pow_eq_zero {𝕜 : Type u_1} [Field 𝕜] (P : Polynomial 𝕜) (k : ℕ) (hk : k ≠ 0) : (Polynomial.aeval (AdjoinRoot.root P)) (P ^ k) = 0

In AdjoinRoot P, the element root P is a root of P^k for k ≠ 0.

theorem SomeLocalRings.exists_injective_algHom_adjoinRoot_to_adjoinRoot_pow {𝕜 : Type u_1} [Field 𝕜] (P : Polynomial 𝕜) (hP : Irreducible P) (hP' : Polynomial.derivative P ≠ 0) (k : ℕ) : 1 ≤ k → ∃ (f : AdjoinRoot P →ₐ[𝕜] AdjoinRoot (P ^ k)), Function.Injective ⇑f

Proposition 1.3. Let 𝕜 be a field and let P be an irreducible polynomial over 𝕜. If P' ≠ 0, then for every k ≥ 1 there exists an injective 𝕜-algebra morphism from the field 𝕜[X]⧸(P) into 𝕜[X]⧸(P^k).

theorem SomeLocalRings.exists_residueField_algEquiv_subalgebra_adjoinRoot_pow {𝕜 : Type u_1} [Field 𝕜] (P : Polynomial 𝕜) (hP : Irreducible P) (hP' : Polynomial.derivative P ≠ 0) (k : ℕ) : 1 ≤ k → ∃ (S : Subalgebra 𝕜 (AdjoinRoot (P ^ k))), Nonempty (AdjoinRoot P ≃ₐ[𝕜] ↥S)

Corollary 1.4. Let 𝕜 be a field and P be an irreducible polynomial over 𝕜. If P' ≠ 0, then for every k ≥ 1, the quotient 𝕜[X]⧸(P ^ k) contains 𝕜[X]⧸(P) as a 𝕜-subalgebra.

theorem SomeLocalRings.nonempty_algebra_adjoinRoot_pow_over_adjoinRoot {𝕜 : Type u_1} [Field 𝕜] (P : Polynomial 𝕜) (hP : Irreducible P) (hP' : Polynomial.derivative P ≠ 0) (k : ℕ) : 1 ≤ k → Nonempty (Algebra (AdjoinRoot P) (AdjoinRoot (P ^ k)))

Corollary 1.5. Let 𝕜 be a field and P be an irreducible polynomial over 𝕜. If P' ≠ 0, then for every k ≥ 1 the local ring 𝕜[X]⧸(P ^ k) admits the structure of an algebra over 𝕜[X]⧸(P).

theorem SomeLocalRings.mk_pow_eq_pow_mk {𝕜 : Type u_1} [Field 𝕜] (P : Polynomial 𝕜) (k n : ℕ) : (AdjoinRoot.mk (P ^ k)) (P ^ n) = (AdjoinRoot.mk (P ^ k)) P ^ n

In AdjoinRoot (P^k), the class of P^n is the n-th power of the class of P.

theorem SomeLocalRings.beta_pow_k_eq_zero {𝕜 : Type u_1} [Field 𝕜] (P : Polynomial 𝕜) (k : ℕ) : (AdjoinRoot.mk (P ^ k)) P ^ k = 0

In AdjoinRoot (P^k), the class of P is nilpotent of index k.

theorem SomeLocalRings.beta_pow_pred_ne_zero {𝕜 : Type u_1} [Field 𝕜] (P : Polynomial 𝕜) (hP : Irreducible P) (k : ℕ) (hk : 1 ≤ k) : (AdjoinRoot.mk (P ^ k)) P ^ (k - 1) ≠ 0

In AdjoinRoot (P^k), the class of P^(k-1) is nonzero when P is irreducible and k ≥ 1.

theorem SomeLocalRings.coeffs_eq_zero_of_sum_smul_pows_eq_zero {𝕜 : Type u_1} [Field 𝕜] (P : Polynomial 𝕜) (hP : Irreducible P) (k : ℕ) (hk : 1 ≤ k) [Algebra (AdjoinRoot P) (AdjoinRoot (P ^ k))] (g : Fin k → AdjoinRoot P) : ∑ i : Fin k, g i • (AdjoinRoot.mk (P ^ k)) P ^ ↑i = 0 → ∀ (j : Fin k), g j = 0

Descending elimination for relations among 1, β, …, β^(k-1) in AdjoinRoot (P^k).

theorem SomeLocalRings.linearIndependent_powers_mk_adjoinRoot_pow {𝕜 : Type u_1} [Field 𝕜] (P : Polynomial 𝕜) (hP : Irreducible P) (hP' : Polynomial.derivative P ≠ 0) (k : ℕ) (hk : 1 ≤ k) [Algebra (AdjoinRoot P) (AdjoinRoot (P ^ k))] : LinearIndependent (AdjoinRoot P) fun (i : Fin k) => (AdjoinRoot.mk (P ^ k)) (P ^ ↑i)

Lemma 1.6. Let 𝕜 be a field and P be an irreducible polynomial over 𝕜. If P' ≠ 0, then for every k ≥ 1, the family 1, P, P^2, …, P^(k-1) in 𝕜[X]⧸(P^k) is linearly independent over 𝕜[X]⧸(P).

noncomputable def SomeLocalRings.psiK {𝕜 : Type u_1} [Field 𝕜] (P : Polynomial 𝕜) (k : ℕ) [Algebra (AdjoinRoot P) (AdjoinRoot (P ^ k))] : AdjoinRoot (Polynomial.X ^ k) →ₐ[AdjoinRoot P] AdjoinRoot (P ^ k)

The algebra map ψₖ sending the class of X in AdjoinRoot (X^k) to the class of P.

Equations

• SomeLocalRings.psiK P k = AdjoinRoot.liftAlgHom (Polynomial.X ^ k) (Algebra.ofId (AdjoinRoot P) (AdjoinRoot (P ^ k))) ((AdjoinRoot.mk (P ^ k)) P) ⋯

theorem SomeLocalRings.psiK_def_and_root {𝕜 : Type u_1} [Field 𝕜] (P : Polynomial 𝕜) (k : ℕ) [Algebra (AdjoinRoot P) (AdjoinRoot (P ^ k))] : (psiK P k) (AdjoinRoot.root (Polynomial.X ^ k)) = (AdjoinRoot.mk (P ^ k)) P

theorem SomeLocalRings.psiK_injective {𝕜 : Type u_1} [Field 𝕜] (P : Polynomial 𝕜) (hP : Irreducible P) (hP' : Polynomial.derivative P ≠ 0) (k : ℕ) (hk : 1 ≤ k) [Algebra (AdjoinRoot P) (AdjoinRoot (P ^ k))] : Function.Injective ⇑(psiK P k)

Injectivity of ψₖ, deduced from the linear independence of 1, P, …, P^(k-1) (Lemma 1.6).

theorem SomeLocalRings.finrank_domain_over_adjoinRoot_eq_k {𝕜 : Type u_1} [Field 𝕜] (P : Polynomial 𝕜) (hP : Irreducible P) (k : ℕ) : Module.finrank (AdjoinRoot P) (AdjoinRoot (Polynomial.X ^ k)) = k

The AdjoinRoot P-dimension of AdjoinRoot (X^k) is k.