Saturation of ℤ + ℤα + ℤα² and cyclicity of M/ℤ[α]

Model: a quartic field K = ℚ(α) is identified with ℚ⁴ through the basis 1, α, α², α³, so ℤ[α] is ℤ⁴ (Louboutin.Z4), and for x ∈ V₂ = ℚ + ℚα + ℚα² multiplication by α is Louboutin.shift. An order M ⊇ ℤ[α] is an additive subgroup containing ℤ⁴, closed under shift on V₂, of finite index over ℤ[α]. Neither d₁ = 1 nor the Galois structure is used.

Main results

• Louboutin.saturated_iff_cyclic: L = ℤ + ℤα + ℤα² is saturated in M (M ∩ V₂ ⊆ ℤ⁴) iff M/ℤ[α] is cyclic.

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).

def Louboutin.Z4 : AddSubgroup (Fin 4 → ℚ)

ℤ⁴ inside ℚ⁴ (= ℤ[α] in the power basis).

Equations

• Louboutin.Z4 = { carrier := {x : Fin 4 → ℚ | ∀ (i : Fin 4), ∃ (n : ℤ), ↑n = x i}, add_mem' := @Louboutin.Z4._proof_1, zero_mem' := Louboutin.Z4._proof_4, neg_mem' := @Louboutin.Z4._proof_3 }

theorem Louboutin.mem_Z4 {x : Fin 4 → ℚ} : x ∈ Z4 ↔ ∀ (i : Fin 4), ∃ (n : ℤ), ↑n = x i

def Louboutin.shift (x : Fin 4 → ℚ) : Fin 4 → ℚ

Multiplication by α on V₂ = {x | x 3 = 0}.

Equations

• Louboutin.shift x = ![0, x 0, x 1, x 2]

def Louboutin.Saturated (M : AddSubgroup (Fin 4 → ℚ)) : Prop

L = ℤ + ℤα + ℤα² is saturated in M: M ∩ V₂ ⊆ ℤ⁴.

Equations

• Louboutin.Saturated M = ∀ x ∈ M, x 3 = 0 → x ∈ Louboutin.Z4

theorem Louboutin.not_cyclic_of_indep {G : Type u_1} [AddCommGroup G] [Fintype G] [IsAddCyclic G] {p : ℕ} (hp : Nat.Prime p) {a b : G} (ha : p • a = 0) (hb : p • b = 0) (hind : ∀ (e f : ℤ), e • a + f • b = 0 → ↑p ∣ e ∧ ↑p ∣ f) : False

A finite cyclic group does not contain two independent elements of p-torsion.

theorem Louboutin.dvd_of_intCast_eq_div {p : ℕ} (hp : Nat.Prime p) {k n : ℤ} (h : ↑n = ↑k / ↑p) : ↑p ∣ k

theorem Louboutin.indep {p : ℕ} (hp : Nat.Prime p) {γ : Fin 4 → ℚ} (h3 : γ 3 = 0) (hpγ : p • γ ∈ Z4) (hγ : γ ∉ Z4) (e f : ℤ) (hef : e • γ + f • shift γ ∈ Z4) : ↑p ∣ e ∧ ↑p ∣ f

If γ ∈ V₂, pγ ∈ ℤ⁴ and γ ∉ ℤ⁴, then γ and αγ are independent modulo ℤ⁴ (and modulo p).

theorem Louboutin.e3_mem : Pi.single 3 1 ∈ Z4

e₃ = α³ ∈ ℤ⁴.

theorem Louboutin.cyclic_of_saturated (M : AddSubgroup (Fin 4 → ℚ)) (hZ : Z4 ≤ M) [hfi : (Z4.addSubgroupOf M).FiniteIndex] (hsat : Saturated M) : IsAddCyclic (↥M ⧸ Z4.addSubgroupOf M)

(ii) ⇒ (iv): saturated ⇒ M/ℤ[α] cyclic (it embeds in ZMod N, N the index).

theorem Louboutin.saturated_of_cyclic (M : AddSubgroup (Fin 4 → ℚ)) (hsh : ∀ x ∈ M, x 3 = 0 → shift x ∈ M) [(Z4.addSubgroupOf M).FiniteIndex] (hcyc : IsAddCyclic (↥M ⧸ Z4.addSubgroupOf M)) : Saturated M

(iv) ⇒ (ii): M/ℤ[α] cyclic ⇒ saturated. Uses closure under α on V₂.

theorem Louboutin.saturated_iff_cyclic (M : AddSubgroup (Fin 4 → ℚ)) (hZ : Z4 ≤ M) (hsh : ∀ x ∈ M, x 3 = 0 → shift x ∈ M) [(Z4.addSubgroupOf M).FiniteIndex] : Saturated M ↔ IsAddCyclic (↥M ⧸ Z4.addSubgroupOf M)

(ii) ⇔ (iv) for every order M ⊇ ℤ[α] of rank 4.