CM-extension of number fields

A CM-extension K/F of number fields is an extension where K is totally complex, F is totally real and K is a quadratic extension of F. In this situation, the totally real subfield F is (isomorphic to) the maximal real subfield of K.

Main definitions

• NumberField.CMExtension.complexConj: the complex conjugation of a CM-extension.

• NumberField.CMExtension.isConj_complexConj: the complex conjugation is the conjugation of any complex embedding of a CM-extension.

• NumberField.IsCMField: A predicate that says that if a number field is CM, then it is a totally complex quadratic extension of its totally real subfield

• NumberField.CMExtension.equivMaximalRealSubfield: Any field F such that K/F is a CM-extension is isomorphic to the maximal real subfield of K.

• NumberField.IsCM.ofIsCMExtension: Assume that there exists F such that K/F is a CM-extension. Then K is CM.

• NumberField.IsCMField.of_isMulCommutative: A totally complex abelian extension of ℚ is CM.

Implementation note

Most result are proved under the general hypothesis: K/F quadratic extension of number fields with F totally real and K totally complex and then, if relevant, we deduce the special case F = maximalRealSubfield K. Results of the first kind live in the NumberField.CMExtension namespace whereas results of the second kind live in the NumberField.IsCMField namespace.

theorem NumberField.CMExtension.card_infinitePlace_eq_card_infinitePlace (F : Type u_1) (K : Type u_2) [Field F] [NumberField F] [IsTotallyReal F] [Field K] [NumberField K] [IsTotallyComplex K] [Algebra F K] [Algebra.IsQuadraticExtension F K] : Fintype.card (InfinitePlace F) = Fintype.card (InfinitePlace K)

theorem NumberField.CMExtension.units_rank_eq_units_rank (F : Type u_1) (K : Type u_2) [Field F] [NumberField F] [IsTotallyReal F] [Field K] [NumberField K] [IsTotallyComplex K] [Algebra F K] [Algebra.IsQuadraticExtension F K] : Units.rank F = Units.rank K

theorem NumberField.CMExtension.exists_isConj (F : Type u_1) {K : Type u_2} [Field F] [NumberField F] [IsTotallyReal F] [Field K] [NumberField K] [IsTotallyComplex K] [Algebra F K] [Algebra.IsQuadraticExtension F K] (φ : K →+* ℂ) : ∃ (σ : K ≃ₐ[F] K), ComplexEmbedding.IsConj φ σ

theorem NumberField.CMExtension.isConj_eq_isConj (F : Type u_1) {K : Type u_2} [Field F] [NumberField F] [Field K] [NumberField K] [IsTotallyComplex K] [Algebra F K] [Algebra.IsQuadraticExtension F K] {φ ψ : K →+* ℂ} {σ τ : K ≃ₐ[F] K} (hφ : ComplexEmbedding.IsConj φ σ) (hψ : ComplexEmbedding.IsConj ψ τ) : σ = τ

All the conjugations of a CM-extension are the same.

noncomputable def NumberField.CMExtension.complexConj (F : Type u_1) (K : Type u_2) [Field F] [NumberField F] [IsTotallyReal F] [Field K] [NumberField K] [IsTotallyComplex K] [Algebra F K] [Algebra.IsQuadraticExtension F K] : K ≃ₐ[F] K

The complex conjugation of a CM-extension.

Equations

• NumberField.CMExtension.complexConj F K = ⋯.choose

theorem NumberField.CMExtension.isConj_complexConj (F : Type u_1) {K : Type u_2} [Field F] [NumberField F] [IsTotallyReal F] [Field K] [NumberField K] [IsTotallyComplex K] [Algebra F K] [Algebra.IsQuadraticExtension F K] (φ : K →+* ℂ) : ComplexEmbedding.IsConj φ (complexConj F K)

The complex conjugation is the conjugation of any complex embedding of a CM-extension.

theorem NumberField.CMExtension.complexConj_ne_one (F : Type u_1) (K : Type u_2) [Field F] [NumberField F] [IsTotallyReal F] [Field K] [NumberField K] [IsTotallyComplex K] [Algebra F K] [Algebra.IsQuadraticExtension F K] : complexConj F K ≠ 1

@[simp]

theorem NumberField.CMExtension.complexEmbedding_complexConj (F : Type u_1) {K : Type u_2} [Field F] [NumberField F] [IsTotallyReal F] [Field K] [NumberField K] [IsTotallyComplex K] [Algebra F K] [Algebra.IsQuadraticExtension F K] (φ : K →+* ℂ) (x : K) : φ ((complexConj F K) x) = (starRingEnd ℂ) (φ x)

@[simp]

theorem NumberField.CMExtension.complexConj_apply_apply (F : Type u_1) {K : Type u_2} [Field F] [NumberField F] [IsTotallyReal F] [Field K] [NumberField K] [IsTotallyComplex K] [Algebra F K] [Algebra.IsQuadraticExtension F K] (x : K) : (complexConj F K) ((complexConj F K) x) = x

theorem NumberField.CMExtension.orderOf_complexConj (F : Type u_1) (K : Type u_2) [Field F] [NumberField F] [IsTotallyReal F] [Field K] [NumberField K] [IsTotallyComplex K] [Algebra F K] [Algebra.IsQuadraticExtension F K] : orderOf (complexConj F K) = 2

The complex conjugation is an automorphism of degree 2.

theorem NumberField.CMExtension.zpowers_complexConj_eq_top (F : Type u_1) (K : Type u_2) [Field F] [NumberField F] [IsTotallyReal F] [Field K] [NumberField K] [IsTotallyComplex K] [Algebra F K] [Algebra.IsQuadraticExtension F K] : Subgroup.zpowers (complexConj F K) = ⊤

The complex conjugation generates the Galois group of K/F.

theorem NumberField.CMExtension.eq_maximalRealSubfield {K : Type u_2} [Field K] [NumberField K] [IsTotallyComplex K] (E : Subfield K) [IsTotallyReal ↥E] [Algebra.IsQuadraticExtension (↥E) K] : E = maximalRealSubfield K

noncomputable def NumberField.CMExtension.equivMaximalRealSubfield (F : Type u_1) (K : Type u_2) [Field F] [NumberField F] [IsTotallyReal F] [Field K] [NumberField K] [IsTotallyComplex K] [Algebra F K] [Algebra.IsQuadraticExtension F K] : F ≃+* ↥(maximalRealSubfield K)

Any field F such that K/F is a CM-extension is isomorphic to the maximal real subfield of K.

Equations

• NumberField.CMExtension.equivMaximalRealSubfield F K = (algebraMap F K).rangeRestrictFieldEquiv.trans (RingEquiv.subfieldCongr ⋯)

@[simp]

theorem NumberField.CMExtension.equivMaximalRealSubfield_apply (F : Type u_1) (K : Type u_2) [Field F] [NumberField F] [IsTotallyReal F] [Field K] [NumberField K] [IsTotallyComplex K] [Algebra F K] [Algebra.IsQuadraticExtension F K] (x : F) : ↑((equivMaximalRealSubfield F K) x) = (algebraMap F K) x

@[simp]

theorem NumberField.CMExtension.algebraMap_equivMaximalRealSubfield_symm_apply (F : Type u_1) (K : Type u_2) [Field F] [NumberField F] [IsTotallyReal F] [Field K] [NumberField K] [IsTotallyComplex K] [Algebra F K] [Algebra.IsQuadraticExtension F K] (x : ↥(maximalRealSubfield K)) : (algebraMap F K) ((equivMaximalRealSubfield F K).symm x) = (algebraMap (↥(maximalRealSubfield K)) K) x

class NumberField.IsCMField (K : Type u_1) [Field K] [NumberField K] [IsTotallyComplex K] : Prop

A number field K is CM if K is a totally complex quadratic extension of its maximal real subfield.

• is_quadratic : Algebra.IsQuadraticExtension (↥(maximalRealSubfield K)) K

theorem NumberField.IsCMField.ofCMExtension (F : Type u_1) (K : Type u_2) [Field K] [NumberField K] [IsTotallyComplex K] [Field F] [NumberField F] [IsTotallyReal F] [Algebra F K] [Algebra.IsQuadraticExtension F K] : IsCMField K

theorem NumberField.IsCMField.of_forall_isConj (K : Type u_2) [Field K] [NumberField K] [IsTotallyComplex K] {σ : K ≃ₐ[ℚ] K} (hσ : ∀ (φ : K →+* ℂ), ComplexEmbedding.IsConj φ σ) : IsCMField K

A totally complex field that has a unique complex conjugation is CM.

instance NumberField.IsCMField.of_isMulCommutative (K : Type u_2) [Field K] [NumberField K] [IsTotallyComplex K] [IsGalois ℚ K] [IsMulCommutative (K ≃ₐ[ℚ] K)] : IsCMField K

A totally complex abelian extension of ℚ is CM.

instance NumberField.IsCMField.isQuadraticExtension (K : Type u_2) [Field K] [NumberField K] [IsTotallyComplex K] [IsCMField K] : Algebra.IsQuadraticExtension (↥(maximalRealSubfield K)) K

noncomputable instance NumberField.IsCMField.starRing (K : Type u_2) [Field K] [NumberField K] [IsTotallyComplex K] [IsCMField K] : StarRing K

Equations

• NumberField.IsCMField.starRing K = { star := ⇑(NumberField.CMExtension.complexConj (↥(NumberField.maximalRealSubfield K)) K), star_involutive := ⋯, star_mul := ⋯, star_add := ⋯ }

theorem NumberField.IsCMField.card_infinitePlace_eq_card_infinitePlace (K : Type u_2) [Field K] [NumberField K] [IsTotallyComplex K] [IsCMField K] : Fintype.card (InfinitePlace ↥(maximalRealSubfield K)) = Fintype.card (InfinitePlace K)

theorem NumberField.IsCMField.units_rank_eq_units_rank (K : Type u_2) [Field K] [NumberField K] [IsTotallyComplex K] [IsCMField K] : Units.rank ↥(maximalRealSubfield K) = Units.rank K