Galois-invariant monogenic orders in cyclic fields of prime degree: the algebraic core

In any commutative ring R:

• four Bézout certificates (by ring): A Φ₅(t) − B((t+1)⁵ − 1) = 11, A' Φ₅(t) + B'((t+1)⁵ + 1) = 11, C Φ₇(t) − D((t+1)⁷ − 1) = 58, C' Φ₇(t) + D'((t+1)⁷ + 1) = 86;
• hence Φ_ℓ(t) ∈ I and (1 + t)^ℓ − ε ∈ I (ε = ±1) give 11 ∈ I (ℓ = 5), and 58 ∈ I resp. 86 ∈ I (ℓ = 7);
• the congruence step, for every ℓ: with σ : R →+* R, σ^[ℓ] = id, d = σα − α, σd = t d, σ trivial modulo dR, d a non-zero-divisor and ∏_{j<ℓ} σ^[j](1 + t) = ε, one has ∑_{j<ℓ} t^j ∈ (d) and (1 + t)^ℓ − ε ∈ (d). That these hypotheses hold for a Galois-invariant monogenic order, ramification, the conductor, local maximality at 11 and Gras's theorem are not formalized; primality of ℓ is not used.

Main results

• Louboutin.QuinticBezout.bezout5_plus, bezout5_minus, bezout7_plus, bezout7_minus.
• Louboutin.QuinticBezout.eleven_mem, fiftyeight_mem, eightysix_mem.
• Louboutin.QuinticBezout.cyclotomic_mem, Louboutin.QuinticBezout.norm_mem, Louboutin.QuinticBezout.quintic_eleven_mem, Louboutin.QuinticBezout.septic_mem_span.

References

• M.-N. Gras, Non monogénéité de l'anneau des entiers des extensions cycliques de ℚ de degré premier l ≥ 5, J. Number Theory 23 (1986), 347–353.
• C. Marín, Orders generated by conjugates of Galois quartic integers, preprint (2026).

def Louboutin.QuinticBezout.phi5 {R : Type u_1} [CommRing R] (t : R) : R

Φ₅(t).

Equations

• Louboutin.QuinticBezout.phi5 t = t ^ 4 + t ^ 3 + t ^ 2 + t + 1

def Louboutin.QuinticBezout.phi7 {R : Type u_1} [CommRing R] (t : R) : R

Φ₇(t).

Equations

• Louboutin.QuinticBezout.phi7 t = t ^ 6 + t ^ 5 + t ^ 4 + t ^ 3 + t ^ 2 + t + 1

S1 Bézout certificates

theorem Louboutin.QuinticBezout.bezout5_plus {R : Type u_1} [CommRing R] (t : R) : (5 * t ^ 4 + 25 * t ^ 3 + 45 * t ^ 2 + 34 * t + 11) * phi5 t - (5 * t ^ 3 + 5 * t ^ 2 + 9) * ((t + 1) ^ 5 - 1) = 11

theorem Louboutin.QuinticBezout.bezout5_minus {R : Type u_1} [CommRing R] (t : R) : (-5 * t ^ 4 - 25 * t ^ 3 - 45 * t ^ 2 - 32 * t - 3) * phi5 t + (5 * t ^ 3 + 5 * t ^ 2 + 7) * ((t + 1) ^ 5 + 1) = 11

theorem Louboutin.QuinticBezout.bezout7_plus {R : Type u_1} [CommRing R] (t : R) : (28 * t ^ 6 + 175 * t ^ 5 + 441 * t ^ 4 + 560 * t ^ 3 + 364 * t ^ 2 + 124 * t + 58) * phi7 t - (28 * t ^ 5 + 7 * t ^ 4 + 7 * t ^ 3 + 28 * t ^ 2 + 26) * ((t + 1) ^ 7 - 1) = 58

theorem Louboutin.QuinticBezout.bezout7_minus {R : Type u_1} [CommRing R] (t : R) : (-35 * t ^ 6 - 231 * t ^ 5 - 637 * t ^ 4 - 945 * t ^ 3 - 798 * t ^ 2 - 346 * t - 18) * phi7 t + (35 * t ^ 5 + 21 * t ^ 4 + 21 * t ^ 3 + 35 * t ^ 2 + 52) * ((t + 1) ^ 7 + 1) = 86

S2 Ideal corollaries

theorem Louboutin.QuinticBezout.eleven_mem {R : Type u_1} [CommRing R] {I : Ideal R} {t ε : R} (hε : ε = 1 ∨ ε = -1) (hΦ : phi5 t ∈ I) (hN : (1 + t) ^ 5 - ε ∈ I) : 11 ∈ I

theorem Louboutin.QuinticBezout.fiftyeight_mem {R : Type u_1} [CommRing R] {I : Ideal R} {t : R} (hΦ : phi7 t ∈ I) (hN : (1 + t) ^ 7 - 1 ∈ I) : 58 ∈ I

theorem Louboutin.QuinticBezout.eightysix_mem {R : Type u_1} [CommRing R] {I : Ideal R} {t : R} (hΦ : phi7 t ∈ I) (hN : (1 + t) ^ 7 - -1 ∈ I) : 86 ∈ I

theorem Louboutin.QuinticBezout.septic_mem {R : Type u_1} [CommRing R] {I : Ideal R} {t ε : R} (hΦ : phi7 t ∈ I) (hN : (1 + t) ^ 7 - ε ∈ I) : (ε = 1 → 58 ∈ I) ∧ (ε = -1 → 86 ∈ I)

S3 The congruence step (generic ℓ)

theorem Louboutin.QuinticBezout.iter_mul {R : Type u_1} [CommRing R] (σ : R →+* R) (j : ℕ) (x y : R) : (⇑σ)^[j] (x * y) = (⇑σ)^[j] x * (⇑σ)^[j] y

theorem Louboutin.QuinticBezout.iter_sub {R : Type u_1} [CommRing R] (σ : R →+* R) (j : ℕ) (x y : R) : (⇑σ)^[j] (x - y) = (⇑σ)^[j] x - (⇑σ)^[j] y

theorem Louboutin.QuinticBezout.iter_d {R : Type u_1} [CommRing R] (σ : R →+* R) (d t : R) (H1 : σ d = t * d) (j : ℕ) : (⇑σ)^[j] d = (∏ i ∈ Finset.range j, (⇑σ)^[i] t) * d

σ^[j] d = (∏_{i<j} σ^[i] t) · d.

theorem Louboutin.QuinticBezout.iter_mk {R : Type u_1} [CommRing R] (σ : R →+* R) (d : R) (H2 : ∀ (x : R), ∃ (y : R), σ x - x = d * y) (j : ℕ) (x : R) : (Ideal.Quotient.mk (Ideal.span {d})) ((⇑σ)^[j] x) = (Ideal.Quotient.mk (Ideal.span {d})) x

σ is trivial mod (d), hence so are its iterates.

theorem Louboutin.QuinticBezout.cyclotomic_mem {R : Type u_1} [CommRing R] (σ : R →+* R) (ℓ : ℕ) (α t : R) (hℓ : ∀ (x : R), (⇑σ)^[ℓ] x = x) (H1 : σ (σ α - α) = t * (σ α - α)) (H2 : ∀ (x : R), ∃ (y : R), σ x - x = (σ α - α) * y) (H3 : ∀ (z : R), (σ α - α) * z = 0 → z = 0) : ∑ j ∈ Finset.range ℓ, t ^ j ∈ Ideal.span {σ α - α}

Main congruence step: Φ_ℓ(t) = Σ_{j<ℓ} t^j ∈ (d), d = σα − α.

theorem Louboutin.QuinticBezout.norm_mem {R : Type u_1} [CommRing R] (σ : R →+* R) (ℓ : ℕ) (d t ε : R) (H2 : ∀ (x : R), ∃ (y : R), σ x - x = d * y) (H4 : ∏ j ∈ Finset.range ℓ, (⇑σ)^[j] (1 + t) = ε) : (1 + t) ^ ℓ - ε ∈ Ideal.span {d}

Norm congruence: (1+t)^ℓ − ε ∈ (d).

theorem Louboutin.QuinticBezout.phi5_eq {R : Type u_1} [CommRing R] (t : R) : phi5 t = ∑ j ∈ Finset.range 5, t ^ j

theorem Louboutin.QuinticBezout.phi7_eq {R : Type u_1} [CommRing R] (t : R) : phi7 t = ∑ j ∈ Finset.range 7, t ^ j

theorem Louboutin.QuinticBezout.quintic_eleven_mem {R : Type u_1} [CommRing R] (σ : R →+* R) (α t ε : R) (hε : ε = 1 ∨ ε = -1) (hℓ : ∀ (x : R), (⇑σ)^[5] x = x) (H1 : σ (σ α - α) = t * (σ α - α)) (H2 : ∀ (x : R), ∃ (y : R), σ x - x = (σ α - α) * y) (H3 : ∀ (z : R), (σ α - α) * z = 0 → z = 0) (H4 : ∏ j ∈ Finset.range 5, (⇑σ)^[j] (1 + t) = ε) : 11 ∈ Ideal.span {σ α - α}

ℓ = 5: 11 ∈ (σα − α).

theorem Louboutin.QuinticBezout.septic_mem_span {R : Type u_1} [CommRing R] (σ : R →+* R) (α t ε : R) (hℓ : ∀ (x : R), (⇑σ)^[7] x = x) (H1 : σ (σ α - α) = t * (σ α - α)) (H2 : ∀ (x : R), ∃ (y : R), σ x - x = (σ α - α) * y) (H3 : ∀ (z : R), (σ α - α) * z = 0 → z = 0) (H4 : ∏ j ∈ Finset.range 7, (⇑σ)^[j] (1 + t) = ε) : (ε = 1 → 58 ∈ Ideal.span {σ α - α}) ∧ (ε = -1 → 86 ∈ Ideal.span {σ α - α})

ℓ = 7: 58 ∈ (σα − α) if ε = 1, 86 ∈ (σα − α) if ε = −1.