The index and discriminant of ℤ[conj α] for Galois quartic integers

Model Louboutin.TeoremaB.QuartData O, one model for both Galois groups: O a commutative domain of characteristic 0, pairwise distinct conjugates x₀ = α, x₁ = τα, x₂ = β = ρα, x₃ = ρτα, ring endomorphisms τ, ρ with τ : x₀ ↔ x₁, x₂ ↔ x₃, ρ : x₀ ↦ x₂, x₁ ↦ x₃ and either ρ : x₂ ↦ x₀, x₃ ↦ x₁ (Γ ≅ C₂ × C₂) or ρ : x₂ ↦ x₁, x₃ ↦ x₀ (Γ ≅ C₄), and "fixed by τ and ρ ⇒ integer" on A = ℤ[x₀, …, x₃]. Bridges: ofC4, ofV4. The auxiliary data (η, n₁, n₂, s₀, s₁, …) form Lam M and exist (lam_nonempty); the data L, 𝖬 form Lam.LGH P and exist (exists_LGH).

Main results

• Louboutin.TeoremaB.Lam.lem_Lambda: Λ = ℤ[η] is an order of rank 2 with |disc Λ| = gcd(δ₁, δ₂, δ₃).
• Louboutin.TeoremaB.Lam.lem_B: bases {1, η, α, ηα} and {1, α, α², ω₀}; B = Λ[α]; [B : ℤ[α]] = |R'(z)| / |disc Λ|.
• Louboutin.TeoremaB.Lam.lem_AB: A = B + Bβ.
• Louboutin.TeoremaB.Lam.lem_lambda_a, lem_lambda_b: the V₄ and C₄ cases.
• Louboutin.TeoremaB.Lam.d1: A ∩ (ℚ + ℚα) = ℤ + ℤα (Louboutin's Theorem 13, proved here).
• Louboutin.TeoremaB.Lam.thm_B: [A : ℤ[α]] = J [A : B] and disc A · [A : ℤ[α]]² = D_α.
• Louboutin.TeoremaB.Lam.LGH.thm_B_LGH, Louboutin.TeoremaB.Lam.LGH.d2_form: [A : B] = L²/H, [A : ℤ[α]] = J L²/H, disc A = D_α (H/(J L²))², d₂ = LG/H.
• Louboutin.TeoremaB.hermite: the index lemma in ℤ² (Hermite form, e G = ±H).
• Louboutin.TeoremaB.Lam.LGH.thm_B_divisors: with the triangular basis as hypothesis, d₁ = 1, d₂ = LG/H, d₃ = JL/G, A/ℤ[α] ≅ ℤ/(LG/H) × ℤ/(JL/G).

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

structure Louboutin.TeoremaB.QuartData (O : Type u_1) [CommRing O] : Type u_1

The model for Section 4 of the note (both Galois groups).

• x : Fin 4 → O
• τ : O →+* O
• ρ : O →+* O
• hτ : self.τ (self.x 0) = self.x 1 ∧ self.τ (self.x 1) = self.x 0 ∧ self.τ (self.x 2) = self.x 3 ∧ self.τ (self.x 3) = self.x 2
• hρ : self.ρ (self.x 0) = self.x 2 ∧ self.ρ (self.x 1) = self.x 3
• hρ2 : self.ρ (self.x 2) = self.x 0 ∧ self.ρ (self.x 3) = self.x 1 ∨ self.ρ (self.x 2) = self.x 1 ∧ self.ρ (self.x 3) = self.x 0
• fix (y : O) : y ∈ Subring.closure (Set.range self.x) → self.τ y = y → self.ρ y = y → ∃ (n : ℤ), y = ↑n
• inj : Function.Injective self.x

def Louboutin.TeoremaB.QuartData.A {O : Type u_1} [CommRing O] (M : QuartData O) : Subring O

A = ℤ[x₀, x₁, x₂, x₃] = ℤ[conj(α)].

Equations

• M.A = Subring.closure (Set.range M.x)

theorem Louboutin.TeoremaB.QuartData.x_mem {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] (M : QuartData O) (k : Fin 4) : M.x k ∈ M.A

def Louboutin.TeoremaB.QuartData.S {O : Type u_1} [CommRing O] (M : QuartData O) : O

S = α + τα, Q = α·τα, and their ρ-images S' = ρS, Q' = ρQ.

Equations

• M.S = M.x 0 + M.x 1

def Louboutin.TeoremaB.QuartData.Q {O : Type u_1} [CommRing O] (M : QuartData O) : O

Equations

• M.Q = M.x 0 * M.x 1

def Louboutin.TeoremaB.QuartData.S' {O : Type u_1} [CommRing O] (M : QuartData O) : O

Equations

• M.S' = M.x 2 + M.x 3

def Louboutin.TeoremaB.QuartData.Q' {O : Type u_1} [CommRing O] (M : QuartData O) : O

Equations

• M.Q' = M.x 2 * M.x 3

theorem Louboutin.TeoremaB.QuartData.S_mem {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] (M : QuartData O) : M.S ∈ M.A

theorem Louboutin.TeoremaB.QuartData.Q_mem {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] (M : QuartData O) : M.Q ∈ M.A

theorem Louboutin.TeoremaB.QuartData.S'_mem {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] (M : QuartData O) : M.S' ∈ M.A

theorem Louboutin.TeoremaB.QuartData.Q'_mem {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] (M : QuartData O) : M.Q' ∈ M.A

theorem Louboutin.TeoremaB.QuartData.τS {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] (M : QuartData O) : M.τ M.S = M.S

theorem Louboutin.TeoremaB.QuartData.τQ {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] (M : QuartData O) : M.τ M.Q = M.Q

theorem Louboutin.TeoremaB.QuartData.τS' {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] (M : QuartData O) : M.τ M.S' = M.S'

theorem Louboutin.TeoremaB.QuartData.τQ' {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] (M : QuartData O) : M.τ M.Q' = M.Q'

theorem Louboutin.TeoremaB.QuartData.ρS {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] (M : QuartData O) : M.ρ M.S = M.S'

theorem Louboutin.TeoremaB.QuartData.ρQ {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] (M : QuartData O) : M.ρ M.Q = M.Q'

theorem Louboutin.TeoremaB.QuartData.ρS' {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] (M : QuartData O) : M.ρ M.S' = M.S

theorem Louboutin.TeoremaB.QuartData.ρQ' {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] (M : QuartData O) : M.ρ M.Q' = M.Q

theorem Louboutin.TeoremaB.QuartData.intOf {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] (M : QuartData O) {y : O} (hA : y ∈ M.A) (h1 : M.τ y = y) (h2 : M.ρ y = y) : ∃ (n : ℤ), y = ↑n

fixed by τ and ρ, in A ⇒ integer.

def Louboutin.TeoremaB.QuartData.eta {O : Type u_1} [CommRing O] (M : QuartData O) (m₁ m₂ : ℤ) : O

η = m₁S + m₂Q and η' = ρη = m₁S' + m₂Q'.

Equations

• M.eta m₁ m₂ = ↑m₁ * M.S + ↑m₂ * M.Q

def Louboutin.TeoremaB.QuartData.eta' {O : Type u_1} [CommRing O] (M : QuartData O) (m₁ m₂ : ℤ) : O

Equations

• M.eta' m₁ m₂ = ↑m₁ * M.S' + ↑m₂ * M.Q'

theorem Louboutin.TeoremaB.QuartData.eta_mem {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] (M : QuartData O) (m₁ m₂ : ℤ) : M.eta m₁ m₂ ∈ M.A

theorem Louboutin.TeoremaB.QuartData.eta'_mem {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] (M : QuartData O) (m₁ m₂ : ℤ) : M.eta' m₁ m₂ ∈ M.A

theorem Louboutin.TeoremaB.QuartData.τeta {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] (M : QuartData O) (m₁ m₂ : ℤ) : M.τ (M.eta m₁ m₂) = M.eta m₁ m₂

theorem Louboutin.TeoremaB.QuartData.τeta' {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] (M : QuartData O) (m₁ m₂ : ℤ) : M.τ (M.eta' m₁ m₂) = M.eta' m₁ m₂

theorem Louboutin.TeoremaB.QuartData.ρeta {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] (M : QuartData O) (m₁ m₂ : ℤ) : M.ρ (M.eta m₁ m₂) = M.eta' m₁ m₂

theorem Louboutin.TeoremaB.QuartData.ρeta' {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] (M : QuartData O) (m₁ m₂ : ℤ) : M.ρ (M.eta' m₁ m₂) = M.eta m₁ m₂

lem:Lambda: the data

structure Louboutin.TeoremaB.Lam {O : Type u_1} [CommRing O] (M : QuartData O) : Type

The integers of Section 4: a, b, c, d (Π_α = X⁴ − aX³ + bX² − cX + d), z = Q + ρQ, and the data of lem:Lambda: Λ = ℤ + ℤη with η = m₁S + m₂Q, S = s₀ + n₁η, Q = s₁ + n₂η, m₁n₁ + m₂n₂ = 1, η + ρη = t, η·ρη = ν and disc Λ = (η − ρη)² = D.

• a : ℤ
• b : ℤ
• c : ℤ
• d : ℤ
• z : ℤ
• ha : ↑self.a = M.x 0 + M.x 1 + M.x 2 + M.x 3
• hb : ↑self.b = M.x 0 * M.x 1 + M.x 0 * M.x 2 + M.x 0 * M.x 3 + M.x 1 * M.x 2 + M.x 1 * M.x 3 + M.x 2 * M.x 3
• hc : ↑self.c = M.x 0 * M.x 1 * M.x 2 + M.x 0 * M.x 1 * M.x 3 + M.x 0 * M.x 2 * M.x 3 + M.x 1 * M.x 2 * M.x 3
• hd : ↑self.d = M.x 0 * M.x 1 * M.x 2 * M.x 3
• hz : ↑self.z = M.Q + M.Q'
• n₁ : ℤ
• n₂ : ℤ
• m₁ : ℤ
• m₂ : ℤ
• s₀ : ℤ
• s₁ : ℤ
• t : ℤ
• ν : ℤ
• D : ℤ
• bez : self.m₁ * self.n₁ + self.m₂ * self.n₂ = 1
• hS : M.S = ↑self.s₀ + ↑self.n₁ * M.eta self.m₁ self.m₂
• hQ : M.Q = ↑self.s₁ + ↑self.n₂ * M.eta self.m₁ self.m₂
• ht : M.eta self.m₁ self.m₂ + M.eta' self.m₁ self.m₂ = ↑self.t
• hν : M.eta self.m₁ self.m₂ * M.eta' self.m₁ self.m₂ = ↑self.ν
• hD : (M.eta self.m₁ self.m₂ - M.eta' self.m₁ self.m₂) ^ 2 = ↑self.D

def Louboutin.TeoremaB.Lam.η {O : Type u_1} [CommRing O] {M : QuartData O} (P : Lam M) : O

η, ρη and θ = η − ρη.

Equations

• P.η = M.eta P.m₁ P.m₂

def Louboutin.TeoremaB.Lam.η' {O : Type u_1} [CommRing O] {M : QuartData O} (P : Lam M) : O

Equations

• P.η' = M.eta' P.m₁ P.m₂

def Louboutin.TeoremaB.Lam.θ {O : Type u_1} [CommRing O] {M : QuartData O} (P : Lam M) : O

Equations

• P.θ = P.η - P.η'

def Louboutin.TeoremaB.Lam.δ₁ {O : Type u_1} [CommRing O] {M : QuartData O} (P : Lam M) : ℤ

δ₁ = a² − 4b + 4z, δ₂ = az − 2c, δ₃ = z² − 4d.

Equations

• P.δ₁ = P.a ^ 2 - 4 * P.b + 4 * P.z

def Louboutin.TeoremaB.Lam.δ₂ {O : Type u_1} [CommRing O] {M : QuartData O} (P : Lam M) : ℤ

Equations

• P.δ₂ = P.a * P.z - 2 * P.c

def Louboutin.TeoremaB.Lam.δ₃ {O : Type u_1} [CommRing O] {M : QuartData O} (P : Lam M) : ℤ

Equations

• P.δ₃ = P.z ^ 2 - 4 * P.d

theorem Louboutin.TeoremaB.Lam.hS' {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : QuartData O} (P : Lam M) : M.S' = ↑P.s₀ + ↑P.n₁ * P.η'

theorem Louboutin.TeoremaB.Lam.hQ' {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : QuartData O} (P : Lam M) : M.Q' = ↑P.s₁ + ↑P.n₂ * P.η'

theorem Louboutin.TeoremaB.Lam.DS_eq {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : QuartData O} (P : Lam M) : M.S - M.S' = ↑P.n₁ * P.θ

theorem Louboutin.TeoremaB.Lam.DQ_eq {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : QuartData O} (P : Lam M) : M.Q - M.Q' = ↑P.n₂ * P.θ

theorem Louboutin.TeoremaB.Lam.θ_sq {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : QuartData O} (P : Lam M) : P.θ ^ 2 = ↑P.D

theorem Louboutin.TeoremaB.Lam.η_sq {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : QuartData O} (P : Lam M) : P.η ^ 2 = ↑P.t * P.η - ↑P.ν

theorem Louboutin.TeoremaB.Lam.ident {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : QuartData O} (P : Lam M) : (M.S - M.S') ^ 2 = ↑P.δ₁ ∧ (M.S - M.S') * (M.Q - M.Q') = ↑P.δ₂ ∧ (M.Q - M.Q') ^ 2 = ↑P.δ₃

lem:Lambda, the three identities (S − ρS)² = δ₁, (S − ρS)(Q − ρQ) = δ₂, (Q − ρQ)² = δ₃.

theorem Louboutin.TeoremaB.Lam.R_z {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : QuartData O} (P : Lam M) : P.z ^ 3 - P.b * P.z ^ 2 + (P.a * P.c - 4 * P.d) * P.z - (P.a ^ 2 * P.d - 4 * P.b * P.d + P.c ^ 2) = 0

z is a root of the cubic resolvent R(y) = y³ − by² + (ac − 4d)y − (a²d − 4bd + c²).

theorem Louboutin.TeoremaB.Lam.θ_ne {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : QuartData O} (P : Lam M) : P.θ ≠ 0

theorem Louboutin.TeoremaB.Lam.D_ne {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : QuartData O} (P : Lam M) : P.D ≠ 0

theorem Louboutin.TeoremaB.Lam.isCoprime {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : QuartData O} (P : Lam M) : IsCoprime P.n₁ P.n₂

theorem Louboutin.TeoremaB.Lam.δ_eq {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : QuartData O} (P : Lam M) : P.δ₁ = P.n₁ ^ 2 * P.D ∧ P.δ₂ = P.n₁ * P.n₂ * P.D ∧ P.δ₃ = P.n₂ ^ 2 * P.D

theorem Louboutin.TeoremaB.gcd3 (n₁ n₂ D : ℤ) (h : IsCoprime n₁ n₂) : ↑((n₁ ^ 2 * D).gcd ↑((n₁ * n₂ * D).gcd (n₂ ^ 2 * D))) = |D|

def Louboutin.TeoremaB.tacticAmem : Lean.ParserDescr

membership in A of polynomial expressions in the conjugates.

Equations

• Louboutin.TeoremaB.tacticAmem = Lean.ParserDescr.node `Louboutin.TeoremaB.tacticAmem 1024 (Lean.ParserDescr.nonReservedSymbol "amem" false)

theorem Louboutin.TeoremaB.QuartData.exists_lam {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] (M : QuartData O) : Nonempty (Lam M)

lem:Lambda, existence of the data: a primitive (n₁, n₂) with S − ρS = n₁θ, Q − ρQ = n₂θ. The pair is the note's: (δ₁, δ₂)/gcd(δ₁, δ₂) if δ₁ ≠ 0, (0, 1) if δ₁ = 0.

def Louboutin.TeoremaB.QuartData.Λ {O : Type u_1} [CommRing O] (M : QuartData O) : Submodule ℤ O

Λ = ℤ + ℤS + ℤQ.

Equations

• M.Λ = Submodule.span ℤ {1, M.S, M.Q}

theorem Louboutin.TeoremaB.Lam.hSη {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : QuartData O} (P : Lam M) : M.S = ↑P.s₀ + ↑P.n₁ * P.η

theorem Louboutin.TeoremaB.Lam.hQη {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : QuartData O} (P : Lam M) : M.Q = ↑P.s₁ + ↑P.n₂ * P.η

theorem Louboutin.TeoremaB.Lam.Λ_eq {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : QuartData O} (P : Lam M) : M.Λ = Submodule.span ℤ {1, P.η}

lem:Lambda: Λ = ℤ + ℤη.

theorem Louboutin.TeoremaB.Lam.mem_Λ {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : QuartData O} (P : Lam M) {y : O} : y ∈ M.Λ ↔ ∃ (p : ℤ) (q : ℤ), y = ↑p + ↑q * P.η

theorem Louboutin.TeoremaB.Lam.one_mem_Λ {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : QuartData O} (P : Lam M) : 1 ∈ M.Λ

theorem Louboutin.TeoremaB.Lam.S_mem_Λ {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : QuartData O} (P : Lam M) : M.S ∈ M.Λ

theorem Louboutin.TeoremaB.Lam.Q_mem_Λ {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : QuartData O} (P : Lam M) : M.Q ∈ M.Λ

theorem Louboutin.TeoremaB.Lam.η_mem_Λ {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : QuartData O} (P : Lam M) : P.η ∈ M.Λ

theorem Louboutin.TeoremaB.Lam.intCast_mem_Λ {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : QuartData O} (P : Lam M) (n : ℤ) : ↑n ∈ M.Λ

theorem Louboutin.TeoremaB.Lam.mul_mem_Λ {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : QuartData O} (P : Lam M) {y y' : O} (hy : y ∈ M.Λ) (hy' : y' ∈ M.Λ) : y * y' ∈ M.Λ

lem:Lambda: Λ is a ring (an order: ℤ[η] = ℤ + ℤη).

theorem Louboutin.TeoremaB.Lam.τ_Λ {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : QuartData O} (P : Lam M) {y : O} (hy : y ∈ M.Λ) : M.τ y = y

lem:Lambda: Λ ⊆ E = K^⟨τ⟩.

theorem Louboutin.TeoremaB.Lam.linIndep_Λ {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : QuartData O} (P : Lam M) : LinearIndependent ℤ ![1, P.η]

lem:Lambda: Λ has rank 2 (1, η are ℤ-independent).

Lattices in O: the determinant D (detG with γ = 1, τ, ρ, ρτ) and indices

@[reducible, inline]

abbrev Louboutin.TeoremaB.Lat4 {O : Type u_1} [CommRing O] (v : Fin 4 → O) : AddSubgroup O

The lattice spanned by a family.

Equations

• Louboutin.TeoremaB.Lat4 v = (Submodule.span ℤ (Set.range v)).toAddSubgroup

def Louboutin.TeoremaB.QuartData.γ {O : Type u_1} [CommRing O] (M : QuartData O) (i : Fin 4) : O →+* O

γ₀ = 1, γ₁ = τ, γ₂ = ρ, γ₃ = ρτ.

Equations

• M.γ i = ![RingHom.id O, M.τ, M.ρ, M.ρ.comp M.τ] i

theorem Louboutin.TeoremaB.QuartData.γ_x0 {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] (M : QuartData O) (i : Fin 4) : (M.γ i) (M.x 0) = M.x i

noncomputable def Louboutin.TeoremaB.QuartData.Dq {O : Type u_1} [CommRing O] (M : QuartData O) (w : Fin 4 → O) : O

D(ω) = det[γ_i(ω_l)].

Equations

• M.Dq w = (Matrix.of fun (i l : Fin 4) => (M.γ i) (w l)).det

theorem Louboutin.TeoremaB.QuartData.Dq_comb {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] (M : QuartData O) (v w : Fin 4 → O) (C : Matrix (Fin 4) (Fin 4) ℤ) (h : ∀ (l : Fin 4), w l = ∑ k : Fin 4, ↑(C l k) * v k) : M.Dq w = M.Dq v * ↑C.det

theorem Louboutin.TeoremaB.QuartData.linIndep_of_Dq {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] (M : QuartData O) {v : Fin 4 → O} (hv : M.Dq v ≠ 0) : LinearIndependent ℤ v

theorem Louboutin.TeoremaB.QuartData.relIndex_Dq {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] (M : QuartData O) {v w : Fin 4 → O} (hv : M.Dq v ≠ 0) (hw : M.Dq w ≠ 0) (hwv : ∀ (l : Fin 4), w l ∈ Submodule.span ℤ (Set.range v)) : ∃ (C : Matrix (Fin 4) (Fin 4) ℤ), M.Dq w = M.Dq v * ↑C.det ∧ (Lat4 w).relIndex (Lat4 v) = C.det.natAbs

[⟨v⟩ : ⟨w⟩] = |det C| where w = C v, and D(w) = D(v) det C.

def Louboutin.TeoremaB.QuartData.vpow {O : Type u_1} [CommRing O] (M : QuartData O) : Fin 4 → O

ℤ[α] = ℤ + ℤα + ℤα² + ℤα³.

Equations

• M.vpow = ![1, M.x 0, M.x 0 ^ 2, M.x 0 ^ 3]

theorem Louboutin.TeoremaB.QuartData.Dq_vpow {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] (M : QuartData O) : M.Dq M.vpow = Conj61.Vand M.x

theorem Louboutin.TeoremaB.QuartData.Vand_ne {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] (M : QuartData O) : Conj61.Vand M.x ≠ 0

lem:B

def Louboutin.TeoremaB.Lam.vB {O : Type u_1} [CommRing O] {M : QuartData O} (P : Lam M) : Fin 4 → O

{1, η, α, ηα}.

Equations

• P.vB = ![1, P.η, M.x 0, P.η * M.x 0]

def Louboutin.TeoremaB.Lam.ω₀ {O : Type u_1} [CommRing O] {M : QuartData O} (P : Lam M) : O

ω₀ = m₁η + m₂ηα.

Equations

• P.ω₀ = ↑P.m₁ * P.η + ↑P.m₂ * (P.η * M.x 0)

def Louboutin.TeoremaB.Lam.vW {O : Type u_1} [CommRing O] {M : QuartData O} (P : Lam M) : Fin 4 → O

{1, α, α², ω₀}.

Equations

• P.vW = ![1, M.x 0, M.x 0 ^ 2, P.ω₀]

def Louboutin.TeoremaB.Lam.B {O : Type u_1} [CommRing O] {M : QuartData O} (P : Lam M) : Submodule ℤ O

B = Λ[α] = ℤ + ℤη + ℤα + ℤηα.

Equations

• P.B = Submodule.span ℤ (Set.range P.vB)

def Louboutin.TeoremaB.Lam.J {O : Type u_1} [CommRing O] {M : QuartData O} (P : Lam M) : ℤ

J = n₂² − s₀n₁n₂ + s₁n₁², the index [B : ℤ[α]] up to sign.

Equations

• P.J = P.n₂ ^ 2 - P.s₀ * P.n₁ * P.n₂ + P.s₁ * P.n₁ ^ 2

def Louboutin.TeoremaB.Lam.R'z {O : Type u_1} [CommRing O] {M : QuartData O} (P : Lam M) : ℤ

R'(z) = 3z² − 2bz + (ac − 4d).

Equations

• P.R'z = 3 * P.z ^ 2 - 2 * P.b * P.z + (P.a * P.c - 4 * P.d)

theorem Louboutin.TeoremaB.Lam.α_sq {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : QuartData O} (P : Lam M) : M.x 0 ^ 2 = -↑P.s₁ - ↑P.n₂ * P.η + ↑P.s₀ * M.x 0 + ↑P.n₁ * (P.η * M.x 0)

theorem Louboutin.TeoremaB.Lam.α_cube {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : QuartData O} (P : Lam M) : M.x 0 ^ 3 = -↑(P.s₀ * P.s₁ - P.n₁ * P.n₂ * P.ν) - ↑(P.s₀ * P.n₂ + P.s₁ * P.n₁ + P.n₁ * P.n₂ * P.t) * P.η + ↑(P.s₀ ^ 2 - P.n₁ ^ 2 * P.ν - P.s₁) * M.x 0 + ↑(2 * P.s₀ * P.n₁ + P.n₁ ^ 2 * P.t - P.n₂) * (P.η * M.x 0)

theorem Louboutin.TeoremaB.Lam.J_mul_D {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : QuartData O} (P : Lam M) : P.J * P.D = P.R'z

The key identity: J·disc Λ = R'(z).

theorem Louboutin.TeoremaB.Lam.Dq_vB {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : QuartData O} (P : Lam M) : M.Dq P.vB = -P.θ ^ 2 * (M.x 0 - M.x 1) * (M.x 2 - M.x 3)

theorem Louboutin.TeoremaB.Lam.Dq_vB_ne {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : QuartData O} (P : Lam M) : M.Dq P.vB ≠ 0

theorem Louboutin.TeoremaB.Lam.Vand_eq {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : QuartData O} (P : Lam M) : Conj61.Vand M.x = M.Dq P.vB * -↑P.J

theorem Louboutin.TeoremaB.Lam.vpow_mem_B {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : QuartData O} (P : Lam M) (l : Fin 4) : M.vpow l ∈ P.B

theorem Louboutin.TeoremaB.Lam.relIndex_B {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : QuartData O} (P : Lam M) : (Lat4 M.vpow).relIndex (Lat4 P.vB) = P.J.natAbs

lem:B, the index: [B : ℤ[α]] = |J|.

theorem Louboutin.TeoremaB.Lam.J_natAbs {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : QuartData O} (P : Lam M) : P.J.natAbs = P.R'z.natAbs / P.D.natAbs

lem:B: J = |R'(z)|/|disc Λ|.

theorem Louboutin.TeoremaB.Lam.bezO {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : QuartData O} (P : Lam M) : ↑P.m₁ * ↑P.n₁ + ↑P.m₂ * ↑P.n₂ = 1

theorem Louboutin.TeoremaB.Lam.vW_comb {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : QuartData O} (P : Lam M) (l : Fin 4) : P.vW l = ∑ k : Fin 4, ↑(!![1, 0, 0, 0; 0, 0, 1, 0; -P.s₁, -P.n₂, P.s₀, P.n₁; 0, P.m₁, 0, P.m₂] l k) * P.vB k

the change of basis {1, η, α, ηα} → {1, α, α², ω₀} (determinant 1).

theorem Louboutin.TeoremaB.Lam.Dq_vW {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : QuartData O} (P : Lam M) : M.Dq P.vW = M.Dq P.vB

theorem Louboutin.TeoremaB.Lam.vB_mem_W {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : QuartData O} (P : Lam M) (l : Fin 4) : P.vB l ∈ Submodule.span ℤ (Set.range P.vW)

theorem Louboutin.TeoremaB.Lam.vW_mem_B {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : QuartData O} (P : Lam M) (l : Fin 4) : P.vW l ∈ P.B

theorem Louboutin.TeoremaB.Lam.B_eq_W {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : QuartData O} (P : Lam M) : P.B = Submodule.span ℤ (Set.range P.vW)

lem:B: {1, α, α², ω₀} spans B.

theorem Louboutin.TeoremaB.Lam.linIndep_vB {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : QuartData O} (P : Lam M) : LinearIndependent ℤ P.vB

lem:B: {1, η, α, ηα} and {1, α, α², ω₀} are ℤ-bases of B (independent families).

theorem Louboutin.TeoremaB.Lam.linIndep_vW {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : QuartData O} (P : Lam M) : LinearIndependent ℤ P.vW

theorem Louboutin.TeoremaB.Lam.mem_B {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : QuartData O} (P : Lam M) {y : O} : y ∈ P.B ↔ ∃ l₁ ∈ M.Λ, ∃ l₂ ∈ M.Λ, y = l₁ + l₂ * M.x 0

B = Λ + Λα.

theorem Louboutin.TeoremaB.Lam.Λ_le_B {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : QuartData O} (P : Lam M) {y : O} (hy : y ∈ M.Λ) : y ∈ P.B

theorem Louboutin.TeoremaB.Lam.α_mem_B {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : QuartData O} (P : Lam M) : M.x 0 ∈ P.B

theorem Louboutin.TeoremaB.Lam.mul_mem_B {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : QuartData O} (P : Lam M) {y y' : O} (hy : y ∈ P.B) (hy' : y' ∈ P.B) : y * y' ∈ P.B

lem:B: B is a ring (α² = Sα − Q with S, Q ∈ Λ).

theorem Louboutin.TeoremaB.Lam.B_le_subring {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : QuartData O} (P : Lam M) (R : Subring O) (hΛ : ∀ y ∈ M.Λ, y ∈ R) (hα : M.x 0 ∈ R) {y : O} (hy : y ∈ P.B) : y ∈ R

lem:B: B = Λ[α], the smallest subring containing Λ and α.

lem:AB

theorem Louboutin.TeoremaB.Lam.Λ_le_A {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : QuartData O} (P : Lam M) {y : O} (hy : y ∈ M.Λ) : y ∈ M.A

theorem Louboutin.TeoremaB.Lam.B_le_A {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : QuartData O} (P : Lam M) {y : O} (hy : y ∈ P.B) : y ∈ M.A

theorem Louboutin.TeoremaB.Lam.lem_AB {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : QuartData O} (P : Lam M) {y : O} : y ∈ M.A ↔ ∃ b₁ ∈ P.B, ∃ b₂ ∈ P.B, y = b₁ + b₂ * M.x 2

lem:AB: A = B + Bβ, β = ρ(α) = x₂.

lem:lambda

def Louboutin.TeoremaB.QuartData.u {O : Type u_1} [CommRing O] (M : QuartData O) : O

u = α − τα, v = ρ(u) = β − ρτα, N = a² − 2b − 2z, k = an₁ − 4n₂.

Equations

• M.u = M.x 0 - M.x 1

def Louboutin.TeoremaB.QuartData.v {O : Type u_1} [CommRing O] (M : QuartData O) : O

Equations

• M.v = M.x 2 - M.x 3

def Louboutin.TeoremaB.Lam.N {O : Type u_1} [CommRing O] {M : QuartData O} (P : Lam M) : ℤ

Equations

• P.N = P.a ^ 2 - 2 * P.b - 2 * P.z

def Louboutin.TeoremaB.Lam.k {O : Type u_1} [CommRing O] {M : QuartData O} (P : Lam M) : ℤ

Equations

• P.k = P.a * P.n₁ - 4 * P.n₂

theorem Louboutin.TeoremaB.Lam.u_ne {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : QuartData O} (P : Lam M) : M.u ≠ 0

theorem Louboutin.TeoremaB.Lam.v_ne {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : QuartData O} (P : Lam M) : M.v ≠ 0

theorem Louboutin.TeoremaB.Lam.uv_sum {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : QuartData O} (P : Lam M) : M.u ^ 2 + M.v ^ 2 = ↑P.N

theorem Louboutin.TeoremaB.Lam.uv_diff {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : QuartData O} (P : Lam M) : M.u ^ 2 - M.v ^ 2 = ↑P.k * P.θ

theorem Louboutin.TeoremaB.Lam.N_sub_kθ {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : QuartData O} (P : Lam M) : ↑P.N - ↑P.k * P.θ = 2 * M.v ^ 2

theorem Louboutin.TeoremaB.Lam.τ_uv {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : QuartData O} (P : Lam M) : M.τ M.u = -M.u ∧ M.τ M.v = -M.v

lem:lambda: τu = −u and τv = −v, so λ = v/u is τ-fixed (λ ∈ E).

theorem Louboutin.TeoremaB.Lam.β_eq {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : QuartData O} (P : Lam M) : 2 * M.u * M.x 2 = M.u * ↑P.a - M.S * (M.u + M.v) + 2 * M.v * M.x 0

lem:lambda: β = μ + λα with λ = v/u, μ = (a − S(1 + λ))/2, cleared of denominators: 2u·β = u·a − S(u + v) + 2v·α.

theorem Louboutin.TeoremaB.Lam.lem_lambda_a {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : QuartData O} (P : Lam M) (hV : M.ρ (M.x 2) = M.x 0 ∧ M.ρ (M.x 3) = M.x 1) : ∃ (κ : ℤ), ↑κ = M.u * M.v ∧ κ ≠ 0 ∧ ↑κ = M.x 0 * M.x 2 + M.x 1 * M.x 3 - (M.x 0 * M.x 3 + M.x 1 * M.x 2) ∧ 4 * κ ^ 2 = P.N ^ 2 - P.k ^ 2 * P.D ∧ 2 * ↑κ * M.v = M.u * (↑P.N - ↑P.k * P.θ) ∧ 4 * ↑κ * M.x 2 = 2 * ↑κ * ↑P.a - M.S * (2 * ↑κ + (↑P.N - ↑P.k * P.θ)) + 2 * (↑P.N - ↑P.k * P.θ) * M.x 0

lem:lambda (a), Γ ≅ C₂ × C₂: κ = uv is a nonzero integer, κ = z' − z'', 4κ² = N² − k² disc Λ, λ = (N − kθ)/(2κ) (as 2κv = u(N − kθ)) and 4κβ = 2κa − S(2κ + N − kθ) + 2(N − kθ)α.

theorem Louboutin.TeoremaB.Lam.lem_lambda_b {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : QuartData O} (P : Lam M) (hC : M.ρ (M.x 2) = M.x 1 ∧ M.ρ (M.x 3) = M.x 0) : M.ρ (M.u * M.v) = -(M.u * M.v) ∧ M.ρ P.θ = -P.θ ∧ ∃ (h : ℤ), ↑h = M.u * M.v * P.θ ∧ h ≠ 0 ∧ 4 * h ^ 2 = P.D * (P.N ^ 2 - P.k ^ 2 * P.D) ∧ 2 * ↑h * M.v = M.u * (↑P.N * P.θ - ↑P.k * ↑P.D) ∧ 4 * ↑h * M.x 2 = 2 * ↑h * ↑P.a - M.S * (2 * ↑h + (↑P.N * P.θ - ↑P.k * ↑P.D)) + 2 * (↑P.N * P.θ - ↑P.k * ↑P.D) * M.x 0

lem:lambda (b), Γ = ⟨σ⟩ ≅ C₄ (ρ = σ, τ = σ²): σ(uv) = −uv, σθ = −θ, h = uvθ is a nonzero integer, 4h² = disc Λ (N² − k² disc Λ), λ = (Nθ − k disc Λ)/(2h) (as 2hv = u(Nθ − k disc Λ)) and 4hβ = 2ha − S(2h + Nθ − k disc Λ) + 2(Nθ − k disc Λ)α.

thm:B, assembly: indices and the discriminant of A

theorem Louboutin.TeoremaB.Lam.θ_mem_Λ {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : QuartData O} (P : Lam M) : P.θ ∈ M.Λ

theorem Louboutin.TeoremaB.Lam.intCast_mem_B {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : QuartData O} (P : Lam M) (n : ℤ) : ↑n ∈ P.B

theorem Louboutin.TeoremaB.Lam.exists_Nβ {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : QuartData O} (P : Lam M) : ∃ (N : ℤ), N ≠ 0 ∧ ↑N * M.x 2 ∈ P.B

A nonzero integer N with N·β ∈ B (N = 4κ or 4h, lem:lambda).

theorem Louboutin.TeoremaB.Lam.exists_NA {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : QuartData O} (P : Lam M) : ∃ (N : ℤ), N ≠ 0 ∧ ∀ y ∈ M.A, ↑N * y ∈ P.B

N·A ⊆ B for some nonzero integer N.

theorem Louboutin.TeoremaB.Lam.Zα_le_B {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : QuartData O} (P : Lam M) : Lat4 M.vpow ≤ Lat4 P.vB

theorem Louboutin.TeoremaB.Lam.B_le_Aadd {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : QuartData O} (P : Lam M) : Lat4 P.vB ≤ M.A.toAddSubgroup

theorem Louboutin.TeoremaB.Lam.index_A {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : QuartData O} (P : Lam M) : (Lat4 M.vpow).relIndex M.A.toAddSubgroup = P.J.natAbs * (Lat4 P.vB).relIndex M.A.toAddSubgroup

thm:B: [A : ℤ[α]] = J·[A : B] (with [B : ℤ[α]] = J from lem:B).

def Louboutin.TeoremaB.Lam.Asub {O : Type u_1} [CommRing O] {M : QuartData O} : Submodule ℤ O

A as a ℤ-submodule of O.

Equations

• Louboutin.TeoremaB.Lam.Asub = AddSubgroup.toIntSubmodule M.A.toAddSubgroup

theorem Louboutin.TeoremaB.Lam.exists_basis_A {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : QuartData O} (P : Lam M) : ∃ (b : Fin 4 → O), ∀ (y : O), y ∈ Submodule.span ℤ (Set.range b) ↔ y ∈ M.A

A is free of rank 4: it has a family of four elements spanning it.

theorem Louboutin.TeoremaB.Lam.disc_A {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : QuartData O} (P : Lam M) (b : Fin 4 → O) (hb : ∀ (y : O), y ∈ Submodule.span ℤ (Set.range b) ↔ y ∈ M.A) : M.Dq b ≠ 0 ∧ (Lat4 M.vpow).relIndex M.A.toAddSubgroup ≠ 0 ∧ M.Dq b ^ 2 * ↑((Lat4 M.vpow).relIndex M.A.toAddSubgroup) ^ 2 = Conj61.Vand M.x ^ 2

thm:B, the discriminant: for every family b of four elements spanning A, D(b) ≠ 0 (so b is a ℤ-basis), [A : ℤ[α]] ≠ 0, and disc A · [A : ℤ[α]]² = D_α, with disc A = D(b)² and D_α = Vand(x)² = disc(1, α, α², α³).

Bridges from the existing models

def Louboutin.TeoremaB.QuartData.ofC4 {O : Type u_1} [CommRing O] (C : Identidades.C4Data O) (hinj : Function.Injective C.x) : QuartData O

From the C4 model of IdentidadesNota (α_k = σᵏα): x = (α, σ²α, σα, σ³α), τ = σ², ρ = σ.

Equations

• Louboutin.TeoremaB.QuartData.ofC4 C hinj = { x := ![C.x 0, C.x 2, C.x 1, C.x 3], τ := C.σ.comp C.σ, ρ := C.σ, hτ := ⋯, hρ := ⋯, hρ2 := ⋯, fix := ⋯, inj := ⋯ }

def Louboutin.TeoremaB.QuartData.ofV4 {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] (V : Conj61.V4Data O) : QuartData O

From the V4 model of Conj61Model (τ = τ₁, ρ = τ₂). On A = ℤ[x] the τ's compose as V₄ (DiscV4.comp_of_mem), so "fixed by τ₁, τ₂ ⇒ fixed by τ₃ ⇒ integer".

Equations

• Louboutin.TeoremaB.QuartData.ofV4 V = { x := V.x, τ := V.τ₁, ρ := V.τ₂, hτ := ⋯, hρ := ⋯, hρ2 := ⋯, fix := ⋯, inj := ⋯ }

The statements

theorem Louboutin.TeoremaB.Lam.lem_Lambda {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : QuartData O} (P : Lam M) : ((M.S - M.S') ^ 2 = ↑P.δ₁ ∧ (M.S - M.S') * (M.Q - M.Q') = ↑P.δ₂ ∧ (M.Q - M.Q') ^ 2 = ↑P.δ₃) ∧ M.Λ = Submodule.span ℤ {1, P.η} ∧ (∀ y ∈ M.Λ, ∀ y' ∈ M.Λ, y * y' ∈ M.Λ) ∧ LinearIndependent ℤ ![1, P.η] ∧ (∀ y ∈ M.Λ, M.τ y = y) ∧ M.S = ↑P.s₀ + ↑P.n₁ * P.η ∧ M.Q = ↑P.s₁ + ↑P.n₂ * P.η ∧ IsCoprime P.n₁ P.n₂ ∧ (P.η - M.ρ P.η) ^ 2 = ↑P.D ∧ (P.δ₁ = P.n₁ ^ 2 * P.D ∧ P.δ₂ = P.n₁ * P.n₂ * P.D ∧ P.δ₃ = P.n₂ ^ 2 * P.D) ∧ ↑(P.δ₁.gcd ↑(P.δ₂.gcd P.δ₃)) = |P.D|

lem:Lambda (4.1). (S − ρS)² = δ₁, (S − ρS)(Q − ρQ) = δ₂, (Q − ρQ)² = δ₃; Λ = ℤ + ℤS + ℤQ equals ℤ + ℤη = ℤ[η] (a ring, of rank 2, inside E = K^⟨τ⟩), S = s₀ + n₁η, Q = s₁ + n₂η with gcd(n₁, n₂) = 1, (δ₁, δ₂, δ₃) = (n₁², n₁n₂, n₂²)·disc Λ with disc Λ = (η − ρη)², and |disc Λ| = gcd(δ₁, δ₂, δ₃).

theorem Louboutin.TeoremaB.Lam.lem_B {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : QuartData O} (P : Lam M) : P.B = Submodule.span ℤ (Set.range P.vW) ∧ LinearIndependent ℤ P.vB ∧ LinearIndependent ℤ P.vW ∧ (∀ (y : O), y ∈ P.B ↔ ∃ l₁ ∈ M.Λ, ∃ l₂ ∈ M.Λ, y = l₁ + l₂ * M.x 0) ∧ (∀ y ∈ P.B, ∀ y' ∈ P.B, y * y' ∈ P.B) ∧ (∀ (R : Subring O), (∀ y ∈ M.Λ, y ∈ R) → M.x 0 ∈ R → ∀ y ∈ P.B, y ∈ R) ∧ P.J * P.D = P.R'z ∧ (Lat4 M.vpow).relIndex (Lat4 P.vB) = P.R'z.natAbs / P.D.natAbs

lem:B (4.2). B = Λ[α] = Λ + Λα has the ℤ-bases {1, η, α, ηα} and {1, α, α², ω₀}, it is the smallest subring containing Λ and α, and [B : ℤ[α]] = J = |R'(z)|/|disc Λ|.

theorem Louboutin.TeoremaB.Lam.thm_B {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : QuartData O} (P : Lam M) : (∀ y ∈ M.Λ, ∀ y' ∈ M.Λ, y * y' ∈ M.Λ) ∧ (∀ y ∈ M.Λ, M.τ y = y) ∧ ↑(P.δ₁.gcd ↑(P.δ₂.gcd P.δ₃)) = |P.D| ∧ (Lat4 M.vpow).relIndex (Lat4 P.vB) = P.R'z.natAbs / P.D.natAbs ∧ (∀ (y : O), y ∈ M.A ↔ ∃ b₁ ∈ P.B, ∃ b₂ ∈ P.B, y = b₁ + b₂ * M.x 2) ∧ (Lat4 M.vpow).relIndex M.A.toAddSubgroup = P.R'z.natAbs / P.D.natAbs * (Lat4 P.vB).relIndex M.A.toAddSubgroup ∧ (Lat4 P.vB).relIndex M.A.toAddSubgroup ≠ 0 ∧ (∃ (b : Fin 4 → O), ∀ (y : O), y ∈ Submodule.span ℤ (Set.range b) ↔ y ∈ M.A) ∧ ∀ (b : Fin 4 → O), (∀ (y : O), y ∈ Submodule.span ℤ (Set.range b) ↔ y ∈ M.A) → M.Dq b ^ 2 * ↑((Lat4 M.vpow).relIndex M.A.toAddSubgroup) ^ 2 = Conj61.Vand M.x ^ 2

thm:B (Theorem C of the note), the part that closes in the model: Λ is an order of E = K^⟨τ⟩ with |disc Λ| = gcd(a² − 4b + 4z, az − 2c, z² − 4d); B = Λ[α] has [B : ℤ[α]] = J = |R'(z)|/|disc Λ|; A = B + Bβ; [A : ℤ[α]] = J·[A : B] with [A : B] finite; A has a ℤ-basis of four elements, and for every such basis b, disc A = D(b)² satisfies disc A · [A : ℤ[α]]² = D_α.

theorem Louboutin.TeoremaB.lam_nonempty {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] (M : QuartData O) : Nonempty (Lam M)

The data of lem:Lambda exist in every model (in particular in ofC4 C and ofV4 V).

Lattices in ℤ²: index = gcd of the 2 × 2 minors (Hermite form of a rank-2 lattice)

def Louboutin.TeoremaB.minor2 (u v : Fin 2 → ℤ) : ℤ

the 2 × 2 minor det(u | v).

Equations

• Louboutin.TeoremaB.minor2 u v = u 0 * v 1 - u 1 * v 0

def Louboutin.TeoremaB.Lam2 {k : ℕ} (col : Fin k → Fin 2 → ℤ) : Submodule ℤ (Fin 2 → ℤ)

the lattice spanned by the columns.

Equations

• Louboutin.TeoremaB.Lam2 col = Submodule.span ℤ (Set.range col)

def Louboutin.TeoremaB.Hm {k : ℕ} (col : Fin k → Fin 2 → ℤ) : ℤ

gcd of all 2 × 2 minors of the columns.

Equations

• Louboutin.TeoremaB.Hm col = Finset.univ.gcd fun (p : Fin k × Fin k) => Louboutin.TeoremaB.minor2 (col p.1) (col p.2)

def Louboutin.TeoremaB.Gm {k : ℕ} (col : Fin k → Fin 2 → ℤ) : ℤ

gcd of the second coordinates.

Equations

• Louboutin.TeoremaB.Gm col = Finset.univ.gcd fun (i : Fin k) => col i 1

theorem Louboutin.TeoremaB.minor2_sum {k : ℕ} (col : Fin k → Fin 2 → ℤ) (a b : Fin k → ℤ) : minor2 (∑ i : Fin k, a i • col i) (∑ j : Fin k, b j • col j) = ∑ i : Fin k, ∑ j : Fin k, a i * b j * minor2 (col i) (col j)

theorem Louboutin.TeoremaB.Hm_dvd_minor2 {k : ℕ} (col : Fin k → Fin 2 → ℤ) {u v : Fin 2 → ℤ} (hu : u ∈ Lam2 col) (hv : v ∈ Lam2 col) : Hm col ∣ minor2 u v

theorem Louboutin.TeoremaB.Gm_dvd {k : ℕ} (col : Fin k → Fin 2 → ℤ) {v : Fin 2 → ℤ} (hv : v ∈ Lam2 col) : Gm col ∣ v 1

theorem Louboutin.TeoremaB.col_mem {k : ℕ} (col : Fin k → Fin 2 → ℤ) (i : Fin k) : col i ∈ Lam2 col

theorem Louboutin.TeoremaB.Gm_ne {k : ℕ} (col : Fin k → Fin 2 → ℤ) (hH : Hm col ≠ 0) : Gm col ≠ 0

theorem Louboutin.TeoremaB.Hm_nonneg {k : ℕ} (col : Fin k → Fin 2 → ℤ) : 0 ≤ Hm col

theorem Louboutin.TeoremaB.Gm_nonneg {k : ℕ} (col : Fin k → Fin 2 → ℤ) : 0 ≤ Gm col

theorem Louboutin.TeoremaB.hermite {k : ℕ} (col : Fin k → Fin 2 → ℤ) (hH : Hm col ≠ 0) : ∃ (e : ℤ) (x : ℤ), e ≠ 0 ∧ ![e, 0] ∈ Lam2 col ∧ ![x, Gm col] ∈ Lam2 col ∧ (∀ v ∈ Lam2 col, ∃ (a : ℤ) (b : ℤ), v = a • ![e, 0] + b • ![x, Gm col]) ∧ (e * Gm col).natAbs = (Hm col).natAbs

Hermite form: Λ = ℤ(e, 0) + ℤ(x, G) with G = gcd of the second coordinates and e·G = ±H (H = gcd of the 2 × 2 minors).

A ∩ V₁ = ℤ + ℤα (Lou20a Thm. 13, d₁ = 1), proved in the model

def Louboutin.TeoremaB.QuartData.D1 {O : Type u_1} [CommRing O] (M : QuartData O) : Prop

A ∩ (ℚ + ℚα) = ℤ + ℤα (Lou20a Thm. 13, d₁ = 1), in the form: m·y ∈ ℤ + ℤα with m ≠ 0 and y ∈ A ⇒ y ∈ ℤ + ℤα.

Equations

• M.D1 = ∀ y ∈ M.A, ∀ (m r s : ℤ), m ≠ 0 → ↑m * y = ↑r + ↑s * M.x 0 → ∃ (r' : ℤ) (s' : ℤ), y = ↑r' + ↑s' * M.x 0

theorem Louboutin.TeoremaB.QuartData.τ_x_mem {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] (M : QuartData O) (k : Fin 4) : M.τ (M.x k) ∈ M.A

theorem Louboutin.TeoremaB.QuartData.ρ_x_mem {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] (M : QuartData O) (k : Fin 4) : M.ρ (M.x k) ∈ M.A

theorem Louboutin.TeoremaB.QuartData.map_mem {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] (M : QuartData O) (f : O →+* O) (hf : ∀ (k : Fin 4), f (M.x k) ∈ M.A) {y : O} (hy : y ∈ M.A) : f y ∈ M.A

theorem Louboutin.TeoremaB.QuartData.γ_mem {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] (M : QuartData O) (i : Fin 4) {y : O} (hy : y ∈ M.A) : (M.γ i) y ∈ M.A

theorem Louboutin.TeoremaB.Lam.not_le_Zp {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : QuartData O} (P : Lam M) {p : ℕ} (hp : Nat.Prime p) : ¬∀ y ∈ M.A, ∃ (n : ℤ), ∃ w ∈ M.A, y = ↑n + ↑p * w

A ⊄ ℤ + pA for every prime p (A/pA ≅ 𝔽_p⁴): via a ℤ-basis b of A, b = K b with K ≡ rank one (mod p), so 1 = det K ≡ 0 (mod p).

theorem Louboutin.TeoremaB.Lam.d1 {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : QuartData O} (P : Lam M) : M.D1

A ∩ (ℚ + ℚα) = ℤ + ℤα (d₁ = 1), the argument in the proof of thm:B.

thm:B, second half: the integers L, G, H (Definition def:LGH)

structure Louboutin.TeoremaB.Lam.LGH {O : Type u_1} [CommRing O] {M : QuartData O} (P : Lam M) : Type

Definition def:LGH: L is a common denominator of the coordinates of β, αβ, ηβ, ηαβ in the basis {1, α, α², ω₀}: L·(β·vB_j) = Σ_i C_ji·vW_i with C integral. (The note takes the least one; the formulas hold for every common denominator.)

• L : ℤ
• hL : self.L ≠ 0
• C : Fin 4 → Fin 4 → ℤ
• hC (j : Fin 4) : ↑self.L * (M.x 2 * P.vB j) = ∑ i : Fin 4, ↑(self.C j i) * P.vW i

theorem Louboutin.TeoremaB.Lam.exists_LGH {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : QuartData O} (P : Lam M) : Nonempty P.LGH

such data exist.

def Louboutin.TeoremaB.Lam.LGH.col {O : Type u_1} [CommRing O] {M : QuartData O} {P : Lam M} (W : P.LGH) : Fin 6 → Fin 2 → ℤ

the six columns of (L·I₂ | 𝖬).

Equations

• W.col = ![![W.L, 0], ![0, W.L], ![W.C 0 2, W.C 0 3], ![W.C 1 2, W.C 1 3], ![W.C 2 2, W.C 2 3], ![W.C 3 2, W.C 3 3]]

def Louboutin.TeoremaB.Lam.LGH.G {O : Type u_1} [CommRing O] {M : QuartData O} {P : Lam M} (W : P.LGH) : ℤ

G = gcd(L, 𝖬₂₁, …, 𝖬₂₄).

Equations

• W.G = Louboutin.TeoremaB.Gm W.col

def Louboutin.TeoremaB.Lam.LGH.H {O : Type u_1} [CommRing O] {M : QuartData O} {P : Lam M} (W : P.LGH) : ℤ

H = gcd of the 2 × 2 minors of (L·I₂ | 𝖬).

Equations

• W.H = Louboutin.TeoremaB.Hm W.col

theorem Louboutin.TeoremaB.Lam.LGH.H_ne {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : QuartData O} {P : Lam M} (W : P.LGH) : W.H ≠ 0

theorem Louboutin.TeoremaB.Lam.LGH.lift {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : QuartData O} {P : Lam M} (W : P.LGH) {v : Fin 2 → ℤ} (hv : v ∈ Lam2 W.col) : ∃ y ∈ M.A, ∃ (r : ℤ) (s : ℤ), ↑W.L * y = ↑r + ↑s * M.x 0 + ↑(v 0) * M.x 0 ^ 2 + ↑(v 1) * P.ω₀

every vector of ⟨columns⟩ lifts to A.

theorem Louboutin.TeoremaB.Lam.LGH.coords {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : QuartData O} {P : Lam M} (W : P.LGH) {y : O} (hy : y ∈ M.A) : ∃ (r : ℤ) (s : ℤ), ∃ v ∈ Lam2 W.col, ↑W.L * y = ↑r + ↑s * M.x 0 + ↑(v 0) * M.x 0 ^ 2 + ↑(v 1) * P.ω₀

every element of A has (α², ω₀)-coordinates (times L) in ⟨columns⟩.

theorem Louboutin.TeoremaB.Lam.LGH.index_AB {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : QuartData O} {P : Lam M} (W : P.LGH) (hd1 : M.D1) : (Lat4 P.vB).relIndex M.A.toAddSubgroup * W.H.natAbs = (W.L ^ 2).natAbs

thm:B: [A : B] = L²/H, in the form [A : B]·H = L², given A ∩ (ℚ + ℚα) = ℤ + ℤα (D1).

theorem Louboutin.TeoremaB.Lam.LGH.thm_B_LGH {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : QuartData O} {P : Lam M} (W : P.LGH) : 0 < W.H ∧ (Lat4 P.vB).relIndex M.A.toAddSubgroup * W.H.natAbs = (W.L ^ 2).natAbs ∧ (Lat4 P.vB).relIndex M.A.toAddSubgroup = (W.L ^ 2).natAbs / W.H.natAbs ∧ (Lat4 M.vpow).relIndex M.A.toAddSubgroup * W.H.natAbs = P.J.natAbs * (W.L ^ 2).natAbs ∧ ∀ (b : Fin 4 → O), (∀ (y : O), y ∈ Submodule.span ℤ (Set.range b) ↔ y ∈ M.A) → M.Dq b ^ 2 * (↑P.J * ↑W.L ^ 2) ^ 2 = Conj61.Vand M.x ^ 2 * ↑W.H ^ 2

thm:B, the formulas in L, H: [A : B] = L²/H, [A : ℤ[α]] = JL²/H and disc A = D_α (H/(JL²))² (for every ℤ-basis b of A, disc A = D(b)²), in integral form.

theorem Louboutin.TeoremaB.Lam.LGH.d2_form {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : QuartData O} {P : Lam M} (W : P.LGH) : ∃ y₂ ∈ M.A, ∃ (a : ℤ), a.natAbs * W.H.natAbs = (W.L * W.G).natAbs ∧ (∃ (r : ℤ) (s : ℤ), M.x 0 ^ 2 = ↑r + ↑s * M.x 0 + ↑a * y₂) ∧ ∀ (y : O), (y ∈ M.A ∧ ∃ (m : ℤ) (c₀ : ℤ) (c₁ : ℤ) (c₂ : ℤ), m ≠ 0 ∧ ↑m * y = ↑c₀ + ↑c₁ * M.x 0 + ↑c₂ * M.x 0 ^ 2) ↔ ∃ (p : ℤ) (q : ℤ) (t : ℤ), y = ↑p + ↑q * M.x 0 + ↑t * y₂

thm:B, d₂ = LG/H in basis form: there is y₂ ∈ A with A ∩ V₂ = ℤ + ℤα + ℤy₂ and α² ≡ a·y₂ (mod ℤ + ℤα) with |a|·H = |LG|; hence L₂ = ℤ + ℤα + ℤα² = ℤ + ℤα + ℤ(a y₂) has index |a| = LG/H in A ∩ V₂ (V₂ = ℚ + ℚα + ℚα²).

theorem Louboutin.TeoremaB.Lam.thm_B_LGH_exists {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : QuartData O} (P : Lam M) : ∃ (W : P.LGH), 0 < W.H ∧ (Lat4 P.vB).relIndex M.A.toAddSubgroup = (W.L ^ 2).natAbs / W.H.natAbs ∧ (Lat4 M.vpow).relIndex M.A.toAddSubgroup * W.H.natAbs = P.J.natAbs * (W.L ^ 2).natAbs

such L-data exist, and with them thm:B holds in full (up to the elementary divisors).

Coordinates in the power basis (A → ℚ⁴) and the elementary divisors,

with prop:triang as hypothesis (`Triang`, as in `T1Completo` and `DiscV4`) 

theorem Louboutin.TeoremaB.Lam.linIndep_vpow {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : QuartData O} (P : Lam M) : LinearIndependent ℤ M.vpow

theorem Louboutin.TeoremaB.Lam.sum_const {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : QuartData O} (P : Lam M) (a : ℤ) (c : Fin 4 → ℤ) : ∑ k : Fin 4, ↑(a * c k) * M.vpow k = ↑a * ∑ k : Fin 4, ↑(c k) * M.vpow k

noncomputable def Louboutin.TeoremaB.Lam.cZ {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : QuartData O} (P : Lam M) (z : O) : Fin 4 → ℤ

integer coordinates in the power basis 1, α, α², α³ (0 outside ℤ[α]).

Equations

• P.cZ z = if h : z ∈ Submodule.span ℤ (Set.range M.vpow) then (Module.Basis.span ⋯).equivFun ⟨z, h⟩ else 0

theorem Louboutin.TeoremaB.Lam.cZ_spec {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : QuartData O} (P : Lam M) {z : O} (h : z ∈ Submodule.span ℤ (Set.range M.vpow)) : z = ∑ k : Fin 4, ↑(P.cZ z k) * M.vpow k

theorem Louboutin.TeoremaB.Lam.cZ_unique {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : QuartData O} (P : Lam M) {z : O} (c : Fin 4 → ℤ) (hc : z = ∑ k : Fin 4, ↑(c k) * M.vpow k) : P.cZ z = c

noncomputable def Louboutin.TeoremaB.Lam.I {O : Type u_1} [CommRing O] {M : QuartData O} (_P : Lam M) : ℕ

I = [A : ℤ[α]].

Equations

• _P.I = (Louboutin.TeoremaB.Lat4 M.vpow).relIndex M.A.toAddSubgroup

theorem Louboutin.TeoremaB.Lam.I_ne {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : QuartData O} (P : Lam M) : P.I ≠ 0

theorem Louboutin.TeoremaB.Lam.I_mem {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : QuartData O} (P : Lam M) (y : ↥M.A.toAddSubgroup) : ↑P.I * ↑y ∈ Submodule.span ℤ (Set.range M.vpow)

noncomputable def Louboutin.TeoremaB.Lam.φ {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : QuartData O} (P : Lam M) : ↥M.A.toAddSubgroup →+ Fin 4 → ℚ

φ : A → ℚ⁴, the coordinates in the basis 1, α, α², α³.

Equations

• P.φ = { toFun := fun (y : ↥M.A.toAddSubgroup) (k : Fin 4) => ↑(P.cZ (↑P.I * ↑y) k) / ↑P.I, map_zero' := ⋯, map_add' := ⋯ }

theorem Louboutin.TeoremaB.Lam.φ_spec {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : QuartData O} (P : Lam M) (y : ↥M.A.toAddSubgroup) {m : ℤ} (hm : m ≠ 0) (c : Fin 4 → ℤ) (h : ↑m * ↑y = ∑ k : Fin 4, ↑(c k) * M.vpow k) : P.φ y = fun (k : Fin 4) => ↑(c k) / ↑m

theorem Louboutin.TeoremaB.Lam.φ_injective {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : QuartData O} (P : Lam M) : Function.Injective ⇑P.φ

theorem Louboutin.TeoremaB.Lam.vsum_mem_A {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : QuartData O} (P : Lam M) (c : Fin 4 → ℤ) : ∑ k : Fin 4, ↑(c k) * M.vpow k ∈ M.A

theorem Louboutin.TeoremaB.Lam.φ_inv {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : QuartData O} (P : Lam M) (y : ↥M.A.toAddSubgroup) {m : ℤ} (hm : m ≠ 0) (c : Fin 4 → ℤ) (h : P.φ y = fun (k : Fin 4) => ↑(c k) / ↑m) : ↑m * ↑y = ∑ k : Fin 4, ↑(c k) * M.vpow k

inverse of φ_spec.

noncomputable def Louboutin.TeoremaB.Lam.MQ {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : QuartData O} (P : Lam M) : AddSubgroup (Fin 4 → ℚ)

φ(A) ⊆ ℚ⁴.

Equations

• P.MQ = P.φ.range

noncomputable def Louboutin.TeoremaB.Lam.φequiv {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : QuartData O} (P : Lam M) : ↥M.A.toAddSubgroup ≃+ ↥P.MQ

A ≃ φ(A).

Equations

• P.φequiv = AddMonoidHom.ofInjective ⋯

theorem Louboutin.TeoremaB.Lam.map_Zα {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : QuartData O} (P : Lam M) : AddSubgroup.map (↑P.φequiv) ((Lat4 M.vpow).addSubgroupOf M.A.toAddSubgroup) = Z4.addSubgroupOf P.MQ

noncomputable def Louboutin.TeoremaB.Lam.quotEquiv {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : QuartData O} (P : Lam M) : ↥M.A.toAddSubgroup ⧸ (Lat4 M.vpow).addSubgroupOf M.A.toAddSubgroup ≃+ ↥P.MQ ⧸ Z4.addSubgroupOf P.MQ

A/ℤ[α] ≃ φ(A)/ℤ⁴.

Equations

• P.quotEquiv = QuotientAddGroup.congr ((Louboutin.TeoremaB.Lat4 M.vpow).addSubgroupOf M.A.toAddSubgroup) (Louboutin.Z4.addSubgroupOf P.MQ) P.φequiv ⋯

theorem Louboutin.TeoremaB.Lam.index_Z4 {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : QuartData O} (P : Lam M) : (Z4.addSubgroupOf P.MQ).index = P.I

theorem Louboutin.TeoremaB.Lam.φ_mem {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : QuartData O} (P : Lam M) (y : ↥M.A.toAddSubgroup) : P.φ y ∈ P.MQ

theorem Louboutin.TeoremaB.Lam.triang_d1 {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : QuartData O} (P : Lam M) (T : Triang P.MQ) : T.d₁ = 1

prop:triang (hypothesis) forces d₁ = 1 (via d1).

theorem Louboutin.TeoremaB.Lam.LGH.triang_d2 {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : QuartData O} {P : Lam M} (W : P.LGH) (T : Triang P.MQ) : T.d₂ * W.H.natAbs = (W.L * W.G).natAbs

d₂ = LG/H, with prop:triang as hypothesis.

theorem Louboutin.TeoremaB.Lam.LGH.thm_B_divisors {O : Type u_1} [CommRing O] [IsDomain O] [CharZero O] {M : QuartData O} {P : Lam M} (W : P.LGH) (T : Triang P.MQ) : T.d₁ = 1 ∧ T.d₂ = (W.L * W.G).natAbs / W.H.natAbs ∧ T.d₃ = (P.J * W.L).natAbs / W.G.natAbs ∧ Nonempty (↥M.A.toAddSubgroup ⧸ (Lat4 M.vpow).addSubgroupOf M.A.toAddSubgroup ≃+ ZMod ((W.L * W.G).natAbs / W.H.natAbs) × ZMod ((P.J * W.L).natAbs / W.G.natAbs))

thm:B, elementary divisors (prop:triang as hypothesis): d₁ = 1, d₂ = LG/H, d₃ = JL/G and A/ℤ[α] ≅ ℤ/(LG/H) × ℤ/(JL/G).