Cubic fields $K=\mathbb{Q}[x]/(x^3+dx+e)$ : the field, the integral model, and $\mathbb{Z}[\theta]$

Definition

CollapsibleCubics_q7

by quesswho · Sep 8, 2026 · Mathlib 0df444a (Lean v4.33.1)

algebraalgebraic-number-theorynumber-theory

The objects needed to state splitting questions for a depressed cubic. For $d,e\in\mathbb{Q}$ we write $m(x)=x^3+dx+e$ (cubicPoly) and, when $m$ is irreducible, $K=\mathbb{Q}[x]/(m)$ (CubicField), realised as an AdjoinRoot. For $D,E\in\mathbb{Z}$ the same cubic over $\mathbb{Z}$ (cubicPolyInt) is monic, so its root $\theta$ is integral over $\mathbb{Z}$ and lands in the ring of integers $\mathcal{O}_K$ (thetaO). Finally adjoinAddSubgroup views the order $\mathbb{Z}[\theta]\subseteq\mathcal{O}_K$ as an additive subgroup, which is what the index $[\mathcal{O}_K:\mathbb{Z}[\theta]]$ is taken of.

Definition code

import Mathlib

namespace CollapsibleCubics

open Polynomial NumberField

variable (d e : ℚ)

/-- The depressed cubic `x ^ 3 + d * x + e` as an element of `ℚ[X]`. -/
noncomputable def cubicPoly : ℚ[X] := X ^ 3 + C d * X + C e

/-- The cubic field `K = ℚ[X] / (x ^ 3 + d * x + e)`, realised as an `AdjoinRoot`. -/
noncomputable abbrev CubicField := AdjoinRoot (cubicPoly d e)

variable (D E : ℤ)

/-- The depressed cubic `x ^ 3 + D * x + E` as an element of `ℤ[X]`. -/
noncomputable def cubicPolyInt : ℤ[X] := X ^ 3 + C D * X + C E

theorem cubicPolyInt_monic : (cubicPolyInt D E).Monic := by
  unfold cubicPolyInt; monicity!

/-- The integer cubic maps to the rational one under `ℤ[X] → ℚ[X]`. -/
theorem cubicPolyInt_map :
    (cubicPolyInt D E).map (algebraMap ℤ ℚ) = cubicPoly (D : ℚ) (E : ℚ) := by
  unfold cubicPolyInt cubicPoly
  simp

/-- `θ = AdjoinRoot.root (cubicPoly D E)` is integral over `ℤ`. Stated with no irreducibility
hypothesis, so the `CommRing (AdjoinRoot ...)` instance here is the plain quotient-ring one. -/
theorem isIntegral_root : IsIntegral ℤ (AdjoinRoot.root (cubicPoly (D : ℚ) (E : ℚ))) := by
  refine ⟨cubicPolyInt D E, cubicPolyInt_monic D E, ?_⟩
  rw [← Polynomial.aeval_def, ← Polynomial.aeval_map_algebraMap ℚ, cubicPolyInt_map]
  simp

variable [hf : Fact (Irreducible (cubicPoly (D : ℚ) (E : ℚ)))]

/-- `θ`, packaged as an element of `𝓞 K` for `K = CubicField D E`. -/
noncomputable def thetaO : 𝓞 (CubicField (D : ℚ) (E : ℚ)) :=
  ⟨AdjoinRoot.root (cubicPoly (D : ℚ) (E : ℚ)), isIntegral_root D E⟩

variable {K : Type*} [Field K] [NumberField K]

/-- `ℤ[θ] = Algebra.adjoin ℤ {θ}`, viewed as an `AddSubgroup (𝓞 K)`. -/
noncomputable def adjoinAddSubgroup (θ : 𝓞 K) : AddSubgroup (𝓞 K) :=
  (Algebra.adjoin ℤ {θ}).toSubmodule.toAddSubgroup

end CollapsibleCubics

Source

https://quesswho.github.io/miles-blog/2026/08/20/collapsible/ (Collapsible Cubics mission; Macris Problem 3)

View graph

Cubic fields K=Q[x]/(x3+dx+e)K=\mathbb{Q}[x]/(x^3+dx+e)K=Q[x]/(x3+dx+e): the field, the integral model, and Z[θ]\mathbb{Z}[\theta]Z[θ]

Cubic fields $K=\mathbb{Q}[x]/(x^3+dx+e)$ : the field, the integral model, and $\mathbb{Z}[\theta]$