Determinant and discriminant lemmas for quartic orders (biquadratic and cyclic)

Biquadratic case, in the model V4Data O with the determinant D of Discriminant:

• D(ω) ∈ ℤ when the γ's compose as V₄ on every ω_l (true on all of 𝒪_K), and unconditionally for ω ∈ A = ℤ[x₀, …, x₃];
• det[γ_i(∑_k m_lk αᵏ)] = Vand(γ_i α) · det(m) with det(m) ∈ R, for any subring R of elements fixed by the γ_i. Cyclic case, in a new model C4Act / C4Data (x_k = σᵏα, σ a ring endomorphism shifting the conjugates cyclically, and "σ-fixed ⇒ integer"):
• N, Q₂, U, Y, r ∈ ℤ with Q₂ = a² − 4b + 4r, N = a² − 2b − 2r, U = a³ − 4ab + 8c, U² + Y² = N² Q₂, and in every ring S ⊇ ι (ι² = −1) fed by a ring hom O → S: R₁R₃ = N, R₂² = Q₂, R₁²R₂ = U + ιY;
• two discriminant identities, in field form and in integral form.

Main results

• Louboutin.Identidades.lem_detZ, Louboutin.Identidades.lem_detZ_A.
• Louboutin.Identidades.lem_sub_core, Louboutin.Identidades.lem_sub_Z.
• Louboutin.Identidades.lem_inv.
• Louboutin.Identidades.lem_disc2, lem_disc2_b_ne, lem_disc2_b_zero, and the integral forms disc2_a, disc2_b, disc2_b0.

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

lem:detZ

theorem Louboutin.Identidades.D_fixed {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] (M : Conj61.V4Data O) (w : Fin 4 → O) (hw : ∀ (l : Fin 4), w l ∈ DiscV4.compSub M) (a : Fin 4) : (M.ρ a) (DiscV4.D M w) = DiscV4.D M w

γ_a fixes D(ω) when the γ's compose as V4 on the ω_l (row permutation xtPerm a, even).

theorem Louboutin.Identidades.lem_detZ {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] (M : Conj61.V4Data O) (w : Fin 4 → O) (hw : ∀ (l : Fin 4), w l ∈ DiscV4.compSub M) : ∃ (n : ℤ), DiscV4.D M w = ↑n

lem:detZ (Lou20b (5.2), Thm. 5.1). If the γ's act on ω₁, …, ω₄ as the group V4 (γ_aγ_i = γ_{a xor i}; for 𝒪_K this holds for every ω), then detG(ω) ∈ ℤ.

theorem Louboutin.Identidades.lem_detZ_A {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] (M : Conj61.V4Data O) (w : Fin 4 → O) (hw : ∀ (l : Fin 4), w l ∈ DiscV4.Aring M) : ∃ (n : ℤ), DiscV4.D M w = ↑n

lem:detZ in the model, unconditionally, for ω₁, …, ω₄ ∈ A = ℤ[x₀, …, x₃].

lem:sub

theorem Louboutin.Identidades.lem_sub_core {K : Type u_1} [CommRing K] (γ : Fin 4 → K →+* K) (α : K) (R : Subring K) (hR : ∀ (i : Fin 4), ∀ r ∈ R, (γ i) r = r) (m : Matrix (Fin 4) (Fin 4) K) (hm : ∀ (l k : Fin 4), m l k ∈ R) : (Matrix.of fun (i l : Fin 4) => (γ i) (∑ k : Fin 4, m l k * α ^ ↑k)).det = (Conj61.Vand fun (i : Fin 4) => (γ i) α) * m.det ∧ m.det ∈ R

lem:sub, algebraic core. γ₀, …, γ₃ ring endomorphisms of K, R a subring whose elements are fixed by every γ_i (R = ℤ or ℤ_(p) inside a number field), ω_l = Σ_k m_lk α^k with m_lk ∈ R. Then det[γ_i(ω_l)] = Vand(γ₀α, …, γ₃α)·det(m) and det(m) ∈ R.

theorem Louboutin.Identidades.lem_sub_Z {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] (M : Conj61.V4Data O) (m : Matrix (Fin 4) (Fin 4) ℤ) (w : Fin 4 → O) (hw : ∀ (l : Fin 4), w l = ∑ k : Fin 4, ↑(m l k) * M.x 0 ^ ↑k) : DiscV4.D M w = Conj61.Vand M.x * ↑m.det ∧ ∃ (n : ℤ), DiscV4.D M w = Conj61.Vand M.x * ↑n

lem:sub for R = ℤ, in the model: ω_l = Σ_k m_lk α^k with m_lk ∈ ℤ ⇒ detG(ω) = Δ_α·det(m) ∈ Δ_α ℤ.

The cyclic model and the polynomials of §5

structure Louboutin.Identidades.C4Act (O : Type u_1) [CommRing O] : Type u_1

C4 action: conjugates x₀ = α, x_k = σᵏα, σ a ring endomorphism shifting them cyclically.

• x : Fin 4 → O
• σ : O →+* O
• hσ : self.σ (self.x 0) = self.x 1 ∧ self.σ (self.x 1) = self.x 2 ∧ self.σ (self.x 2) = self.x 3 ∧ self.σ (self.x 3) = self.x 0

structure Louboutin.Identidades.C4Data (O : Type u_1) [CommRing O] extends Louboutin.Identidades.C4Act O : Type u_1

C4 model: C4 action plus "σ-fixed ⇒ integer" (𝓞_K^Γ = ℤ).

• x : Fin 4 → O
• σ : O →+* O
• hσ : self.σ (self.x 0) = self.x 1 ∧ self.σ (self.x 1) = self.x 2 ∧ self.σ (self.x 2) = self.x 3 ∧ self.σ (self.x 3) = self.x 0
• fix (y : O) : self.σ y = y → ∃ (n : ℤ), y = ↑n

def Louboutin.Identidades.rr {R : Type u_1} [CommRing R] (x : Fin 4 → R) : R

r = α₀α₂ + α₁α₃ (the rational root of the resolvent).

Equations

• Louboutin.Identidades.rr x = x 0 * x 2 + x 1 * x 3

def Louboutin.Identidades.R2 {R : Type u_1} [CommRing R] (x : Fin 4 → R) : R

R₂ = α₀ + α₂ − α₁ − α₃.

Equations

• Louboutin.Identidades.R2 x = x 0 - x 1 + x 2 - x 3

def Louboutin.Identidades.Nn {R : Type u_1} [CommRing R] (x : Fin 4 → R) : R

N = u² + v², u = α₀ − α₂, v = α₁ − α₃.

Equations

• Louboutin.Identidades.Nn x = (x 0 - x 2) ^ 2 + (x 1 - x 3) ^ 2

def Louboutin.Identidades.Q2 {R : Type u_1} [CommRing R] (x : Fin 4 → R) : R

Q₂ = R₂².

Equations

• Louboutin.Identidades.Q2 x = Louboutin.Identidades.R2 x ^ 2

def Louboutin.Identidades.Yy {R : Type u_1} [CommRing R] (x : Fin 4 → R) : R

Y = Im Ξ = 2uv(s − t).

Equations

• Louboutin.Identidades.Yy x = 2 * (x 0 - x 2) * (x 1 - x 3) * Louboutin.Identidades.R2 x

def Louboutin.Identidades.Rj {R : Type u_1} [CommRing R] (x : Fin 4 → R) (ι : R) (j : ℕ) : R

R_j = Σ_k ι^{jk} α_k.

Equations

• Louboutin.Identidades.Rj x ι j = ∑ k : Fin 4, ι ^ (j * ↑k) * x k

theorem Louboutin.Identidades.Rj_one {R : Type u_1} [CommRing R] (x : Fin 4 → R) (ι : R) : Rj x ι 1 = x 0 + ι * x 1 + ι ^ 2 * x 2 + ι ^ 3 * x 3

theorem Louboutin.Identidades.Rj_two {R : Type u_1} [CommRing R] (x : Fin 4 → R) (ι : R) : Rj x ι 2 = x 0 + ι ^ 2 * x 1 + ι ^ 4 * x 2 + ι ^ 6 * x 3

theorem Louboutin.Identidades.Rj_three {R : Type u_1} [CommRing R] (x : Fin 4 → R) (ι : R) : Rj x ι 3 = x 0 + ι ^ 3 * x 1 + ι ^ 6 * x 2 + ι ^ 9 * x 3

theorem Louboutin.Identidades.Rj_zero {R : Type u_1} [CommRing R] (x : Fin 4 → R) (ι : R) : Rj x ι 0 = Conj61.ea x

theorem Louboutin.Identidades.inv_poly {R : Type u_1} [CommRing R] (x : Fin 4 → R) : Q2 x = Conj61.ea x ^ 2 - 4 * Conj61.eb x + 4 * rr x ∧ Nn x = Conj61.ea x ^ 2 - 2 * Conj61.eb x - 2 * rr x ∧ Conj61.U x = Conj61.ea x ^ 3 - 4 * Conj61.ea x * Conj61.eb x + 8 * Conj61.ec x ∧ Conj61.U x ^ 2 + Yy x ^ 2 = Nn x ^ 2 * Q2 x ∧ Conj61.U x = R2 x * (Conj61.ea x * R2 x - 4 * (x 0 * x 2 - x 1 * x 3))

lem:inv, the polynomial identities (exact expansion).

theorem Louboutin.Identidades.inv_iota {R : Type u_1} [CommRing R] (x : Fin 4 → R) (ι : R) (hι : ι ^ 2 = -1) : Rj x ι 1 * Rj x ι 3 = Nn x ∧ Rj x ι 2 = R2 x ∧ Rj x ι 2 ^ 2 = Q2 x ∧ Rj x ι 1 ^ 2 * Rj x ι 2 = Conj61.U x + ι * Yy x

lem:inv, the identities with i: R₁R₃ = N, R₂ = α₀ + α₂ − α₁ − α₃, R₂² = Q₂, Ξ = R₁²R₂ = U + iY.

theorem Louboutin.Identidades.map_Nn {R : Type u_1} [CommRing R] (x : Fin 4 → R) {S : Type u_2} [CommRing S] (f : R →+* S) : Nn (⇑f ∘ x) = f (Nn x)

theorem Louboutin.Identidades.map_Q2 {R : Type u_1} [CommRing R] (x : Fin 4 → R) {S : Type u_2} [CommRing S] (f : R →+* S) : Q2 (⇑f ∘ x) = f (Q2 x)

theorem Louboutin.Identidades.map_U {R : Type u_1} [CommRing R] (x : Fin 4 → R) {S : Type u_2} [CommRing S] (f : R →+* S) : Conj61.U (⇑f ∘ x) = f (Conj61.U x)

theorem Louboutin.Identidades.map_Yy {R : Type u_1} [CommRing R] (x : Fin 4 → R) {S : Type u_2} [CommRing S] (f : R →+* S) : Yy (⇑f ∘ x) = f (Yy x)

lem:inv

theorem Louboutin.Identidades.C4Data.int_of_fix {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] (M : C4Data O) {y : O} (h : M.σ y = y) : ∃ (n : ℤ), y = ↑n

theorem Louboutin.Identidades.lem_inv {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] (M : C4Data O) : ∃ (a : ℤ) (b : ℤ) (c : ℤ) (r : ℤ) (n : ℤ) (q : ℤ) (u : ℤ) (y : ℤ), Conj61.ea M.x = ↑a ∧ Conj61.eb M.x = ↑b ∧ Conj61.ec M.x = ↑c ∧ rr M.x = ↑r ∧ Nn M.x = ↑n ∧ Q2 M.x = ↑q ∧ Conj61.U M.x = ↑u ∧ Yy M.x = ↑y ∧ q = a ^ 2 - 4 * b + 4 * r ∧ n = a ^ 2 - 2 * b - 2 * r ∧ u = a ^ 3 - 4 * a * b + 8 * c ∧ u ^ 2 + y ^ 2 = n ^ 2 * q ∧ Conj61.U M.x = R2 M.x * (Conj61.ea M.x * R2 M.x - 4 * (M.x 0 * M.x 2 - M.x 1 * M.x 3)) ∧ ∀ {S : Type u_2} [inst : CommRing S] (f : O →+* S) (ι : S), ι ^ 2 = -1 → Rj (⇑f ∘ M.x) ι 1 * Rj (⇑f ∘ M.x) ι 3 = ↑n ∧ Rj (⇑f ∘ M.x) ι 2 = f (R2 M.x) ∧ Rj (⇑f ∘ M.x) ι 2 ^ 2 = ↑q ∧ Rj (⇑f ∘ M.x) ι 1 ^ 2 * Rj (⇑f ∘ M.x) ι 2 = ↑u + ι * ↑y

lem:inv. With a, b, c, r the integers e₁, e₂, e₃(α) and α₀α₂ + α₁α₃: N, Q₂, U, Y are integers with Q₂ = a² − 4b + 4r, N = a² − 2b − 2r, U = a³ − 4ab + 8c, U² + Y² = N²Q₂; and in any commutative ring S with ι² = −1 receiving O by a ring hom f (e.g. K ⊗ ℚ(i)), with R_j = Σ_k ι^{jk} f(α_k): R₁R₃ = N, R₂² = Q₂, Ξ = R₁²R₂ = U + ιY, and U = R₂(aR₂ − 4(α₀α₂ − α₁α₃)) with R₂ = α₀ + α₂ − α₁ − α₃.

lem:disc2

def Louboutin.Identidades.C4Act.ρ {O : Type u_1} [CommRing O] (M : C4Act O) (m : Fin 4) : O →+* O

σ⁰, σ¹, σ², σ³.

Equations

• M.ρ m = ![RingHom.id O, M.σ, M.σ.comp M.σ, M.σ.comp (M.σ.comp M.σ)] m

noncomputable def Louboutin.Identidades.C4Act.disc {O : Type u_1} [CommRing O] (M : C4Act O) (w : Fin 4 → O) : O

disc(ω) = det[σᵐ(ω_l)]².

Equations

• M.disc w = (Matrix.of fun (m l : Fin 4) => (M.ρ m) (w l)).det ^ 2

def Louboutin.Identidades.C4Act.w1 {O : Type u_1} [CommRing O] (M : C4Act O) : Fin 4 → O

(1, α, σα, σ²α).

Equations

• M.w1 = ![1, M.x 0, M.σ (M.x 0), M.σ (M.σ (M.x 0))]

def Louboutin.Identidades.C4Act.w2 {O : Type u_1} [CommRing O] (M : C4Act O) : Fin 4 → O

(1, α, σα, α·σα).

Equations

• M.w2 = ![1, M.x 0, M.σ (M.x 0), M.x 0 * M.σ (M.x 0)]

theorem Louboutin.Identidades.det_w1 {O : Type u_1} [CommRing O] (M : C4Act O) : (Matrix.of fun (m l : Fin 4) => (M.ρ m) (M.w1 l)).det = R2 M.x * Nn M.x

theorem Louboutin.Identidades.det_w2 {O : Type u_1} [CommRing O] (M : C4Act O) : (Matrix.of fun (m l : Fin 4) => (M.ρ m) (M.w2 l)).det = (M.x 0 - M.x 2) * (M.x 1 - M.x 3) * (Conj61.eb M.x - 3 * rr M.x)

theorem Louboutin.Identidades.disc2_a {O : Type u_1} [CommRing O] (M : C4Act O) : M.disc M.w1 = Nn M.x ^ 2 * Q2 M.x

lem:disc2, first formula: disc(1, α, σα, σ²α) = N²Q₂ (any commutative ring).

theorem Louboutin.Identidades.disc2_b {O : Type u_1} [CommRing O] (M : C4Act O) : 16 * Q2 M.x * M.disc M.w2 = Yy M.x ^ 2 * (Nn M.x - Q2 M.x) ^ 2

lem:disc2, second formula, integral form: 16Q₂·disc(1, α, σα, α·σα) = Y²(N − Q₂)².

theorem Louboutin.Identidades.disc2_b0 {O : Type u_1} [CommRing O] (M : C4Act O) [IsDomain O] (hQ : Q2 M.x = 0) : 64 * M.disc M.w2 = Nn M.x ^ 2 * ∏ k : Fin 4, (Conj61.ea M.x - 4 * M.x k)

lem:disc2, second formula, case Q₂ = 0, integral form (O a domain): 64·disc(1, α, σα, α·σα) = N²·∏_k(a − 4α_k), i.e. disc = 4N²Π_α(a/4).

def Louboutin.Identidades.Pi {O : Type u_1} [CommRing O] (x : Fin 4 → O) (X : O) : O

Π_α(X) = ∏_k (X − α_k).

Equations

• Louboutin.Identidades.Pi x X = ∏ k : Fin 4, (X - x k)

theorem Louboutin.Identidades.lem_disc2_b_ne {K : Type u_2} [Field K] [CharZero K] (M : C4Act K) (hQ : Q2 M.x ≠ 0) : M.disc M.w2 = Yy M.x ^ 2 * (Nn M.x - Q2 M.x) ^ 2 / (16 * Q2 M.x)

lem:disc2, second formula, Q₂ ≠ 0 (K a field of characteristic 0): disc(1, α, σα, α·σα) = Y²(N − Q₂)²/(16Q₂).

theorem Louboutin.Identidades.lem_disc2_b_zero {K : Type u_2} [Field K] [CharZero K] (M : C4Act K) (hQ : Q2 M.x = 0) : M.disc M.w2 = 4 * Nn M.x ^ 2 * Pi M.x (Conj61.ea M.x / 4)

lem:disc2, second formula, Q₂ = 0 (K a field of characteristic 0): disc(1, α, σα, α·σα) = 4N²Π_α(a/4).

theorem Louboutin.Identidades.lem_disc2 {K : Type u_2} [Field K] [CharZero K] (M : C4Act K) : M.disc M.w1 = Nn M.x ^ 2 * Q2 M.x ∧ M.disc M.w2 = if Q2 M.x ≠ 0 then Yy M.x ^ 2 * (Nn M.x - Q2 M.x) ^ 2 / (16 * Q2 M.x) else 4 * Nn M.x ^ 2 * Pi M.x (Conj61.ea M.x / 4)

lem:disc2 (statement of the note, K a field of characteristic 0).