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.

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