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

The AdjoinRoot P-dimension of AdjoinRoot (P^k) is k under the scalar tower hypothesis.

theorem SomeLocalRings.exists_algEquiv_adjoinRoot_X_pow_to_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))] [IsScalarTower 𝕜 (AdjoinRoot P) (AdjoinRoot (P ^ k))] : ∃ (e : AdjoinRoot (Polynomial.X ^ k) ≃ₐ[AdjoinRoot P] AdjoinRoot (P ^ k)), e (AdjoinRoot.root (Polynomial.X ^ k)) = (AdjoinRoot.mk (P ^ k)) P

Theorem 1.7. Let 𝕜 be a field and P be an irreducible polynomial over 𝕜. If P' ≠ 0, then 𝕜[X]⧸(P ^ k) is isomorphic, as an 𝕜[X]⧸(P)-algebra (and hence as a 𝕜-algebra), to (𝕜[X]⧸(P))[Y]⧸(Y ^ k). The isomorphism is given by Y ↦ P.

theorem SomeLocalRings.nilradical_map_eq_of_ringEquiv {R : Type u_2} {S : Type u_3} [CommSemiring R] [CommSemiring S] (e : R ≃+* S) : Ideal.map (↑e) (nilradical R) = nilradical S

A ring equivalence preserves the nilradical ideal.

noncomputable def SomeLocalRings.quotient_span_root_adjoinRoot_X_pow_ringEquiv_base (A : Type u_2) [CommRing A] (k : ℕ) (hk : 1 ≤ k) : AdjoinRoot (Polynomial.X ^ k) ⧸ Ideal.span {AdjoinRoot.root (Polynomial.X ^ k)} ≃+* A

The quotient of A[Y]/(Y^k) by the ideal (Y) is canonically isomorphic to A.

We present A[Y]/(Y^k) as AdjoinRoot (X^k) and the ideal (Y) as the span of the adjoined root.

Equations

• One or more equations did not get rendered due to their size.

theorem SomeLocalRings.quotient_span_root_adjoinRoot_X_pow_ringEquiv_base_algebraMap (A : Type u_2) [CommRing A] (k : ℕ) (hk : 1 ≤ k) (a : A) : (quotient_span_root_adjoinRoot_X_pow_ringEquiv_base A k hk) ((algebraMap A (AdjoinRoot (Polynomial.X ^ k) ⧸ Ideal.span {AdjoinRoot.root (Polynomial.X ^ k)})) a) = a

The isomorphism A[Y]/(Y^k)/(Y) ≃ A sends scalars to scalars.

theorem SomeLocalRings.nilradical_adjoinRoot_X_pow_eq_span_root (A : Type u_2) [Field A] (k : ℕ) (hk : 1 ≤ k) : nilradical (AdjoinRoot (Polynomial.X ^ k)) = Ideal.span {AdjoinRoot.root (Polynomial.X ^ k)}

For a field A, the nilradical of A[Y]/(Y^k) (presented as AdjoinRoot (X^k)) is the ideal generated by Y, i.e. the span of the adjoined root.

theorem SomeLocalRings.nonempty_ringEquiv_adjoinRoot_X_pow_iff_nonempty_ringEquiv_base (A : Type u_2) (B : Type u_3) [Field A] [Field B] (k : ℕ) (hk : 1 ≤ k) : Nonempty (AdjoinRoot (Polynomial.X ^ k) ≃+* AdjoinRoot (Polynomial.X ^ k)) ↔ Nonempty (A ≃+* B)

For fields A and B, the truncated polynomial rings A[Y]/(Y^k) and B[Y]/(Y^k) (presented as AdjoinRoot (X^k)) are isomorphic if and only if A and B are isomorphic.

theorem SomeLocalRings.nonempty_algEquiv_adjoinRoot_X_pow_iff_nonempty_algEquiv_base {𝕜 : Type u_1} [Field 𝕜] (A : Type u_2) (B : Type u_3) [Field A] [Field B] [Algebra 𝕜 A] [Algebra 𝕜 B] (k : ℕ) (hk : 1 ≤ k) : Nonempty (AdjoinRoot (Polynomial.X ^ k) ≃ₐ[𝕜] AdjoinRoot (Polynomial.X ^ k)) ↔ Nonempty (A ≃ₐ[𝕜] B)

For 𝕜-algebra fields A and B, the truncated polynomial rings A[Y]/(Y^k) and B[Y]/(Y^k) (presented as AdjoinRoot (X^k)) are isomorphic as 𝕜-algebras if and only if A and B are isomorphic as 𝕜-algebras.

theorem SomeLocalRings.nonempty_ringEquiv_adjoinRoot_pow_iff_nonempty_ringEquiv_adjoinRoot {𝕜 : Type u_1} [Field 𝕜] (P₁ P₂ : Polynomial 𝕜) (hP₁ : Irreducible P₁) (hP₂ : Irreducible P₂) (hP₁' : Polynomial.derivative P₁ ≠ 0) (hP₂' : Polynomial.derivative P₂ ≠ 0) (k : ℕ) (hk : 1 ≤ k) : Nonempty (AdjoinRoot (P₁ ^ k) ≃+* AdjoinRoot (P₂ ^ k)) ↔ Nonempty (AdjoinRoot P₁ ≃+* AdjoinRoot P₂)

Theorem 1.8. Let 𝕜 be a field. Let P₁ and P₂ be irreducible polynomials over 𝕜 and let k be a positive integer. If P₁ and P₂ are separable (i.e. Pᵢ' ≠ 0), then the local rings 𝕜[X]⧸(P₁ ^ k) and 𝕜[X]⧸(P₂ ^ k) are isomorphic if and only if their residue fields 𝕜[X]⧸(P₁) and 𝕜[X]⧸(P₂) are isomorphic.

theorem SomeLocalRings.nonempty_algEquiv_adjoinRoot_pow_iff_nonempty_algEquiv_adjoinRoot {𝕜 : Type u_1} [Field 𝕜] (P₁ P₂ : Polynomial 𝕜) (hP₁ : Irreducible P₁) (hP₂ : Irreducible P₂) (hP₁' : Polynomial.derivative P₁ ≠ 0) (hP₂' : Polynomial.derivative P₂ ≠ 0) (k : ℕ) (hk : 1 ≤ k) : Nonempty (AdjoinRoot (P₁ ^ k) ≃ₐ[𝕜] AdjoinRoot (P₂ ^ k)) ↔ Nonempty (AdjoinRoot P₁ ≃ₐ[𝕜] AdjoinRoot P₂)

Proposition 1.10. Let P₁ and P₂ be two irreducible polynomials over 𝕜 and k a positive integer. If P₁ and P₂ are separable (i.e. Pᵢ' ≠ 0), then the local rings 𝕜[X]⧸(P₁ ^ k) and 𝕜[X]⧸(P₂ ^ k) are isomorphic as 𝕜-algebras if and only if their residue fields 𝕜[X]⧸(P₁) and 𝕜[X]⧸(P₂) are isomorphic as 𝕜-algebras.