Further questions of Louboutin: cyclic prime degree, powers of α, and a quintic unit

Abstract models; no number field is constructed.

• Cyclic prime degree: K a field, σ ∈ RingAut K with σ^ℓ = 1, ℓ an odd prime, O = ℤ[α] stable under σ, σα ≠ α; N(x) = ∏_{h<ℓ} σʰx, IsU O x for "x ∈ O^×", d_k = σᵏα − α. The ratios (σⁱα − σʲα)/d₁ are units for i ≢ j; η = d₂/d₁ satisfies η − 1 = σ(d₁)/d₁, 1 − η ∈ O^×, N(η − 1) = 1, N(1 − η) = −1; for every ring hom from O to a finite field F, ℓ ≤ |F|, and if |F| = pᶠ with p < ℓ and f ∣ ℓ then f = ℓ.
• Powers of α: N a commutative ring with a group G acting by ring automorphisms and an additive valuation v (v x = ⊤ → x = 0); if 0 < v(gα) for all g, gα ≠ α for some g and k ≥ 2, then ℤ[conj αᵏ] ≠ ℤ[conj α]. For α³ − Cα + C = 0, C = C'² + C' + 7: ℤ[conj αᵏ] = ℤ[conj α] iff k = 1.
• A quintic unit: ε = ζᵃw with ζ⁵ = 1, complex conjugation c with c·ζ = ζ⁴, c·w = w, 5 ∤ a, norm 1: ℤ[conj εᵏ] = ℤ[ζ] for every k with 5 ∤ k.

Main results

• Louboutin.SeccionSeis.lem_ratios, Louboutin.SeccionSeis.cor_inert.
• Louboutin.SeccionSeis.prop_val, Louboutin.SeccionSeis.prop_val_poly, Louboutin.SeccionSeis.cor_q25.
• Louboutin.SeccionSeis.prop_c27.

References

• S. R. Louboutin, On the order generated by the conjugates of an algebraic integer, in: Algebra, Logic and Number Theory, Banach Center Publ. 121 (2020), 107–124, doi:10.4064/bc121-10.
• S. R. Louboutin, When is the order generated by a cubic, quartic or quintic algebraic unit Galois invariant: three conjectures, Czechoslovak Math. J. 70 (2020), 905–919, doi:10.21136/CMJ.2020.0019-19.
• C. Marín, Orders generated by conjugates of Galois quartic integers, preprint (2026).

Cyclic fields of odd prime degree: lem:ratios and cor:inert

theorem Louboutin.SeccionSeis.pow_apply_add {K : Type u_1} [Field K] (σ : RingAut K) (m n : ℕ) (x : K) : (σ ^ (m + n)) x = (σ ^ m) ((σ ^ n) x)

theorem Louboutin.SeccionSeis.pow_succ_apply {K : Type u_1} [Field K] (σ : RingAut K) (n : ℕ) (x : K) : (σ ^ (n + 1)) x = (σ ^ n) (σ x)

def Louboutin.SeccionSeis.nrm {K : Type u_1} [Field K] (σ : RingAut K) (ℓ : ℕ) (x : K) : K

The norm N_{K/ℚ}(x) = ∏_{h<ℓ} σʰ(x) of a cyclic extension of degree ℓ generated by σ.

Equations

• Louboutin.SeccionSeis.nrm σ ℓ x = ∏ h ∈ Finset.range ℓ, (σ ^ h) x

def Louboutin.SeccionSeis.IsU {K : Type u_1} [Field K] (O : Subring K) (x : K) : Prop

x ∈ O^×: x is a nonzero element of O whose inverse lies in O.

Equations

• Louboutin.SeccionSeis.IsU O x = (x ≠ 0 ∧ x ∈ O ∧ x⁻¹ ∈ O)

theorem Louboutin.SeccionSeis.nrm_mul {K : Type u_1} [Field K] (σ : RingAut K) (ℓ : ℕ) (x y : K) : nrm σ ℓ (x * y) = nrm σ ℓ x * nrm σ ℓ y

theorem Louboutin.SeccionSeis.nrm_inv {K : Type u_1} [Field K] (σ : RingAut K) (ℓ : ℕ) (x : K) : nrm σ ℓ x⁻¹ = (nrm σ ℓ x)⁻¹

theorem Louboutin.SeccionSeis.nrm_ne_zero {K : Type u_1} [Field K] (σ : RingAut K) (ℓ : ℕ) {x : K} (hx : x ≠ 0) : nrm σ ℓ x ≠ 0

theorem Louboutin.SeccionSeis.nrm_neg_one {K : Type u_1} [Field K] (σ : RingAut K) (ℓ : ℕ) : nrm σ ℓ (-1) = (-1) ^ ℓ

theorem Louboutin.SeccionSeis.nrm_apply {K : Type u_1} [Field K] (σ : RingAut K) (ℓ : ℕ) (hℓ1 : σ ^ ℓ = 1) (x : K) : nrm σ ℓ (σ x) = nrm σ ℓ x

theorem Louboutin.SeccionSeis.nrm_pow_apply {K : Type u_1} [Field K] (σ : RingAut K) (ℓ : ℕ) (hℓ1 : σ ^ ℓ = 1) (k : ℕ) (x : K) : nrm σ ℓ ((σ ^ k) x) = nrm σ ℓ x

theorem Louboutin.SeccionSeis.pow_mem_of_stab {K : Type u_1} [Field K] {σ : RingAut K} {O : Subring K} (hst : ∀ x ∈ O, σ x ∈ O) (n : ℕ) {x : K} (hx : x ∈ O) : (σ ^ n) x ∈ O

theorem Louboutin.SeccionSeis.IsU.mul {K : Type u_1} [Field K] {O : Subring K} {x y : K} (hx : IsU O x) (hy : IsU O y) : IsU O (x * y)

theorem Louboutin.SeccionSeis.IsU.neg {K : Type u_1} [Field K] {O : Subring K} {x : K} (hx : IsU O x) : IsU O (-x)

theorem Louboutin.SeccionSeis.IsU.pow_apply {K : Type u_1} [Field K] {σ : RingAut K} {O : Subring K} (hst : ∀ x ∈ O, σ x ∈ O) (n : ℕ) {x : K} (hx : IsU O x) : IsU O ((σ ^ n) x)

theorem Louboutin.SeccionSeis.IsU.isUnit {K : Type u_1} [Field K] {O : Subring K} {x : K} (hx : IsU O x) : IsUnit ⟨x, ⋯⟩

theorem Louboutin.SeccionSeis.IsU.of_nrm {K : Type u_1} [Field K] {σ : RingAut K} {ℓ : ℕ} {O : Subring K} (hst : ∀ x ∈ O, σ x ∈ O) (hℓ : 1 ≤ ℓ) {u : K} (hu : u ∈ O) (hN : nrm σ ℓ u = 1 ∨ nrm σ ℓ u = -1) : IsU O u

If u ∈ O and N(u) = ±1 then u⁻¹ = ±∏_{h=1}^{ℓ-1} σʰu ∈ O (O σ-stable).

def Louboutin.SeccionSeis.dd {K : Type u_1} [Field K] (σ : RingAut K) (α : K) (k : ℕ) : K

d_k = σᵏα − α.

Equations

• Louboutin.SeccionSeis.dd σ α k = (σ ^ k) α - α

theorem Louboutin.SeccionSeis.sub_mem_dd {K : Type u_1} [Field K] {σ : RingAut K} {O : Subring K} {α : K} (hO : O = Subring.closure {α}) (hst : ∀ x ∈ O, σ x ∈ O) (k : ℕ) {z : K} (hz : z ∈ O) : ∃ q ∈ O, (σ ^ k) z - z = dd σ α k * q

For O = ℤ[α] σ-stable and τ = σᵏ: τz − z ∈ d_k·O for every z ∈ O.

theorem Louboutin.SeccionSeis.alpha_mem {K : Type u_1} [Field K] {O : Subring K} {α : K} (hO : O = Subring.closure {α}) : α ∈ O

Generic telescoping for an automorphism τ (later τ = σᵏ), e = τα − α.

theorem Louboutin.SeccionSeis.step_mem {K : Type u_1} [Field K] {O : Subring K} {α : K} (τ : RingAut K) (hO : O = Subring.closure {α}) (hst : ∀ x ∈ O, τ x ∈ O) (he : τ α - α ≠ 0) : τ (τ α - α) / (τ α - α) ∈ O

τ(e)/e ∈ O.

theorem Louboutin.SeccionSeis.nrm_step {K : Type u_1} [Field K] {α : K} (τ : RingAut K) {ℓ : ℕ} (hτℓ : τ ^ ℓ = 1) (he : τ α - α ≠ 0) : nrm τ ℓ (τ (τ α - α) / (τ α - α)) = 1

N(τ(e)/e) = 1.

theorem Louboutin.SeccionSeis.step_isU {K : Type u_1} [Field K] {O : Subring K} {α : K} (τ : RingAut K) {ℓ : ℕ} (hO : O = Subring.closure {α}) (hst : ∀ x ∈ O, τ x ∈ O) (hℓ : 1 ≤ ℓ) (hτℓ : τ ^ ℓ = 1) (he : τ α - α ≠ 0) : IsU O (τ (τ α - α) / (τ α - α))

theorem Louboutin.SeccionSeis.tel_isU {K : Type u_1} [Field K] {O : Subring K} {α : K} (τ : RingAut K) {ℓ : ℕ} (hO : O = Subring.closure {α}) (hst : ∀ x ∈ O, τ x ∈ O) (hℓ : 1 ≤ ℓ) (hτℓ : τ ^ ℓ = 1) (he : τ α - α ≠ 0) (h : ℕ) : IsU O ((τ ^ h) (τ α - α) / (τ α - α))

τʰ(e)/e = ∏_{s<h} τˢ(τ(e)/e) ∈ O^×.

theorem Louboutin.SeccionSeis.tel_sum {K : Type u_1} [Field K] {α : K} (τ : RingAut K) (m : ℕ) : ((τ ^ m) α - α) / (τ α - α) = ∑ h ∈ Finset.range m, (τ ^ h) (τ α - α) / (τ α - α)

(τᵐα − α)/e = Σ_{h<m} τʰ(e)/e.

theorem Louboutin.SeccionSeis.tel_mem {K : Type u_1} [Field K] {O : Subring K} {α : K} (τ : RingAut K) {ℓ : ℕ} (hO : O = Subring.closure {α}) (hst : ∀ x ∈ O, τ x ∈ O) (hℓ : 1 ≤ ℓ) (hτℓ : τ ^ ℓ = 1) (he : τ α - α ≠ 0) (m : ℕ) : ((τ ^ m) α - α) / (τ α - α) ∈ O

The setting of lem:ratios.

theorem Louboutin.SeccionSeis.dd_one {K : Type u_1} [Field K] (σ : RingAut K) (α : K) : dd σ α 1 = σ α - α

theorem Louboutin.SeccionSeis.dd_ne_zero {K : Type u_1} [Field K] {σ : RingAut K} {ℓ : ℕ} {α : K} (hℓ : Nat.Prime ℓ) (hℓ1 : σ ^ ℓ = 1) (hα : σ α ≠ α) {k : ℕ} (hk : ¬ℓ ∣ k) : dd σ α k ≠ 0

d_k ≠ 0 for ℓ ∤ k (σᵏα = α with k invertible mod ℓ would give σα = α).

theorem Louboutin.SeccionSeis.pow_pow_eq_one {K : Type u_1} [Field K] {σ : RingAut K} {ℓ : ℕ} (hℓ1 : σ ^ ℓ = 1) (k : ℕ) : (σ ^ k) ^ ℓ = 1

theorem Louboutin.SeccionSeis.ratio_isU {K : Type u_1} [Field K] {σ : RingAut K} {ℓ : ℕ} {O : Subring K} {α : K} (hℓ : Nat.Prime ℓ) (hℓ1 : σ ^ ℓ = 1) (hO : O = Subring.closure {α}) (hst : ∀ x ∈ O, σ x ∈ O) (hα : σ α ≠ α) {k : ℕ} (hk : ¬ℓ ∣ k) : IsU O (dd σ α k / dd σ α 1)

d_k/d₁ ∈ O^× for ℓ ∤ k.

theorem Louboutin.SeccionSeis.ratios_isU {K : Type u_1} [Field K] {σ : RingAut K} {ℓ : ℕ} {O : Subring K} {α : K} (hℓ : Nat.Prime ℓ) (hℓ1 : σ ^ ℓ = 1) (hO : O = Subring.closure {α}) (hst : ∀ x ∈ O, σ x ∈ O) (hα : σ α ≠ α) {i j : ℕ} (hij : i % ℓ ≠ j % ℓ) : IsU O (((σ ^ i) α - (σ ^ j) α) / dd σ α 1)

lem:ratios, first assertion: (σⁱα − σʲα)/d₁ ∈ O^× for i ≢ j (mod ℓ).

theorem Louboutin.SeccionSeis.lem_ratios {K : Type u_1} [Field K] {σ : RingAut K} {ℓ : ℕ} {O : Subring K} {α : K} (hℓ : Nat.Prime ℓ) (hℓ2 : ℓ ≠ 2) (hℓ1 : σ ^ ℓ = 1) (hO : O = Subring.closure {α}) (hst : ∀ x ∈ O, σ x ∈ O) (hα : σ α ≠ α) : (∀ (i j : ℕ), i % ℓ ≠ j % ℓ → IsU O (((σ ^ i) α - (σ ^ j) α) / dd σ α 1)) ∧ IsU O (dd σ α 2 / dd σ α 1) ∧ dd σ α 2 / dd σ α 1 - 1 = σ (dd σ α 1) / dd σ α 1 ∧ IsU O (dd σ α 2 / dd σ α 1 - 1) ∧ nrm σ ℓ (dd σ α 2 / dd σ α 1 - 1) = 1 ∧ IsU O (1 - dd σ α 2 / dd σ α 1) ∧ nrm σ ℓ (1 - dd σ α 2 / dd σ α 1) = -1

lem:ratios (6.2). O = ℤ[α] σ-stable, σ of odd prime order ℓ on K, σα ≠ α. Then (σⁱα − σʲα)/d₁ ∈ O^× for i ≢ j (mod ℓ); η = d₂/d₁ and η − 1 = σ(d₁)/d₁ lie in O^×, N(η − 1) = 1, and η is exceptional: 1 − η ∈ O^× with N(1 − η) = −1.

theorem Louboutin.SeccionSeis.cor_inert_card {K : Type u_1} [Field K] {σ : RingAut K} {ℓ : ℕ} {O : Subring K} {α : K} (hℓ : Nat.Prime ℓ) (hℓ1 : σ ^ ℓ = 1) (hO : O = Subring.closure {α}) (hst : ∀ x ∈ O, σ x ∈ O) (hα : σ α ≠ α) {F : Type u_2} [Field F] [Fintype F] (φ : ↥O →+* F) : ℓ ≤ Fintype.card F

cor:inert (6.3), core: the r_i = d_i/d₁ (i < ℓ) lie in O and have unit differences, so their images under any ring hom O → F, F a finite field (the residue field of a prime above p), are distinct: ℓ ≤ |F|.

theorem Louboutin.SeccionSeis.cor_inert {K : Type u_1} [Field K] {σ : RingAut K} {ℓ : ℕ} {O : Subring K} {α : K} (hℓ : Nat.Prime ℓ) (hℓ1 : σ ^ ℓ = 1) (hO : O = Subring.closure {α}) (hst : ∀ x ∈ O, σ x ∈ O) (hα : σ α ≠ α) {F : Type u_2} [Field F] [Fintype F] (φ : ↥O →+* F) {p f : ℕ} (hcard : Fintype.card F = p ^ f) (hp : p < ℓ) (hf : f ∣ ℓ) : f = ℓ

cor:inert (6.3). If the residue field has pᶠ elements with p < ℓ and f ∣ ℓ (the residue degree divides [K : ℚ] = ℓ), then f = ℓ: p is inert.

Powers of α: prop:val and cor:q25

def Louboutin.SeccionSeis.Zconj {N : Type u_1} [CommRing N] (G : Type u_2) [Group G] [MulSemiringAction G N] (x : N) : Subring N

ℤ[conj x]: the subring generated by the G-orbit of x (G the Galois group of the normal closure, acting on its ring of integers N).

Equations

• Louboutin.SeccionSeis.Zconj G x = Subring.closure (Set.range fun (g : G) => g • x)

theorem Louboutin.SeccionSeis.le_val_closure {N : Type u_1} [CommRing N] {G : Type u_2} [Group G] [MulSemiringAction G N] (v : AddValuation N ℕ∞) {S : Set N} {m : ℕ∞} (hS : ∀ s ∈ S, ∀ (h : G), m ≤ v (s - h • s)) {x : N} (hx : x ∈ Subring.closure S) (h : G) : m ≤ v (x - h • x)

If m ≤ v(s − h·s) for every generator s and every h, the same holds on the whole subring generated (x − h·x lies in the ideal generated by those differences).

theorem Louboutin.SeccionSeis.val_pow_sub {N : Type u_1} [CommRing N] (v : AddValuation N ℕ∞) {a b : N} (ha : 1 ≤ v a) (hb : 1 ≤ v b) (k : ℕ) : v (a - b) + ↑(k - 1) ≤ v (a ^ k - b ^ k)

v(aᵏ − bᵏ) ≥ v(a − b) + (k − 1) when v(a), v(b) ≥ 1.

theorem Louboutin.SeccionSeis.prop_val {N : Type u_1} [CommRing N] {G : Type u_2} [Group G] [MulSemiringAction G N] (v : AddValuation N ℕ∞) (hsupp : ∀ (x : N), v x = ⊤ → x = 0) (α : N) (hpos : ∀ (g : G), 1 ≤ v (g • α)) (hnq : ∃ (g : G), g • α ≠ α) {k : ℕ} (hk : 2 ≤ k) : Zconj G (α ^ k) ≠ Zconj G α

prop:val (6.5), valuation core. v a valuation of N with trivial support (𝔓-adic on 𝒪_N), every conjugate of α has positive valuation, α is not G-fixed (α ∉ ℚ), k ≥ 2. Then ℤ[conj αᵏ] ≠ ℤ[conj α]: μ(ℤ[conj αᵏ]) ≥ μ(ℤ[conj α]) + (k − 1) > μ(ℤ[conj α]).

theorem Louboutin.SeccionSeis.prop_val_root {N : Type u_1} [CommRing N] {G : Type u_2} [Group G] [MulSemiringAction G N] (v : AddValuation N ℕ∞) (hsupp : ∀ (x : N), v x = ⊤ → x = 0) (α : N) {n p : ℕ} (hroot : ∃ (y : N), α ^ n = ↑p * y) (hp : 1 ≤ v ↑p) (hnq : ∃ (g : G), g • α ≠ α) {k : ℕ} (hk : 2 ≤ k) : Zconj G (α ^ k) ≠ Zconj G α

prop:val (6.5) with its hypothesis as in the note: αⁿ ∈ p·N (from Π_α ≡ Xⁿ mod p) and v(p) > 0 (𝔓 lies above p).

theorem Louboutin.SeccionSeis.pow_eq_p_mul {N : Type u_1} [CommRing N] (α : N) {P : Polynomial ℤ} (hm : P.Monic) {n p : ℕ} (hdeg : P.natDegree = n) (hroot : (Polynomial.aeval α) P = 0) (hdvd : ∀ i < n, ↑p ∣ P.coeff i) : ∃ (y : N), α ^ n = ↑p * y

Π_α ≡ Xⁿ (mod p) ⇒ αⁿ ∈ p·ℤ[α]: if Π ∈ ℤ[X] is monic of degree n with Π(α) = 0 and p divides every coefficient of degree < n, then αⁿ = p·y.

theorem Louboutin.SeccionSeis.prop_val_poly {N : Type u_1} [CommRing N] {G : Type u_2} [Group G] [MulSemiringAction G N] (v : AddValuation N ℕ∞) (hsupp : ∀ (x : N), v x = ⊤ → x = 0) (α : N) {P : Polynomial ℤ} (hm : P.Monic) {n p : ℕ} (hdeg : P.natDegree = n) (hroot : (Polynomial.aeval α) P = 0) (hdvd : ∀ i < n, ↑p ∣ P.coeff i) (hp : 1 ≤ v ↑p) (hnq : ∃ (g : G), g • α ≠ α) {k : ℕ} (hk : 2 ≤ k) : Zconj G (α ^ k) ≠ Zconj G α

prop:val (6.5), as stated: Π_α ≡ Xⁿ (mod p) (Π monic of degree n, p ∣ coeff_i for i < n), v(p) > 0, α ∉ ℚ, k ≥ 2 ⇒ ℤ[conj αᵏ] ≠ ℤ[conj α].

theorem Louboutin.SeccionSeis.cor_q25 {N : Type u_1} [CommRing N] {G : Type u_2} [Group G] [MulSemiringAction G N] (α : N) {C C' : ℤ} (hC : C = C' ^ 2 + C' + 7) (hα : α ^ 3 - ↑C * α + ↑C = 0) (hnq : ∃ (g : G), g • α ≠ α) (hval : ∀ (p : ℕ), Nat.Prime p → ↑p ∣ C → ∃ (v : AddValuation N ℕ∞), (∀ (x : N), v x = ⊤ → x = 0) ∧ 1 ≤ v ↑p) {k : ℕ} (hk : 1 ≤ k) : Zconj G (α ^ k) = Zconj G α ↔ k = 1

cor:q25 (6.6). α³ − Cα + C = 0 with C = C'² + C' + 7, α ∉ ℚ; for each prime p ∣ C a valuation v_p of N with trivial support and v_p(p) ≥ 1 (a prime of 𝒪_N above p). Then for k ≥ 1: ℤ[conj αᵏ] = ℤ[conj α] ↔ k = 1, i.e. S_α = {1}.

prop:c27 (Conjecture 27 of Lou20a): the algebraic core

theorem Louboutin.SeccionSeis.smul_mem_closure {N : Type u_1} [CommRing N] {G : Type u_2} [Group G] [MulSemiringAction G N] (ζ : N) (hζ : ∀ (g : G), g • ζ ∈ Subring.closure {ζ}) (g : G) {x : N} (hx : x ∈ Subring.closure {ζ}) : g • x ∈ Subring.closure {ζ}

theorem Louboutin.SeccionSeis.c27_core {N : Type u_1} [CommRing N] {G : Type u_2} [Group G] [Fintype G] [DecidableEq G] [MulSemiringAction G N] (ζ w ε : N) (c : G) {a : ℕ} (hζ5 : ζ ^ 5 = 1) (hcζ : c • ζ = ζ ^ 4) (hcw : c • w = w) (hε : ε = ζ ^ a * w) (ha : ¬5 ∣ a) (hN : ∏ g : G, g • ε = 1) (hζ : ∀ (g : G), g • ζ ∈ Subring.closure {ζ}) (hεZ : ε ∈ Subring.closure {ζ}) : Zconj G ε = Subring.closure {ζ}

prop:c27, core. G finite (Gal(ℚ(ζ₅)/ℚ)) acting on N, c ∈ G (complex conjugation), ζ⁵ = 1, c·ζ = ζ⁴ (= ζ̄), ε = ζᵃw with c·w = w (w = ±((1 − √5)/2)ᵇ is real), 5 ∤ a, N(ε) = ∏g g·ε = 1, G·ζ ⊆ ℤ[ζ] and ε ∈ ℤ[ζ]. Then ℤ[conj ε] = ℤ[ζ]: ε̄⁻¹ = ∏{g≠1} g·ε̄ ∈ A_ε, ε/ε̄ = ζ²ᵃ ∈ A_ε, and 5 ∤ 2a gives ζ ∈ A_ε.

theorem Louboutin.SeccionSeis.prop_c27 {N : Type u_1} [CommRing N] {G : Type u_2} [Group G] [Fintype G] [DecidableEq G] [MulSemiringAction G N] (ζ w ε : N) (c : G) {a : ℕ} (hζ5 : ζ ^ 5 = 1) (hcζ : c • ζ = ζ ^ 4) (hcw : c • w = w) (hε : ε = ζ ^ a * w) (ha : ¬5 ∣ a) (hN : ∏ g : G, g • ε = 1) (hζ : ∀ (g : G), g • ζ ∈ Subring.closure {ζ}) (hεZ : ε ∈ Subring.closure {ζ}) {k : ℕ} (hk : ¬5 ∣ k) : Zconj G (ε ^ k) = Subring.closure {ζ} ∧ Zconj G (ε ^ k) = Zconj G ε

prop:c27 (6.8) ([Lou20a, Conjecture 27]): ℤ[conj εᵏ] = ℤ[ζ] for every k with 5 ∤ k, and hence ℤ[conj εᵏ] = ℤ[conj ε].