The quotient A/ℤ[α] of a quartic order with a triangular basis

In the model of Saturation (K = ℚ(α) as ℚ⁴, ℤ[α] = ℤ⁴), an order M is given with a triangular ℤ-basis 1, ω₁, ω₂, ω₃, ω_k = (αᵏ + P_k(α))/d_k, P_k ∈ ℤ[X] of degree < k, 0 < d₁ ∣ d₂ ∣ d₃ (the structure Louboutin.Triang; the existence of such a basis is cited from Louboutin 2020, Prop. 10, and Cohen 1993, Cor. 4.7.6, and enters as data). That it is a basis, that ℤ[α] ⊆ M, and the flags M ∩ V_k = ℤ + ℤω₁ + … + ℤω_k are proved. For M = A the hypothesis d₁ = 1 is Louboutin's Theorem 13. Triang.ofData realizes every datum, so the hypotheses are not contradictory.

Main results

• Louboutin.Triang.quotient_equiv: M/ℤ[α] ≃+ ℤ/d₁ × ℤ/d₂ × ℤ/d₃.
• Louboutin.Triang.quotient_equiv_T1, Louboutin.Triang.index_V2: with d₁ = 1, A/ℤ[α] ≃+ ℤ/d₂ × ℤ/d₃ and [A ∩ V₂ : L₂] = d₂.
• Louboutin.Triang.T1_i_iff_ii, T1_ii_iff_iii, T1_iii_iff_iv, T1_iii_iff_v, Louboutin.Triang.prop_T1: the five equivalent conditions.
• Louboutin.Triang.T1_mod_p: p ∣ d₂ iff 1, α, α² are dependent over 𝔽_p in A/pA.

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

@[reducible, inline]

abbrev Louboutin.apow (i : Fin 4) : Fin 4 → ℚ

apow i = αⁱ in the power basis.

Equations

• Louboutin.apow i = Pi.single i 1

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

V₂ = ℚ + ℚα + ℚα².

Equations

• Louboutin.V2 = { carrier := {x : Fin 4 → ℚ | x 3 = 0}, add_mem' := @Louboutin.V2._proof_1, zero_mem' := Louboutin.V2._proof_4, neg_mem' := @Louboutin.V2._proof_2 }

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

L₂ = ℤ + ℤα + ℤα² = ℤ[α] ∩ V₂.

Equations

• Louboutin.L2 = Louboutin.Z4 ⊓ Louboutin.V2

def Louboutin.omega1 (d : ℕ) (a : ℤ) : Fin 4 → ℚ

ω₁ = (α + a)/d.

Equations

• Louboutin.omega1 d a = ![↑a / ↑d, 1 / ↑d, 0, 0]

def Louboutin.omega2 (d : ℕ) (a b : ℤ) : Fin 4 → ℚ

ω₂ = (α² + bα + a)/d.

Equations

• Louboutin.omega2 d a b = ![↑a / ↑d, ↑b / ↑d, 1 / ↑d, 0]

def Louboutin.omega3 (d : ℕ) (a b c : ℤ) : Fin 4 → ℚ

ω₃ = (α³ + cα² + bα + a)/d.

Equations

• Louboutin.omega3 d a b c = ![↑a / ↑d, ↑b / ↑d, ↑c / ↑d, 1 / ↑d]

def Louboutin.combOf (ω₁ ω₂ ω₃ : Fin 4 → ℚ) (n : Fin 4 → ℤ) : Fin 4 → ℚ

n₀ + n₁ω₁ + n₂ω₂ + n₃ω₃.

Equations

• Louboutin.combOf ω₁ ω₂ ω₃ n = n 0 • Louboutin.apow 0 + n 1 • ω₁ + n 2 • ω₂ + n 3 • ω₃

structure Louboutin.Triang (M : AddSubgroup (Fin 4 → ℚ)) : Type

The triangular basis of the order M (cited, taken as data): 1, ω₁, ω₂, ω₃ with ω_k = (αᵏ + P_k(α))/d_k, P_k ∈ ℤ[X], deg P_k < k, and d₁ ∣ d₂ ∣ d₃.

• d₁ : ℕ
• d₂ : ℕ
• d₃ : ℕ
• d₁_pos : 0 < self.d₁
• d₂_pos : 0 < self.d₂
• d₃_pos : 0 < self.d₃
• d₁_dvd : self.d₁ ∣ self.d₂
• d₂_dvd : self.d₂ ∣ self.d₃
• p₁₀ : ℤ
• p₂₀ : ℤ
• p₂₁ : ℤ
• p₃₀ : ℤ
• p₃₁ : ℤ
• p₃₂ : ℤ
• one_mem : apow 0 ∈ M
• ω₁_mem : omega1 self.d₁ self.p₁₀ ∈ M
• ω₂_mem : omega2 self.d₂ self.p₂₀ self.p₂₁ ∈ M
• ω₃_mem : omega3 self.d₃ self.p₃₀ self.p₃₁ self.p₃₂ ∈ M
• span (x : Fin 4 → ℚ) : x ∈ M → ∃ (n : Fin 4 → ℤ), x = combOf (omega1 self.d₁ self.p₁₀) (omega2 self.d₂ self.p₂₀ self.p₂₁) (omega3 self.d₃ self.p₃₀ self.p₃₁ self.p₃₂) n

def Louboutin.Triang.ω₁ {M : AddSubgroup (Fin 4 → ℚ)} (B : Triang M) : Fin 4 → ℚ

ω₁ of the triangular basis.

Equations

• B.ω₁ = Louboutin.omega1 B.d₁ B.p₁₀

def Louboutin.Triang.ω₂ {M : AddSubgroup (Fin 4 → ℚ)} (B : Triang M) : Fin 4 → ℚ

ω₂ of the triangular basis.

Equations

• B.ω₂ = Louboutin.omega2 B.d₂ B.p₂₀ B.p₂₁

def Louboutin.Triang.ω₃ {M : AddSubgroup (Fin 4 → ℚ)} (B : Triang M) : Fin 4 → ℚ

ω₃ of the triangular basis.

Equations

• B.ω₃ = Louboutin.omega3 B.d₃ B.p₃₀ B.p₃₁ B.p₃₂

def Louboutin.Triang.comb {M : AddSubgroup (Fin 4 → ℚ)} (B : Triang M) (n : Fin 4 → ℤ) : Fin 4 → ℚ

Coordinates in the basis 1, ω₁, ω₂, ω₃.

Equations

• B.comb n = Louboutin.combOf B.ω₁ B.ω₂ B.ω₃ n

theorem Louboutin.Triang.d₁_q {M : AddSubgroup (Fin 4 → ℚ)} (B : Triang M) : ↑B.d₁ ≠ 0

theorem Louboutin.Triang.d₂_q {M : AddSubgroup (Fin 4 → ℚ)} (B : Triang M) : ↑B.d₂ ≠ 0

theorem Louboutin.Triang.d₃_q {M : AddSubgroup (Fin 4 → ℚ)} (B : Triang M) : ↑B.d₃ ≠ 0

theorem Louboutin.Triang.comb_apply_zero {M : AddSubgroup (Fin 4 → ℚ)} (B : Triang M) (n : Fin 4 → ℤ) : B.comb n 0 = ↑(n 0) + ↑(n 1) * ↑B.p₁₀ / ↑B.d₁ + ↑(n 2) * ↑B.p₂₀ / ↑B.d₂ + ↑(n 3) * ↑B.p₃₀ / ↑B.d₃

theorem Louboutin.Triang.comb_apply_one {M : AddSubgroup (Fin 4 → ℚ)} (B : Triang M) (n : Fin 4 → ℤ) : B.comb n 1 = ↑(n 1) / ↑B.d₁ + ↑(n 2) * ↑B.p₂₁ / ↑B.d₂ + ↑(n 3) * ↑B.p₃₁ / ↑B.d₃

theorem Louboutin.Triang.comb_apply_two {M : AddSubgroup (Fin 4 → ℚ)} (B : Triang M) (n : Fin 4 → ℤ) : B.comb n 2 = ↑(n 2) / ↑B.d₂ + ↑(n 3) * ↑B.p₃₂ / ↑B.d₃

theorem Louboutin.Triang.comb_apply_three {M : AddSubgroup (Fin 4 → ℚ)} (B : Triang M) (n : Fin 4 → ℤ) : B.comb n 3 = ↑(n 3) / ↑B.d₃

theorem Louboutin.Triang.dvd_of_cast_eq {d : ℕ} (hd : 0 < d) {n k q : ℤ} (h : ↑k = ↑n / ↑d + ↑q) : ↑d ∣ n

Auxiliary: if k = n/d + q with k, q integers, then d ∣ n.

theorem Louboutin.Triang.comb_mem_Z4_iff {M : AddSubgroup (Fin 4 → ℚ)} (B : Triang M) (n : Fin 4 → ℤ) : B.comb n ∈ Z4 ↔ ↑B.d₁ ∣ n 1 ∧ ↑B.d₂ ∣ n 2 ∧ ↑B.d₃ ∣ n 3

Key lemma: n₀ + n₁ω₁ + n₂ω₂ + n₃ω₃ ∈ ℤ[α] ↔ d₁ ∣ n₁, d₂ ∣ n₂, d₃ ∣ n₃.

theorem Louboutin.Triang.comb_add {M : AddSubgroup (Fin 4 → ℚ)} (B : Triang M) (n m : Fin 4 → ℤ) : B.comb (n + m) = B.comb n + B.comb m

theorem Louboutin.Triang.comb_zero {M : AddSubgroup (Fin 4 → ℚ)} (B : Triang M) : B.comb 0 = 0

theorem Louboutin.Triang.comb_mem {M : AddSubgroup (Fin 4 → ℚ)} (B : Triang M) (n : Fin 4 → ℤ) : B.comb n ∈ M

def Louboutin.Triang.combHom {M : AddSubgroup (Fin 4 → ℚ)} (B : Triang M) : (Fin 4 → ℤ) →+ ↥M

comb as a homomorphism ℤ⁴ → M.

Equations

• B.combHom = { toFun := fun (n : Fin 4 → ℤ) => ⟨B.comb n, ⋯⟩, map_zero' := ⋯, map_add' := ⋯ }

theorem Louboutin.Triang.combHom_surjective {M : AddSubgroup (Fin 4 → ℚ)} (B : Triang M) : Function.Surjective ⇑B.combHom

theorem Louboutin.Triang.comb_injective {M : AddSubgroup (Fin 4 → ℚ)} (B : Triang M) : Function.Injective B.comb

1, ω₁, ω₂, ω₃ are linearly independent: a ℤ-basis of M.

theorem Louboutin.Triang.inter_V2 {M : AddSubgroup (Fin 4 → ℚ)} (B : Triang M) {x : Fin 4 → ℚ} (hx : x ∈ M) (h3 : x 3 = 0) : ∃ (n : Fin 4 → ℤ), n 3 = 0 ∧ x = B.comb n

Flags, k = 2: M ∩ V₂ = ℤ + ℤω₁ + ℤω₂.

theorem Louboutin.Triang.inter_V1 {M : AddSubgroup (Fin 4 → ℚ)} (B : Triang M) {x : Fin 4 → ℚ} (hx : x ∈ M) (h3 : x 3 = 0) (h2 : x 2 = 0) : ∃ (n : Fin 4 → ℤ), n 3 = 0 ∧ n 2 = 0 ∧ x = B.comb n

Flags, k = 1: M ∩ V₁ = ℤ + ℤω₁.

theorem Louboutin.Triang.Z4_le {M : AddSubgroup (Fin 4 → ℚ)} (B : Triang M) : Z4 ≤ M

ℤ[α] ⊆ M.

theorem Louboutin.Triang.comb_zsmul {M : AddSubgroup (Fin 4 → ℚ)} (B : Triang M) (k : ℤ) (n : Fin 4 → ℤ) : B.comb (k • n) = k • B.comb n

theorem Louboutin.Triang.comb_nsmul {M : AddSubgroup (Fin 4 → ℚ)} (B : Triang M) (k : ℕ) (n : Fin 4 → ℤ) : B.comb (k • n) = k • B.comb n

theorem Louboutin.Triang.d₂_smul_mem {M : AddSubgroup (Fin 4 → ℚ)} (B : Triang M) {x : Fin 4 → ℚ} (hx : x ∈ M) (h3 : x 3 = 0) : ↑B.d₂ • x ∈ Z4

(M ∩ V₂)/L₂ is killed by d₂: x ∈ M, x ∈ V₂ ⇒ d₂ x ∈ ℤ[α].

The quotient A/ℤ[α]

noncomputable def Louboutin.quotEquivOf {P : Type u_1} {G : Type u_2} {Q : Type u_3} [AddCommGroup P] [AddCommGroup G] [AddCommGroup Q] (H : AddSubgroup G) (f : P →+ G) (hf : Function.Surjective ⇑f) (g : P →+ Q) (hg : Function.Surjective ⇑g) (hker : ∀ (n : P), f n ∈ H ↔ g n = 0) : G ⧸ H ≃+ Q

Auxiliary: G ⧸ H ≃+ Q if f : P ↠ G, g : P ↠ Q and f n ∈ H ↔ g n = 0.

Equations

• One or more equations did not get rendered due to their size.

def Louboutin.red3 (a b c : ℕ) : (Fin 4 → ℤ) →+ ZMod a × ZMod b × ZMod c

n ↦ (n₁ mod a, n₂ mod b, n₃ mod c).

Equations

• Louboutin.red3 a b c = { toFun := fun (n : Fin 4 → ℤ) => (↑(n 1), ↑(n 2), ↑(n 3)), map_zero' := ⋯, map_add' := ⋯ }

theorem Louboutin.red3_surjective {a b c : ℕ} (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) : Function.Surjective ⇑(red3 a b c)

theorem Louboutin.red3_eq_zero_iff (a b c : ℕ) (n : Fin 4 → ℤ) : (red3 a b c) n = 0 ↔ ↑a ∣ n 1 ∧ ↑b ∣ n 2 ∧ ↑c ∣ n 3

def Louboutin.red2 (a b : ℕ) : (Fin 4 → ℤ) →+ ZMod a × ZMod b

n ↦ (n₁ mod a, n₂ mod b).

Equations

• Louboutin.red2 a b = { toFun := fun (n : Fin 4 → ℤ) => (↑(n 1), ↑(n 2)), map_zero' := ⋯, map_add' := ⋯ }

theorem Louboutin.red2_surjective {a b : ℕ} (ha : 0 < a) (hb : 0 < b) : Function.Surjective ⇑(red2 a b)

theorem Louboutin.red2_eq_zero_iff (a b : ℕ) (n : Fin 4 → ℤ) : (red2 a b) n = 0 ↔ ↑a ∣ n 1 ∧ ↑b ∣ n 2

noncomputable def Louboutin.Triang.quotient_equiv {M : AddSubgroup (Fin 4 → ℚ)} (B : Triang M) : ↥M ⧸ Z4.addSubgroupOf M ≃+ ZMod B.d₁ × ZMod B.d₂ × ZMod B.d₃

M/ℤ[α] ≅ ℤ/d₁ × ℤ/d₂ × ℤ/d₃.

Equations

• B.quotient_equiv = Louboutin.quotEquivOf (Louboutin.Z4.addSubgroupOf M) B.combHom ⋯ (Louboutin.red3 B.d₁ B.d₂ B.d₃) ⋯ ⋯

theorem Louboutin.Triang.quotient_equiv_T1 {M : AddSubgroup (Fin 4 → ℚ)} (B : Triang M) (h1 : B.d₁ = 1) : Nonempty (↥M ⧸ Z4.addSubgroupOf M ≃+ ZMod B.d₂ × ZMod B.d₃)

With d₁ = 1, A/ℤ[α] ≅ ℤ/d₂ × ℤ/d₃.

theorem Louboutin.Triang.index_eq {M : AddSubgroup (Fin 4 → ℚ)} (B : Triang M) : (Z4.addSubgroupOf M).index = B.d₁ * B.d₂ * B.d₃

[A : ℤ[α]] = d₁ d₂ d₃.

[A ∩ V₂ : L₂] = d₂

def Louboutin.Triang.combHom2 {M : AddSubgroup (Fin 4 → ℚ)} (B : Triang M) : (Fin 4 → ℤ) →+ ↥(M ⊓ V2)

n ↦ n₀ + n₁ω₁ + n₂ω₂ ∈ M ∩ V₂ (n₃ is ignored).

Equations

• B.combHom2 = { toFun := fun (n : Fin 4 → ℤ) => ⟨B.comb ![n 0, n 1, n 2, 0], ⋯⟩, map_zero' := ⋯, map_add' := ⋯ }

theorem Louboutin.Triang.combHom2_surjective {M : AddSubgroup (Fin 4 → ℚ)} (B : Triang M) : Function.Surjective ⇑B.combHom2

noncomputable def Louboutin.Triang.quotient_equiv_V2 {M : AddSubgroup (Fin 4 → ℚ)} (B : Triang M) : ↥(M ⊓ V2) ⧸ L2.addSubgroupOf (M ⊓ V2) ≃+ ZMod B.d₁ × ZMod B.d₂

(M ∩ V₂)/L₂ ≅ ℤ/d₁ × ℤ/d₂.

Equations

• B.quotient_equiv_V2 = Louboutin.quotEquivOf (Louboutin.L2.addSubgroupOf (M ⊓ Louboutin.V2)) B.combHom2 ⋯ (Louboutin.red2 B.d₁ B.d₂) ⋯ ⋯

theorem Louboutin.Triang.index_V2_eq {M : AddSubgroup (Fin 4 → ℚ)} (B : Triang M) : (L2.addSubgroupOf (M ⊓ V2)).index = B.d₁ * B.d₂

[A ∩ V₂ : L₂] = d₁ d₂.

theorem Louboutin.Triang.index_V2 {M : AddSubgroup (Fin 4 → ℚ)} (B : Triang M) (h1 : B.d₁ = 1) : (L2.addSubgroupOf (M ⊓ V2)).index = B.d₂

With d₁ = 1, d₂ = [A ∩ V₂ : L₂].

The five conditions

def Louboutin.lin (ω : Fin 4 → ℚ) (c : Fin 4 → ℤ) : Fin 4 → ℚ

1·c₀ + α·c₁ + α²·c₂ + ω·c₃.

Equations

• Louboutin.lin ω c = c 0 • Louboutin.apow 0 + c 1 • Louboutin.apow 1 + c 2 • Louboutin.apow 2 + c 3 • ω

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

(i): {1, α, α², ω} is a ℤ-basis of M (ω ∈ M and unique integer coordinates).

Equations

• Louboutin.BasisWith M ω = (ω ∈ M ∧ ∀ x ∈ M, ∃! c : Fin 4 → ℤ, x = Louboutin.lin ω c)

def Louboutin.expSet (M : AddSubgroup (Fin 4 → ℚ)) : Set ℕ

(v): the set {e ≥ 1 | eM ⊆ ℤ[α]}.

Equations

• Louboutin.expSet M = {e : ℕ | 1 ≤ e ∧ ∀ x ∈ M, e • x ∈ Louboutin.Z4}

theorem Louboutin.lin_apply_three (ω : Fin 4 → ℚ) (c : Fin 4 → ℤ) : lin ω c 3 = ↑(c 3) * ω 3

theorem Louboutin.lin_apply_two (ω : Fin 4 → ℚ) (c : Fin 4 → ℤ) : lin ω c 2 = ↑(c 2) + ↑(c 3) * ω 2

theorem Louboutin.lin_apply_one (ω : Fin 4 → ℚ) (c : Fin 4 → ℤ) : lin ω c 1 = ↑(c 1) + ↑(c 3) * ω 1

theorem Louboutin.lin_apply_zero (ω : Fin 4 → ℚ) (c : Fin 4 → ℤ) : lin ω c 0 = ↑(c 0) + ↑(c 3) * ω 0

theorem Louboutin.lin_injective {ω : Fin 4 → ℚ} (hω : ω 3 ≠ 0) : Function.Injective (lin ω)

theorem Louboutin.Triang.saturated_of_basis {M : AddSubgroup (Fin 4 → ℚ)} (B : Triang M) {ω : Fin 4 → ℚ} (hω : BasisWith M ω) : Saturated M

(i) ⇒ (ii).

theorem Louboutin.Triang.d₂_eq_one_of_saturated {M : AddSubgroup (Fin 4 → ℚ)} (B : Triang M) (hsat : Saturated M) : B.d₂ = 1

(ii) ⇒ (iii).

theorem Louboutin.Triang.d₁_eq_one_of_d₂ {M : AddSubgroup (Fin 4 → ℚ)} (B : Triang M) (h2 : B.d₂ = 1) : B.d₁ = 1

theorem Louboutin.Triang.basis_of_d₂_eq_one {M : AddSubgroup (Fin 4 → ℚ)} (B : Triang M) (h2 : B.d₂ = 1) : BasisWith M B.ω₃

(iii) ⇒ (i), with ω = ω₃.

theorem Louboutin.Triang.T1_i_iff_ii {M : AddSubgroup (Fin 4 → ℚ)} (B : Triang M) : (∃ (ω : Fin 4 → ℚ), BasisWith M ω) ↔ Saturated M

(i) ⇔ (ii).

theorem Louboutin.Triang.T1_ii_iff_iii {M : AddSubgroup (Fin 4 → ℚ)} (B : Triang M) : Saturated M ↔ B.d₂ = 1

(ii) ⇔ (iii).

theorem Louboutin.Triang.T1_iii_iff_iv {M : AddSubgroup (Fin 4 → ℚ)} (B : Triang M) : B.d₂ = 1 ↔ IsAddCyclic (↥M ⧸ Z4.addSubgroupOf M)

(iii) ⇔ (iv).

theorem Louboutin.Triang.isLeast_expSet {M : AddSubgroup (Fin 4 → ℚ)} (B : Triang M) : IsLeast (expSet M) B.d₃

min{e ≥ 1 : eM ⊆ ℤ[α]} = d₃.

theorem Louboutin.Triang.T1_iii_iff_v {M : AddSubgroup (Fin 4 → ℚ)} (B : Triang M) : B.d₂ = 1 ↔ IsLeast (expSet M) (Z4.addSubgroupOf M).index

(iii) ⇔ (v).

theorem Louboutin.Triang.T1_mod_p {M : AddSubgroup (Fin 4 → ℚ)} (B : Triang M) {p : ℕ} (hp : Nat.Prime p) : p ∣ B.d₂ ↔ ∃ (c : Fin 3 → ℤ), (¬∀ (i : Fin 3), ↑p ∣ c i) ∧ ∃ y ∈ M, c 0 • apow 0 + c 1 • apow 1 + c 2 • apow 2 = p • y

p ∣ d₂ iff 1, α, α² are linearly dependent over 𝔽_p in A/pA, that is, there are c₀, c₁, c₂ ∈ ℤ, not all divisible by p, with c₀ + c₁α + c₂α² ∈ pA.

theorem Louboutin.Triang.prop_T1 {M : AddSubgroup (Fin 4 → ℚ)} (B : Triang M) (h1 : B.d₁ = 1) : Nonempty (↥M ⧸ Z4.addSubgroupOf M ≃+ ZMod B.d₂ × ZMod B.d₃) ∧ (L2.addSubgroupOf (M ⊓ V2)).index = B.d₂ ∧ [∃ (ω : Fin 4 → ℚ), BasisWith M ω, Saturated M, B.d₂ = 1, IsAddCyclic (↥M ⧸ Z4.addSubgroupOf M), IsLeast (expSet M) (Z4.addSubgroupOf M).index].TFAE ∧ ∀ (p : ℕ), Nat.Prime p → (p ∣ B.d₂ ↔ ∃ (c : Fin 3 → ℤ), (¬∀ (i : Fin 3), ↑p ∣ c i) ∧ ∃ y ∈ M, c 0 • apow 0 + c 1 • apow 1 + c 2 • apow 2 = p • y)

The proposition, for M = A with d₁ = 1 (Louboutin 2020, Thm. 13): A/ℤ[α] ≅ ℤ/d₂ × ℤ/d₃, d₂ = [A ∩ V₂ : L₂], (i)–(v) equivalent, and the clause modulo p.

Non-vacuity: every datum (d₁ ∣ d₂ ∣ d₃, P_k) is realized

def Louboutin.combOfHom (ω₁ ω₂ ω₃ : Fin 4 → ℚ) : (Fin 4 → ℤ) →+ Fin 4 → ℚ

combOf as a homomorphism.

Equations

• Louboutin.combOfHom ω₁ ω₂ ω₃ = { toFun := Louboutin.combOf ω₁ ω₂ ω₃, map_zero' := ⋯, map_add' := ⋯ }

def Louboutin.Triang.ofData (d₁ d₂ d₃ : ℕ) (h₁ : 0 < d₁) (h₂ : 0 < d₂) (h₃ : 0 < d₃) (h₁₂ : d₁ ∣ d₂) (h₂₃ : d₂ ∣ d₃) (p₁₀ p₂₀ p₂₁ p₃₀ p₃₁ p₃₂ : ℤ) : Triang (combOfHom (omega1 d₁ p₁₀) (omega2 d₂ p₂₀ p₂₁) (omega3 d₃ p₃₀ p₃₁ p₃₂)).range

For every 0 < d₁ ∣ d₂ ∣ d₃ and P_k, the ℤ-module generated by 1, ω₁, ω₂, ω₃ carries a Triang structure: the hypotheses of Triang are not contradictory, for any d₂.

Equations

• One or more equations did not get rendered due to their size.