Quadratic algebras over ℤ

For a b : ℤ, QuadraticAlgebra ℤ a b is an order in QuadraticAlgebra ℚ a b.

Main results

• QuadraticAlgebra ℚ a b is the localization of QuadraticAlgebra ℤ a b at the nonzero integers and its fraction ring.
• QuadraticAlgebra.Int.isDomain_iff: QuadraticAlgebra ℤ a b is an integral domain iff discr a b is not a square.
• QuadraticAlgebra.Int.exists_im_den_sq_mul: if z is an integral element of QuadraticAlgebra ℚ a b, then discr a b is the square of the denominator of z.im times an integer congruent to 0 or 1 modulo 4.
• QuadraticAlgebra.Int.exists_isIntegral_notMem_of_sq_mul: conversely, if discr a b = d ^ 2 * e with 1 < |d| and e congruent to 0 or 1 modulo 4, then there is an integral element z not in QuadraticAlgebra ℤ a b such that d • z lies in it.

@[instance_reducible]

noncomputable instance QuadraticAlgebra.Int.instAlgebraIntRatCast {a b : ℤ} : Algebra (QuadraticAlgebra ℤ a b) (QuadraticAlgebra ℚ ↑a ↑b)

Equations

• QuadraticAlgebra.Int.instAlgebraIntRatCast = QuadraticAlgebra.algebra ℚ a b

instance QuadraticAlgebra.Int.instIsScalarTowerIntRatCast {a b : ℤ} : IsScalarTower ℤ (QuadraticAlgebra ℤ a b) (QuadraticAlgebra ℚ ↑a ↑b)

@[simp]

theorem QuadraticAlgebra.Int.re_algebraMap {a b : ℤ} (x : QuadraticAlgebra ℤ a b) : ((algebraMap (QuadraticAlgebra ℤ a b) (QuadraticAlgebra ℚ ↑a ↑b)) x).re = ↑x.re

@[simp]

theorem QuadraticAlgebra.Int.im_algebraMap {a b : ℤ} (x : QuadraticAlgebra ℤ a b) : ((algebraMap (QuadraticAlgebra ℤ a b) (QuadraticAlgebra ℚ ↑a ↑b)) x).im = ↑x.im

@[simp]

theorem QuadraticAlgebra.Int.algebraMap_omega {a b : ℤ} : (algebraMap (QuadraticAlgebra ℤ a b) (QuadraticAlgebra ℚ ↑a ↑b)) omega = omega

@[simp]

theorem QuadraticAlgebra.Int.norm_algebraMap_eq {a b : ℤ} (x : QuadraticAlgebra ℤ a b) : norm ((algebraMap (QuadraticAlgebra ℤ a b) (QuadraticAlgebra ℚ ↑a ↑b)) x) = ↑(norm x)

@[simp]

theorem QuadraticAlgebra.Int.trace_algebraMap_eq {a b : ℤ} (x : QuadraticAlgebra ℤ a b) : trace ((algebraMap (QuadraticAlgebra ℤ a b) (QuadraticAlgebra ℚ ↑a ↑b)) x) = ↑(trace x)

instance QuadraticAlgebra.Int.instFaithfulSMulIntRatCast {a b : ℤ} : FaithfulSMul (QuadraticAlgebra ℤ a b) (QuadraticAlgebra ℚ ↑a ↑b)

theorem QuadraticAlgebra.Int.exists_nat_smul_mem {a b : ℤ} (z : QuadraticAlgebra ℚ ↑a ↑b) : ∃ (n : ℕ), 0 < n ∧ n • z ∈ Set.range ⇑(algebraMap (QuadraticAlgebra ℤ a b) (QuadraticAlgebra ℚ ↑a ↑b))

instance QuadraticAlgebra.Int.instIsLocalizationIntAlgebraMapSubmonoidNonZeroDivisorsRatCast {a b : ℤ} : IsLocalization (Algebra.algebraMapSubmonoid (QuadraticAlgebra ℤ a b) (nonZeroDivisors ℤ)) (QuadraticAlgebra ℚ ↑a ↑b)

QuadraticAlgebra ℚ a b is the localization of the order QuadraticAlgebra ℤ a b at the nonzero integers.

instance QuadraticAlgebra.Int.instIsFractionRingIntRatCast {a b : ℤ} : IsFractionRing (QuadraticAlgebra ℤ a b) (QuadraticAlgebra ℚ ↑a ↑b)

theorem QuadraticAlgebra.Int.isDomain_iff {a b : ℤ} : IsDomain (QuadraticAlgebra ℤ a b) ↔ ¬IsSquare (discr a b)

instance QuadraticAlgebra.Int.instIsDomainIntOfFactNotIsSquareDiscr {a b : ℤ} [Fact ¬IsSquare (discr a b)] : IsDomain (QuadraticAlgebra ℤ a b)

Maximality of the order

theorem QuadraticAlgebra.Int.isIntegral_inv_smul_of_dvd {a b d t : ℤ} (ht₁ : d ∣ 2 * t + b) (ht₂ : 4 * d ^ 2 ∣ (2 * t + b) ^ 2 - discr a b) : IsIntegral ℤ ((↑d)⁻¹ • (t • 1 + omega))

If d ∣ 2 * t + b and 4 * d ^ 2 ∣ (2 * t + b) ^ 2 - discr a b, then (t + ω) / d is integral over ℤ.

theorem QuadraticAlgebra.Int.mem_range_iff_im_mem_range {a b : ℤ} {z : QuadraticAlgebra ℚ ↑a ↑b} (hz : IsIntegral ℤ z) : z ∈ Set.range ⇑(algebraMap (QuadraticAlgebra ℤ a b) (QuadraticAlgebra ℚ ↑a ↑b)) ↔ z.im ∈ Set.range ⇑(algebraMap ℤ ℚ)

An integral element z of QuadraticAlgebra ℚ a b lies in QuadraticAlgebra ℤ a b iff its imaginary part is an integer.

theorem QuadraticAlgebra.Int.im_den_smul_mem {a b : ℤ} {z : QuadraticAlgebra ℚ ↑a ↑b} (hz : IsIntegral ℤ z) : ↑z.im.den • z ∈ Set.range ⇑(algebraMap (QuadraticAlgebra ℤ a b) (QuadraticAlgebra ℚ ↑a ↑b))

If z is an integral element of QuadraticAlgebra ℚ a b, then the denominator of z.im times z lies in QuadraticAlgebra ℤ a b.

theorem QuadraticAlgebra.Int.exists_isIntegral_notMem_of_sq_mul {a b d e : ℤ} (hd : 1 < d.natAbs) (he : discr a b = d ^ 2 * e) (he' : e % 4 = 0 ∨ e % 4 = 1) : ∃ (z : QuadraticAlgebra ℚ ↑a ↑b), IsIntegral ℤ z ∧ d • z ∈ Set.range ⇑(algebraMap (QuadraticAlgebra ℤ a b) (QuadraticAlgebra ℚ ↑a ↑b)) ∧ z ∉ Set.range ⇑(algebraMap (QuadraticAlgebra ℤ a b) (QuadraticAlgebra ℚ ↑a ↑b))

If discr a b = d ^ 2 * e with e congruent to 0 or 1 modulo 4 and 1 < |d|, then there is an integral element z of QuadraticAlgebra ℚ a b such that d • z lies in QuadraticAlgebra ℤ a b but z does not.

theorem QuadraticAlgebra.Int.exists_mul_im_sq_eq {a b : ℤ} {z : QuadraticAlgebra ℚ ↑a ↑b} {x : QuadraticAlgebra ℤ a b} {d : ℤ} (hz : IsIntegral ℤ z) (hx : (algebraMap (QuadraticAlgebra ℤ a b) (QuadraticAlgebra ℚ ↑a ↑b)) x = d • z) : ∃ (t : ℤ) (n : ℤ), discr a b * x.im ^ 2 = d ^ 2 * (t ^ 2 - 4 * n)

If z is integral and d • z is the image of an element x of QuadraticAlgebra ℤ a b, then discr a b * x.im ^ 2 is d ^ 2 times t ^ 2 - 4 * n (here t and n are the trace and the norm of z).

theorem QuadraticAlgebra.Int.exists_sq_mul_of_isCoprime {a b : ℤ} {z : QuadraticAlgebra ℚ ↑a ↑b} {x : QuadraticAlgebra ℤ a b} {d : ℤ} (hz : IsIntegral ℤ z) (hd : IsCoprime d x.im) (hx : (algebraMap (QuadraticAlgebra ℤ a b) (QuadraticAlgebra ℚ ↑a ↑b)) x = d • z) : ∃ (e : ℤ), discr a b = d ^ 2 * e ∧ (e % 4 = 0 ∨ e % 4 = 1)

Let z be an integral element such that d • z is the image of an element x of QuadraticAlgebra ℤ a b, with d coprime to x.im. Then discr a b is d ^ 2 times an integer congruent to 0 or 1 modulo 4.

theorem QuadraticAlgebra.Int.exists_im_den_sq_mul {a b : ℤ} {z : QuadraticAlgebra ℚ ↑a ↑b} (hz : IsIntegral ℤ z) : ∃ (e : ℤ), discr a b = ↑z.im.den ^ 2 * e ∧ (e % 4 = 0 ∨ e % 4 = 1)

If z is an integral element of QuadraticAlgebra ℚ a b, then discr a b is the square of the denominator of z.im times an integer congruent to 0 or 1 modulo 4.