feat(Algebra/QuadraticAlgebra): quadratic orders over ℤ and their fraction ring

Mathlib.lean

@@ -1211,6 +1211,7 @@ public import Mathlib.Algebra.Prime.Lemmas
 public import Mathlib.Algebra.QuadraticAlgebra.Basic
 public import Mathlib.Algebra.QuadraticAlgebra.Defs
 public import Mathlib.Algebra.QuadraticAlgebra.Discr
+public import Mathlib.Algebra.QuadraticAlgebra.Int
 public import Mathlib.Algebra.QuadraticAlgebra.NormDeterminant
 public import Mathlib.Algebra.QuadraticDiscriminant
 public import Mathlib.Algebra.Quandle

Mathlib/Algebra/QuadraticAlgebra/Basic.lean

@@ -21,8 +21,11 @@ Let `R` be a commutative ring. We define:
 
 * `QuadraticAlgebra.trace`: the trace, as an `R`-linear map
 
-* `QuadraticAlgebra.map` and `QuadraticAlgebra.mapEquiv`: the `R`-algebra map, respectively
-  isomorphism (when `u` is a unit), induced by the change of generator `ω ↦ u • ω + k`
+* `QuadraticAlgebra.changeGenerator` and `QuadraticAlgebra.changeGeneratorEquiv`: the `R`-algebra
+  map, respectively isomorphism (when `u` is a unit), induced by the change of generator
+  `ω ↦ u • ω + k`
+
+* `QuadraticAlgebra.baseChange`: the `R`-algebra map induced by a base change `R → S`
 
 We prove:
 
@@ -380,54 +383,106 @@ theorem sq_eq_trace_smul_sub_norm :
 
 end trace
 
-section map
+section changeGenerator
 
 variable [CommRing R]
 
 -- The quadratic relation satisfied by the new generator `u • ω + k`; this is what makes
--- `map` well defined. Stated with `x * x` rather than `x ^ 2` to match the shape of the
--- subtype condition of `lift` (`{ u // u * u = a • 1 + b • u }`), so it feeds `map` verbatim.
-private theorem map_relation (a b u k : R) :
+-- `changeGenerator` well defined. Stated with `x * x` rather than `x ^ 2` to match the shape of
+-- the subtype condition of `lift` (`{ u // u * u = a • 1 + b • u }`), so it feeds
+-- `changeGenerator` verbatim.
+private theorem changeGenerator_relation (a b u k : R) :
     (u • ω + algebraMap R (QuadraticAlgebra R a b) k) *
         (u • ω + algebraMap R (QuadraticAlgebra R a b) k) =
       (u ^ 2 * a - u * b * k - k ^ 2) • 1 +
         (u * b + 2 * k) • (u • ω + algebraMap R (QuadraticAlgebra R a b) k) := by
   ext <;> simp <;> ring
 
-/-- The `R`-algebra map induced by the change of generator `ω ↦ u • ω + k`, see `map_omega`. -/
+/-- The `R`-algebra map induced by the change of generator `ω ↦ u • ω + k`, see
+`changeGenerator_omega`. -/
 @[simps!]
-def map (a b u k : R) {a' b' : R} (ha : a' = u ^ 2 * a - u * b * k - k ^ 2)
+def changeGenerator (a b u k : R) {a' b' : R} (ha : a' = u ^ 2 * a - u * b * k - k ^ 2)
     (hb : b' = u * b + 2 * k) :
     QuadraticAlgebra R a' b' →ₐ[R] QuadraticAlgebra R a b :=
-  lift ⟨u • ω + algebraMap R _ k, by rw [ha, hb]; exact map_relation a b u k⟩
+  lift ⟨u • ω + algebraMap R _ k, by rw [ha, hb]; exact changeGenerator_relation a b u k⟩
 
 @[simp]
-theorem map_omega (a b u k : R) {a' b' : R} (ha : a' = u ^ 2 * a - u * b * k - k ^ 2)
+theorem changeGenerator_omega (a b u k : R) {a' b' : R} (ha : a' = u ^ 2 * a - u * b * k - k ^ 2)
     (hb : b' = u * b + 2 * k) :
-    map a b u k ha hb ω = u • ω + algebraMap R (QuadraticAlgebra R a b) k := by
+    changeGenerator a b u k ha hb ω = u • ω + algebraMap R (QuadraticAlgebra R a b) k := by
   ext <;> simp
 
-theorem map_injective (a b u k : R) {a' b' : R} (ha : a' = u ^ 2 * a - u * b * k - k ^ 2)
+theorem changeGenerator_injective (a b u k : R) {a' b' : R}
+    (ha : a' = u ^ 2 * a - u * b * k - k ^ 2)
     (hb : b' = u * b + 2 * k) (hu : IsRegular u) :
-    Function.Injective (map a b u k ha hb) := by
+    Function.Injective (changeGenerator a b u k ha hb) := by
   intro z w h
   have hy : z.im = w.im := hu.right <| by simpa using congr_arg im h
   exact QuadraticAlgebra.ext (by simpa [hy] using congr_arg re h) hy
 
-/-- `map` along a unit `u`, as an isomorphism. -/
+/-- `changeGenerator` along a unit `u`, as an isomorphism. -/
 @[simps! apply symm_apply]
-def mapEquiv (a b : R) (u : Rˣ) (k : R) {a' b' : R}
+def changeGeneratorEquiv (a b : R) (u : Rˣ) (k : R) {a' b' : R}
     (ha : a' = (u : R) ^ 2 * a - (u : R) * b * k - k ^ 2)
     (hb : b' = (u : R) * b + 2 * k) :
     QuadraticAlgebra R a' b' ≃ₐ[R] QuadraticAlgebra R a b where
-  __ := map a b u k ha hb
-  invFun := map a' b' (u⁻¹ : Rˣ) (-(u⁻¹ : Rˣ) * k)
+  __ := changeGenerator a b u k ha hb
+  invFun := changeGenerator a' b' (u⁻¹ : Rˣ) (-(u⁻¹ : Rˣ) * k)
     (by grind [sq, mul_assoc, Units.inv_mul_cancel_left])
     (by grind [Units.inv_mul_cancel_left])
   left_inv _ := by ext <;> simp [mul_assoc]
   right_inv _ := by ext <;> simp [mul_assoc]
 
-end map
+@[deprecated (since := "2026-08-14")] alias map := changeGenerator
+@[deprecated (since := "2026-08-14")] alias map_omega := changeGenerator_omega
+@[deprecated (since := "2026-08-14")] alias map_injective := changeGenerator_injective
+@[deprecated (since := "2026-08-14")] alias mapEquiv := changeGeneratorEquiv
+
+end changeGenerator
+
+section baseChange
+
+variable {R S : Type*} (S)
+
+section CommSemiring
+
+variable [CommSemiring R] [CommRing S] [Algebra R S] (a b : R)
+
+/-- The `R`-algebra map between quadratic algebras induced by the base change `R → S`,
+sending `ω` to `ω`. -/
+@[simps!]
+def baseChange :
+    QuadraticAlgebra R a b →ₐ[R] QuadraticAlgebra S (algebraMap R S a) (algebraMap R S b) :=
+  lift ⟨omega, by ext <;> simp [Algebra.algebraMap_eq_smul_one]⟩
+
+theorem baseChange_omega :
+    baseChange S a b ω = ω := by
+  ext <;> simp
+
+theorem baseChange_injective [FaithfulSMul R S] :
+    Function.Injective (baseChange S a b) := by
+  intro _ _ h
+  simp only [QuadraticAlgebra.ext_iff, re_baseChange_apply, ← Algebra.algebraMap_eq_smul_one,
+    algebraMap.coe_inj, im_baseChange_apply] at h
+  exact QuadraticAlgebra.ext_iff.mpr h
+
+end CommSemiring
+
+section CommRing
+
+variable [CommRing R] [CommRing S] [Algebra R S] (a b : R)
+
+theorem norm_baseChange (x : QuadraticAlgebra R a b) :
+    norm (baseChange S a b x) = algebraMap R S (norm x) := by
+  simp [norm_def, Algebra.smul_def]
+
+theorem trace_baseChange (x : QuadraticAlgebra R a b) :
+    trace (baseChange S a b x) = algebraMap R S (trace x) := by
+  simp [trace_def, Algebra.smul_def, map_ofNat]
+
+end CommRing
+
+end baseChange
 
 section field
 

Mathlib/Algebra/QuadraticAlgebra/Discr.lean

@@ -20,8 +20,8 @@ over a field, a criterion for `QuadraticAlgebra K a b` to be a field.
 
 ## Main results
 
-* `QuadraticAlgebra.discr_map`: the discriminant scales by `u ^ 2` under the change of
-  generator `ω ↦ u • ω + k`.
+* `QuadraticAlgebra.discr_changeGenerator`: the discriminant scales by `u ^ 2` under the change
+  of generator `ω ↦ u • ω + k`.
 * `QuadraticAlgebra.exists_sq_eq_iff_isSquare_discr`: over a ring with `2` invertible,
   `X ^ 2 - b * X - a` has a root iff `discr a b` is a square.
 * `QuadraticAlgebra.isField_iff_not_isSquare_discr`: over a field with `2 ≠ 0`,
@@ -42,12 +42,20 @@ def discr [CommSemiring R] (a b : R) : R := b ^ 2 + 4 * a
 
 theorem discr_def [CommSemiring R] (a b : R) : discr a b = b ^ 2 + 4 * a := rfl
 
-/-- Under the change of generator `ω ↦ u • ω + k` (see `QuadraticAlgebra.map`), the
+/-- The discriminant commutes with a base change `R → S`. -/
+@[simp]
+theorem discr_algebraMap {S : Type*} [CommSemiring R] [CommSemiring S] [Algebra R S] (a b : R) :
+    discr (algebraMap R S a) (algebraMap R S b) = algebraMap R S (discr a b) := by
+  simp [discr_def, map_ofNat]
+
+/-- Under the change of generator `ω ↦ u • ω + k` (see `QuadraticAlgebra.changeGenerator`), the
 discriminant is multiplied by `u ^ 2`. -/
-theorem discr_map [CommRing R] (a b u k : R) :
+theorem discr_changeGenerator [CommRing R] (a b u k : R) :
     discr (u ^ 2 * a - u * b * k - k ^ 2) (u * b + 2 * k) = u ^ 2 * discr a b := by
   rw [discr_def, discr_def]; ring
 
+@[deprecated (since := "2026-08-14")] alias discr_map := discr_changeGenerator
+
 /-- The discriminant is the square of the different `ω - star ω`. -/
 theorem algebraMap_discr [CommRing R] (a b : R) :
     algebraMap R (QuadraticAlgebra R a b) (discr a b) = (ω - star ω) ^ 2 := by

Mathlib/Algebra/QuadraticAlgebra/Int.lean

@@ -0,0 +1,100 @@
+/-
+Copyright (c) 2026 Xavier Roblot. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Xavier Roblot
+-/
+module
+
+public import Mathlib.Algebra.QuadraticAlgebra.Discr
+public import Mathlib.RingTheory.Localization.FractionRing
+public import Mathlib.Data.Rat.Lemmas
+
+/-!
+# 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.
+-/
+
+@[expose] public section
+
+namespace QuadraticAlgebra
+
+open Algebra
+
+namespace Int
+
+variable {a b : ℤ}
+
+noncomputable instance : Algebra (QuadraticAlgebra ℤ a b) (QuadraticAlgebra ℚ a b) :=
+  (baseChange ℚ a b).toRingHom.toAlgebra
+
+instance : IsScalarTower ℤ (QuadraticAlgebra ℤ a b) (QuadraticAlgebra ℚ a b) :=
+  .of_algHom (baseChange ℚ a b)
+
+theorem algebraMap_eq (x : QuadraticAlgebra ℤ a b) :
+    algebraMap (QuadraticAlgebra ℤ a b) (QuadraticAlgebra ℚ a b) x = baseChange ℚ a b x := rfl
+
+@[simp]
+theorem algebraMap_re_eq (x : QuadraticAlgebra ℤ a b) :
+    (algebraMap (QuadraticAlgebra ℤ a b) (QuadraticAlgebra ℚ a b) x).re = x.re := by
+  simp [algebraMap_eq, re_baseChange_apply ℚ]
+
+@[simp]
+theorem algebraMap_im_eq (x : QuadraticAlgebra ℤ a b) :
+    (algebraMap (QuadraticAlgebra ℤ a b) (QuadraticAlgebra ℚ a b) x).im = x.im := by
+  simp [algebraMap_eq, im_baseChange_apply ℚ]
+
+instance : FaithfulSMul (QuadraticAlgebra ℤ a b) (QuadraticAlgebra ℚ a b) :=
+  (faithfulSMul_iff_algebraMap_injective _ _).mpr <| baseChange_injective ℚ _ _
+
+/-- The discriminant commutes with the coercion `ℤ → ℚ`. -/
+theorem discr_intCast :
+    discr (a : ℚ) (b : ℚ) = discr a b := by
+  simpa using discr_algebraMap (S := ℚ) a b
+
+open scoped nonZeroDivisors
+
+theorem exists_nat_smul_mem (z : QuadraticAlgebra ℚ a b) :
+    ∃ n : ℕ, 0 < n ∧ n • z ∈ Set.range (baseChange ℚ a b) := by
+  obtain ⟨n, hn, x, y, hx, hy⟩ : ∃ n : ℕ, 0 < n ∧ ∃ x y : ℤ, n * z.re = x ∧ n * z.im = y :=
+    ⟨z.re.den * z.im.den, by positivity, z.im.den * z.re.num, z.re.den * z.im.num,
+      by push_cast; grind [← Rat.mul_den_eq_num]⟩
+  refine ⟨n, hn, x • 1 + y • ω, ?_⟩
+  ext <;> simp [re_baseChange_apply ℚ, im_baseChange_apply ℚ, hx, hy]
+
+/-- `QuadraticAlgebra ℚ a b` is the localization of the order `QuadraticAlgebra ℤ a b` at the
+nonzero integers. This is not `IsFractionRing` in general: `QuadraticAlgebra ℤ a b` need not be a
+domain (see `isDomain_iff`). -/
+noncomputable instance :
+    IsLocalization (algebraMapSubmonoid (QuadraticAlgebra ℤ a b) ℤ⁰)
+      (QuadraticAlgebra ℚ a b) := by
+  refine ⟨fun ⟨y, ⟨x, hx, hy⟩⟩ ↦ ?_, fun x ↦ ?_, fun h ↦ ⟨1, by simpa using h⟩⟩
+  · dsimp only
+    rw [← hy, ← IsScalarTower.algebraMap_apply, IsScalarTower.algebraMap_apply ℤ ℚ]
+    exact IsUnit.map _ <| by simpa [isUnit_iff_ne_zero] using hx
+  · obtain ⟨n, hn, ⟨w, hw⟩⟩ := exists_nat_smul_mem x
+    exact ⟨⟨w, n, ⟨n, by simpa using hn.ne', rfl⟩⟩, by simp [algebraMap_eq, hw, mul_comm]⟩
+
+instance : IsFractionRing (QuadraticAlgebra ℤ a b) (QuadraticAlgebra ℚ a b) := by
+  refine IsLocalization.of_le (algebraMapSubmonoid (QuadraticAlgebra ℤ a b) ℤ⁰) _ ?_ ?_
+  · rintro _ ⟨x, hx, rfl⟩
+    exact norm_mem_nonZeroDivisors_iff.mp <| by simpa using hx
+  · intro x hx
+    rwa [isUnit_iff_norm_isUnit, isUnit_iff_ne_zero, algebraMap_eq, norm_baseChange ℚ a b,
+      eq_intCast, Int.cast_ne_zero, ← mem_nonZeroDivisors_iff_ne_zero, norm_mem_nonZeroDivisors_iff]
+
+theorem isDomain_iff :
+    IsDomain (QuadraticAlgebra ℤ a b) ↔ ¬ IsSquare (discr a b) := by
+  simp [IsFractionRing.isDomain_iff_isField (K := QuadraticAlgebra ℚ a b),
+    isField_iff_not_isSquare_discr, discr_intCast]
+
+end Int
+
+end QuadraticAlgebra

Mathlib/RingTheory/Localization/FractionRing.lean

@@ -243,6 +243,12 @@ lemma surjective_iff_isField [IsDomain R] : Function.Surjective (algebraMap R K)
     (IsLocalization.atUnits R _ (S := K)
       (fun _ hx ↦ Ne.isUnit (mem_nonZeroDivisors_iff_ne_zero.mp hx))).surjective
 
+/-- The fraction ring `K` of `R` is a field iff `R` is an integral domain. -/
+theorem isDomain_iff_isField : IsDomain R ↔ IsField K := by
+  refine ⟨fun h ↦ (IsFractionRing.toField R).toIsField K, fun h ↦ ?_⟩
+  let := h.toField
+  exact IsDomain.of_faithfulSMul _ K
+
 end CommRing
 
 variable {B : Type*} [CommRing B] [IsDomain B] [Field K] {L : Type*} [Field L] [Algebra A K]