Isomorphisms between the models R(√d)

For a commutative ring R and a unit u with d = u² e, rescaling the generator gives an explicit R-algebra isomorphism QuadraticAlgebra.smulOmegaEquiv u h from QuadraticAlgebra R d 0 to QuadraticAlgebra R e 0, sending ω to u • ω; its inverse sends ω to u⁻¹ • ω. These isomorphisms are closed under inverse and composition. When 2 is regular in R every isomorphism between the two models is of this form, because an isomorphism preserves traces and norms (QuadraticAlgebra.trace_algHom_omega, QuadraticAlgebra.norm_algHom_omega). Over a field of characteristic other than 2 this recovers the classification of the models K(√d), for nonzero d, by the class of d in the square-class group Kˣ ⧸ (Kˣ)².

The isomorphisms are the specialisation of Mathlib's change of generator QuadraticAlgebra.changeGeneratorEquiv to ω ↦ u • ω. The square-class criterion is the b = 0 form of Mathlib's classification of quadratic algebras by their discriminant modulo unit squares, QuadraticAlgebra.nonempty_algEquiv_iff_of_invertible_two, read in the square-class group; its squarefree-integer form over ℚ is QuadraticAlgebra.Rat.nonempty_algEquiv_iff.

Main definitions and results

• QuadraticAlgebra.smulOmegaEquiv: the isomorphism R(√d) ≃ₐ[R] R(√e), ω ↦ u • ω, for d = u² e, with smulOmegaEquiv_omega and smulOmegaEquiv_symm_omega giving its values on the generator in both directions.
• QuadraticAlgebra.smulOmegaEquiv_symm, QuadraticAlgebra.smulOmegaEquiv_trans, QuadraticAlgebra.smulOmegaEquiv_one: inverse, composition and identity.
• QuadraticAlgebra.exists_eq_smulOmegaEquiv: if 2 is regular, every isomorphism R(√d) ≃ₐ[R] R(√e) is smulOmegaEquiv u h for the unit u = (f ω).im.
• QuadraticAlgebra.nonempty_algEquiv_iff_exists_eq_sq_mul: if 2 is regular, R(√d) ≃ₐ[R] R(√e) exactly when d = u² e for a unit u.
• QuadraticAlgebra.nonempty_algEquiv_iff_squareClass_eq: over a field with 2 ≠ 0, for nonzero d and e, K(√d) ≃ₐ[K] K(√e) exactly when d and e have the same square class.

def QuadraticAlgebra.smulOmegaEquiv {R : Type u_1} [CommRing R] {d e : R} (u : Rˣ) (h : d = ↑u ^ 2 * e) : QuadraticAlgebra R d 0 ≃ₐ[R] QuadraticAlgebra R e 0

Rescaling the generator. For a unit u with d = u² e, the R-algebra isomorphism QuadraticAlgebra R d 0 ≃ₐ[R] QuadraticAlgebra R e 0 sending ω to u • ω, so that x + yω ↦ x + (u y)ω.

@[simp]

theorem QuadraticAlgebra.smulOmegaEquiv_apply_re {R : Type u_1} [CommRing R] {d e : R} (u : Rˣ) (h : d = ↑u ^ 2 * e) (z : QuadraticAlgebra R d 0) : ((smulOmegaEquiv u h) z).re = z.re

@[simp]

theorem QuadraticAlgebra.smulOmegaEquiv_apply_im {R : Type u_1} [CommRing R] {d e : R} (u : Rˣ) (h : d = ↑u ^ 2 * e) (z : QuadraticAlgebra R d 0) : ((smulOmegaEquiv u h) z).im = ↑u * z.im

@[simp]

theorem QuadraticAlgebra.smulOmegaEquiv_omega {R : Type u_1} [CommRing R] {d e : R} (u : Rˣ) (h : d = ↑u ^ 2 * e) : (smulOmegaEquiv u h) omega = ↑u • omega

smulOmegaEquiv u h sends the generator ω to u • ω.

@[simp]

theorem QuadraticAlgebra.smulOmegaEquiv_symm_apply_re {R : Type u_1} [CommRing R] {d e : R} (u : Rˣ) (h : d = ↑u ^ 2 * e) (z : QuadraticAlgebra R e 0) : ((smulOmegaEquiv u h).symm z).re = z.re

@[simp]

theorem QuadraticAlgebra.smulOmegaEquiv_symm_apply_im {R : Type u_1} [CommRing R] {d e : R} (u : Rˣ) (h : d = ↑u ^ 2 * e) (z : QuadraticAlgebra R e 0) : ((smulOmegaEquiv u h).symm z).im = ↑u⁻¹ * z.im

@[simp]

theorem QuadraticAlgebra.smulOmegaEquiv_symm_omega {R : Type u_1} [CommRing R] {d e : R} (u : Rˣ) (h : d = ↑u ^ 2 * e) : (smulOmegaEquiv u h).symm omega = ↑u⁻¹ • omega

The inverse of smulOmegaEquiv u h sends the generator ω to u⁻¹ • ω.

theorem QuadraticAlgebra.smulOmegaEquiv_symm {R : Type u_1} [CommRing R] {d e : R} (u : Rˣ) (h : d = ↑u ^ 2 * e) : (smulOmegaEquiv u h).symm = smulOmegaEquiv u⁻¹ ⋯

The inverse of rescaling the generator by u is rescaling it by u⁻¹.

@[simp]

theorem QuadraticAlgebra.smulOmegaEquiv_trans {R : Type u_1} [CommRing R] {c d e : R} (u v : Rˣ) (h : d = ↑u ^ 2 * e) (h' : e = ↑v ^ 2 * c) : (smulOmegaEquiv u h).trans (smulOmegaEquiv v h') = smulOmegaEquiv (u * v) ⋯

Rescaling the generator by u and then by v is rescaling it by u * v.

@[simp]

theorem QuadraticAlgebra.smulOmegaEquiv_one {R : Type u_1} [CommRing R] {d : R} (h : d = ↑1 ^ 2 * d) : smulOmegaEquiv 1 h = AlgEquiv.refl

Rescaling the generator by 1 is the identity.

theorem QuadraticAlgebra.exists_eq_smulOmegaEquiv {R : Type u_1} [CommRing R] {d e : R} (h2 : IsRegular 2) (f : QuadraticAlgebra R d 0 ≃ₐ[R] QuadraticAlgebra R e 0) : ∃ (u : Rˣ) (h : d = ↑u ^ 2 * e), ↑u = (f omega).im ∧ f = smulOmegaEquiv u h

Every isomorphism of the models rescales the generator. If 2 is regular in R, every R-algebra isomorphism f : QuadraticAlgebra R d 0 ≃ₐ[R] QuadraticAlgebra R e 0 is smulOmegaEquiv u h for the unit u = (f ω).im: the image of ω has trace 0 and norm -d, so it is u • ω with d = u² e.

theorem QuadraticAlgebra.nonempty_algEquiv_iff_exists_eq_sq_mul {R : Type u_1} [CommRing R] {d e : R} (h2 : IsRegular 2) : Nonempty (QuadraticAlgebra R d 0 ≃ₐ[R] QuadraticAlgebra R e 0) ↔ ∃ (u : Rˣ), d = ↑u ^ 2 * e

Isomorphism of the models up to unit squares. If 2 is regular in R, the models QuadraticAlgebra R d 0 and QuadraticAlgebra R e 0 are isomorphic exactly when d = u² e for a unit u.

theorem QuadraticAlgebra.nonempty_algEquiv_iff_squareClass_eq {K : Type u_1} [Field K] [NeZero 2] {d e : K} (hd : d ≠ 0) (he : e ≠ 0) : Nonempty (QuadraticAlgebra K d 0 ≃ₐ[K] QuadraticAlgebra K e 0) ↔ TauCeti.squareClass (Units.mk0 d hd) = TauCeti.squareClass (Units.mk0 e he)

The square-class classification of the models. Over a field with 2 ≠ 0, for nonzero d and e, the models QuadraticAlgebra K d 0 and QuadraticAlgebra K e 0 of K(√d) and K(√e) are isomorphic exactly when d and e have the same class in Kˣ ⧸ (Kˣ)².