The complex embeddings of an imaginary quadratic field

For a rational a ≤ 0, the model QuadraticAlgebra ℚ a 0 of ℚ(√a) has a distinguished complex embedding QuadraticAlgebra.complexEmbedding, sending the generator ω to √(-a) · i, the square root of a with nonnegative imaginary part. Every complex embedding of the model is this one or its complex conjugate, and complex conjugation of the distinguished embedding is precomposition with the quadratic involution QuadraticAlgebra.starAlgEquiv. For a nonsquare a < 0 the model is an imaginary quadratic field: the two embeddings are distinct and are told apart by the sign of the imaginary part of the image of ω, so the field has a single infinite place, which is complex, and its signature is (0, 1).

The distinguished embedding fixes the orientation convention for imaginary quadratic fields: the chosen square root of the radicand lies in the upper half-plane.

Main definitions and results

• QuadraticAlgebra.complexEmbedding: the embedding ω ↦ √(-a) · i.
• QuadraticAlgebra.complexEmbedding_star: it intertwines star with complex conjugation.
• QuadraticAlgebra.algHom_eq_or_eq_comp_starAlgEquiv: every ℚ-algebra map to ℂ is the distinguished embedding or its precomposition with starAlgEquiv.
• QuadraticAlgebra.complexEmbedding_comp_smulOmegaEquiv_of_pos, QuadraticAlgebra.complexEmbedding_comp_smulOmegaEquiv_of_neg: along the rescaling isomorphism QuadraticAlgebra.smulOmegaEquiv u h : ℚ(√d) ≃ₐ[ℚ] ℚ(√e) with d = u² e, the distinguished embedding of ℚ(√e) pulls back to that of ℚ(√d) when u > 0 and to its complex conjugate when u < 0.
• QuadraticAlgebra.ringHom_eq_complexEmbedding_iff: for a < 0, a ring homomorphism to ℂ is the distinguished embedding exactly when it sends ω into the upper half-plane.
• QuadraticAlgebra.ringHom_eq_or_eq_conjugate: the two complex embeddings of the field model.
• QuadraticAlgebra.isConj_complexEmbedding: complex conjugation induces starAlgEquiv.
• QuadraticAlgebra.not_isReal_complexEmbedding: for a < 0 the distinguished embedding is not real.
• QuadraticAlgebra.eq_mk_complexEmbedding: the unique infinite place.
• QuadraticAlgebra.nrComplexPlaces_eq_one: there is exactly one complex place; together with NumberField.IsTotallyComplex.nrRealPlaces_eq_zero (via QuadraticAlgebra.isTotallyComplex_iff) the signature is (0, 1).

noncomputable def QuadraticAlgebra.complexEmbedding {a : ℚ} (ha : a ≤ 0) : QuadraticAlgebra ℚ a 0 →ₐ[ℚ] ℂ

The distinguished complex embedding of ℚ(√a) for a ≤ 0: the ℚ-algebra map QuadraticAlgebra ℚ a 0 →ₐ[ℚ] ℂ sending ω to √(-a) · i, the square root of a with nonnegative imaginary part.

@[simp]

theorem QuadraticAlgebra.complexEmbedding_omega {a : ℚ} (ha : a ≤ 0) : (complexEmbedding ha) omega = ↑√(-↑a) * Complex.I

theorem QuadraticAlgebra.complexEmbedding_apply {a : ℚ} (ha : a ≤ 0) (z : QuadraticAlgebra ℚ a 0) : (complexEmbedding ha) z = ↑z.re + ↑z.im * (↑√(-↑a) * Complex.I)

@[simp]

theorem QuadraticAlgebra.re_complexEmbedding {a : ℚ} (ha : a ≤ 0) (z : QuadraticAlgebra ℚ a 0) : ((complexEmbedding ha) z).re = ↑z.re

@[simp]

theorem QuadraticAlgebra.im_complexEmbedding {a : ℚ} (ha : a ≤ 0) (z : QuadraticAlgebra ℚ a 0) : ((complexEmbedding ha) z).im = ↑z.im * √(-↑a)

@[simp]

theorem QuadraticAlgebra.complexEmbedding_star {a : ℚ} (ha : a ≤ 0) (z : QuadraticAlgebra ℚ a 0) : (complexEmbedding ha) (star z) = (starRingEnd ℂ) ((complexEmbedding ha) z)

The distinguished embedding intertwines the quadratic involution with complex conjugation.

theorem QuadraticAlgebra.algHom_eq_or_eq_comp_starAlgEquiv {a : ℚ} (ha : a ≤ 0) (φ : QuadraticAlgebra ℚ a 0 →ₐ[ℚ] ℂ) : φ = complexEmbedding ha ∨ φ = (complexEmbedding ha).comp ↑starAlgEquiv

The two complex embeddings of ℚ(√a). For a ≤ 0, every ℚ-algebra map QuadraticAlgebra ℚ a 0 → ℂ is the distinguished embedding or its precomposition with the quadratic involution, since it sends ω to a square root of a.

theorem QuadraticAlgebra.ringHom_eq_complexEmbedding_iff {a : ℚ} (ha : a < 0) (φ : QuadraticAlgebra ℚ a 0 →+* ℂ) : φ = ↑(complexEmbedding ⋯) ↔ 0 < (φ omega).im

The upper half-plane picks out the distinguished embedding. For a < 0, a ring homomorphism QuadraticAlgebra ℚ a 0 →+* ℂ is the distinguished embedding exactly when it sends ω to a complex number with positive imaginary part.

theorem QuadraticAlgebra.complexEmbedding_comp_smulOmegaEquiv_of_pos {d e : ℚ} (hd : d ≤ 0) (he : e ≤ 0) (u : ℚˣ) (h : d = ↑u ^ 2 * e) (hu : 0 < ↑u) : (complexEmbedding he).comp ↑(smulOmegaEquiv u h) = complexEmbedding hd

Naturality of the distinguished embedding, positive scalar. If d = u² e with u > 0, the distinguished embedding of ℚ(√e) composed with the rescaling isomorphism smulOmegaEquiv u h : ℚ(√d) ≃ₐ[ℚ] ℚ(√e) is the distinguished embedding of ℚ(√d).

theorem QuadraticAlgebra.complexEmbedding_comp_smulOmegaEquiv_of_neg {d e : ℚ} (hd : d ≤ 0) (he : e ≤ 0) (u : ℚˣ) (h : d = ↑u ^ 2 * e) (hu : ↑u < 0) : (complexEmbedding he).comp ↑(smulOmegaEquiv u h) = (complexEmbedding hd).comp ↑starAlgEquiv

Naturality of the distinguished embedding, negative scalar. If d = u² e with u < 0, the distinguished embedding of ℚ(√e) composed with the rescaling isomorphism smulOmegaEquiv u h : ℚ(√d) ≃ₐ[ℚ] ℚ(√e) is the complex conjugate of the distinguished embedding of ℚ(√d), that is, its precomposition with the quadratic involution.

theorem QuadraticAlgebra.ringHom_eq_or_eq_conjugate {a : ℚ} [Fact ¬IsSquare a] (ha : a ≤ 0) (φ : QuadraticAlgebra ℚ a 0 →+* ℂ) : φ = ↑(complexEmbedding ha) ∨ φ = NumberField.ComplexEmbedding.conjugate ↑(complexEmbedding ha)

The two complex embeddings of an imaginary quadratic field. For a nonsquare a ≤ 0, every complex embedding of the field QuadraticAlgebra ℚ a 0 is the distinguished embedding or its complex conjugate.

theorem QuadraticAlgebra.isConj_complexEmbedding {a : ℚ} [Fact ¬IsSquare a] (ha : a ≤ 0) : NumberField.ComplexEmbedding.IsConj (↑(complexEmbedding ha)) starAlgEquiv

Complex conjugation induces the quadratic involution. Under the distinguished embedding, complex conjugation restricts to starAlgEquiv, the nontrivial automorphism of QuadraticAlgebra ℚ a 0 over ℚ.

theorem QuadraticAlgebra.not_isReal_complexEmbedding {a : ℚ} [Fact ¬IsSquare a] (ha : a < 0) : ¬NumberField.ComplexEmbedding.IsReal ↑(complexEmbedding ⋯)

For a negative nonsquare a, the distinguished embedding is not real: the field QuadraticAlgebra ℚ a 0 is totally complex.

theorem QuadraticAlgebra.eq_mk_complexEmbedding {a : ℚ} [Fact ¬IsSquare a] (ha : a ≤ 0) (w : NumberField.InfinitePlace (QuadraticAlgebra ℚ a 0)) : w = NumberField.InfinitePlace.mk ↑(complexEmbedding ha)

An imaginary quadratic field has a single infinite place: every infinite place of QuadraticAlgebra ℚ a 0, for a nonsquare a ≤ 0, is the one defined by the distinguished embedding.

theorem QuadraticAlgebra.nrComplexPlaces_eq_one {a : ℚ} [Fact ¬IsSquare a] (ha : a < 0) : NumberField.InfinitePlace.nrComplexPlaces (QuadraticAlgebra ℚ a 0) = 1

An imaginary quadratic field has exactly one complex place, so its signature is (0, 1).