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 K⁺ of K.

Main definitions and results

• 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 K⁺ of K.

• NumberField.CMExtension.complexConj_eq_self_iff: all the elements of K fixed by the complex conjugation come from the maximal real subfield F.

• NumberField.CMExtension.indexRealUnits_eq_one_or_two: the index of the subgroup of (𝓞 K)ˣ generated by the real units and the roots of unity is equal to 1 or 2 (see NumberField.IsCMField.indexRealUnits_eq_two_iff for the computation of this index).

• NumberField.IsCMField.regulator_div_regulator_eq_two_pow_mul_indexRealUnits_inv: ratio of regulators of K and 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 results are proved for the case of a CM field, that is K is totally complex quadratic extension of its totally real. These results live in the NumberField.IsCMField namespace. Some results deal with the general case K/F, where K is totally complex, F is totally real and K is a quadratic extension of F, and live in the NumberField.CMExtension namespace. Note that results for the general case can be deduced for the CM case by using the isomorphism equivMaximalRealSubfield between F and K⁺ mentioned above.

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

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

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

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

instance NumberField.IsCMField.isTotallyComplex (K : Type u_1) [Field K] [NumberField K] [IsCMField K] : IsTotallyComplex K

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

noncomputable def NumberField.IsCMField.equivInfinitePlace (K : Type u_1) [Field K] [NumberField K] [IsCMField K] : InfinitePlace K ≃ InfinitePlace ↥(maximalRealSubfield K)

The equiv between the infinite places of K and the infinite places of K⁺ induced by the restriction to K⁺, see equivInfinitePlace_apply.

Equations

• NumberField.IsCMField.equivInfinitePlace K = Equiv.ofBijective (fun (w : NumberField.InfinitePlace K) => w.comap (algebraMap (↥(NumberField.maximalRealSubfield K)) K)) ⋯

@[simp]

theorem NumberField.IsCMField.equivInfinitePlace_apply (K : Type u_1) [Field K] [NumberField K] [IsCMField K] (w : InfinitePlace K) : (equivInfinitePlace K) w = w.comap (algebraMap (↥(maximalRealSubfield K)) K)

@[simp]

theorem NumberField.IsCMField.equivInfinitePlace_symm_apply (K : Type u_1) [Field K] [NumberField K] [IsCMField K] (w : InfinitePlace ↥(maximalRealSubfield K)) (x : ↥(maximalRealSubfield K)) : ((equivInfinitePlace K).symm w) ((algebraMap (↥(maximalRealSubfield K)) K) x) = w x

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

theorem NumberField.IsCMField.exists_isConj (K : Type u_1) [Field K] [NumberField K] [IsCMField K] (φ : K →+* ℂ) : ∃ (σ : Gal(K/↥(maximalRealSubfield K))), ComplexEmbedding.IsConj φ σ

theorem NumberField.IsCMField.isConj_eq_isConj (K : Type u_1) [Field K] [NumberField K] [IsCMField K] {φ ψ : K →+* ℂ} {σ τ : Gal(K/↥(maximalRealSubfield K))} (hφ : ComplexEmbedding.IsConj φ σ) (hψ : ComplexEmbedding.IsConj ψ τ) : σ = τ

All the conjugations of a CM-field over its maximal real subfield are the same.

noncomputable def NumberField.IsCMField.complexConj (K : Type u_1) [Field K] [NumberField K] [IsCMField K] : Gal(K/↥(maximalRealSubfield K))

The complex conjugation of the CM-field K.

Equations

• NumberField.IsCMField.complexConj K = ⋯.choose

theorem NumberField.IsCMField.isConj_complexConj (K : Type u_1) [Field K] [NumberField K] [IsCMField K] (φ : K →+* ℂ) : ComplexEmbedding.IsConj φ (complexConj K)

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

@[simp]

theorem NumberField.IsCMField.complexEmbedding_complexConj (K : Type u_1) [Field K] [NumberField K] [IsCMField K] (φ : K →+* ℂ) (x : K) : φ ((complexConj K) x) = (starRingEnd ℂ) (φ x)

@[simp]

theorem NumberField.IsCMField.infinitePlace_complexConj (K : Type u_1) [Field K] [NumberField K] [IsCMField K] (w : InfinitePlace K) (x : K) : w ((complexConj K) x) = w x

@[simp]

theorem NumberField.IsCMField.complexConj_apply_apply (K : Type u_1) [Field K] [NumberField K] [IsCMField K] (x : K) : (complexConj K) ((complexConj K) x) = x

theorem NumberField.IsCMField.complexConj_ne_one (K : Type u_1) [Field K] [NumberField K] [IsCMField K] : complexConj K ≠ 1

@[simp]

theorem NumberField.IsCMField.complexConj_apply_eq_self (K : Type u_1) [Field K] [NumberField K] [IsCMField K] (x : ↥(maximalRealSubfield K)) : (complexConj K) ↑x = ↑x

theorem NumberField.IsCMField.orderOf_complexConj (K : Type u_1) [Field K] [NumberField K] [IsCMField K] : orderOf (complexConj K) = 2

The complex conjugation is an automorphism of degree 2.

theorem NumberField.IsCMField.zpowers_complexConj_eq_top (K : Type u_1) [Field K] [NumberField K] [IsCMField K] : Subgroup.zpowers (complexConj K) = ⊤

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

@[simp]

theorem NumberField.IsCMField.complexConj_eq_self_iff (K : Type u_1) [Field K] [NumberField K] [IsCMField K] (x : K) : (complexConj K) x = x ↔ x ∈ maximalRealSubfield K

An element of K is fixed by the complex conjugation iff it lies in K⁺.

theorem NumberField.IsCMField.RingOfIntegers.complexConj_eq_self_iff (K : Type u_1) [Field K] [NumberField K] [IsCMField K] (x : RingOfIntegers K) : (complexConj K) ↑x = ↑x ↔ ∃ (y : RingOfIntegers ↥(maximalRealSubfield K)), (algebraMap (RingOfIntegers ↥(maximalRealSubfield K)) K) y = ↑x

theorem NumberField.IsCMField.Units.complexConj_eq_self_iff (K : Type u_1) [Field K] [NumberField K] [IsCMField K] (u : (RingOfIntegers K)ˣ) : (complexConj K) ((algebraMap (RingOfIntegers K) K) ↑u) = (algebraMap (RingOfIntegers K) K) ↑u ↔ ∃ (v : (RingOfIntegers ↥(maximalRealSubfield K))ˣ), (algebraMap (RingOfIntegers ↥(maximalRealSubfield K)) K) ↑v = (algebraMap (RingOfIntegers K) K) ↑u

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

Equations

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

@[reducible, inline]

noncomputable abbrev NumberField.IsCMField.ringOfIntegersComplexConj (K : Type u_1) [Field K] [NumberField K] [IsCMField K] : RingOfIntegers K ≃ₐ[RingOfIntegers ↥(maximalRealSubfield K)] RingOfIntegers K

A variant of the complex conjugation defined as an AlgEquiv on the ring of integers.

Equations

• NumberField.IsCMField.ringOfIntegersComplexConj K = NumberField.RingOfIntegers.mapAlgEquiv (NumberField.IsCMField.complexConj K)

@[simp]

theorem NumberField.IsCMField.coe_ringOfIntegersComplexConj (K : Type u_1) [Field K] [NumberField K] [IsCMField K] (x : RingOfIntegers K) : ↑((ringOfIntegersComplexConj K) x) = (complexConj K) ↑x

theorem NumberField.IsCMField.ringOfIntegersComplexConj_eq_self_iff (K : Type u_1) [Field K] [NumberField K] [IsCMField K] (x : RingOfIntegers K) : (ringOfIntegersComplexConj K) x = x ↔ x ∈ Set.range ⇑(algebraMap (RingOfIntegers ↥(maximalRealSubfield K)) (RingOfIntegers K))

@[reducible, inline]

noncomputable abbrev NumberField.IsCMField.unitsComplexConj (K : Type u_1) [Field K] [NumberField K] [IsCMField K] : (RingOfIntegers K)ˣ ≃* (RingOfIntegers K)ˣ

The complex conjugation as an isomorphism of the units of K.

Equations

• NumberField.IsCMField.unitsComplexConj K = Units.mapEquiv ↑(NumberField.RingOfIntegers.mapRingEquiv (NumberField.IsCMField.complexConj K).toRingEquiv)

def NumberField.IsCMField.realUnits (K : Type u_1) [Field K] [NumberField K] : Subgroup (RingOfIntegers K)ˣ

The subgroup of (𝓞 K)ˣ generated by the units of K⁺. These units are exactly the units fixed by the complex conjugation, see IsCMField.unitsComplexConj_eq_self_iff.

Equations

• NumberField.IsCMField.realUnits K = (Units.map ↑(algebraMap (NumberField.RingOfIntegers ↥(NumberField.maximalRealSubfield K)) (NumberField.RingOfIntegers K))).range

theorem NumberField.IsCMField.mem_realUnits_iff (K : Type u_1) [Field K] [NumberField K] (u : (RingOfIntegers K)ˣ) : u ∈ realUnits K ↔ ∃ (v : (RingOfIntegers ↥(maximalRealSubfield K))ˣ), (algebraMap (RingOfIntegers ↥(maximalRealSubfield K)) (RingOfIntegers K)) ↑v = ↑u

theorem NumberField.IsCMField.unitsComplexConj_eq_self_iff (K : Type u_1) [Field K] [NumberField K] [IsCMField K] (u : (RingOfIntegers K)ˣ) : (unitsComplexConj K) u = u ↔ u ∈ realUnits K

@[simp]

theorem NumberField.IsCMField.complexConj_torsion (K : Type u_1) [Field K] [NumberField K] [IsCMField K] (ζ : ↥(Units.torsion K)) : (complexConj K) ((algebraMap (RingOfIntegers K) K) ↑↑ζ) = ((algebraMap (RingOfIntegers K) K) ↑↑ζ)⁻¹

The image of a root of unity by the complex conjugation is its inverse. This is the version of Complex.conj_rootsOfUnity for CM-fields.

theorem NumberField.IsCMField.unitsComplexConj_torsion (K : Type u_1) [Field K] [NumberField K] [IsCMField K] (ζ : ↥(Units.torsion K)) : (unitsComplexConj K) ↑ζ = ↑ζ⁻¹

noncomputable def NumberField.IsCMField.unitsMulComplexConjInv (K : Type u_1) [Field K] [NumberField K] [IsCMField K] : (RingOfIntegers K)ˣ →* ↥(Units.torsion K)

The map (𝓞 K)ˣ →* torsion K defined by u ↦ u * (conj u)⁻¹.

Equations

• One or more equations did not get rendered due to their size.

theorem NumberField.IsCMField.unitsMulComplexConjInv_apply (K : Type u_1) [Field K] [NumberField K] [IsCMField K] (u : (RingOfIntegers K)ˣ) : ↑((unitsMulComplexConjInv K) u) = u * ((unitsComplexConj K) u)⁻¹

@[simp]

theorem NumberField.IsCMField.unitsMulComplexConjInv_apply_torsion (K : Type u_1) [Field K] [NumberField K] [IsCMField K] (ζ : ↥(Units.torsion K)) : (unitsMulComplexConjInv K) ↑ζ = ζ ^ 2

theorem NumberField.IsCMField.map_unitsMulComplexConjInv_torsion (K : Type u_1) [Field K] [NumberField K] [IsCMField K] : Subgroup.map (unitsMulComplexConjInv K) (Units.torsion K) = (powMonoidHom 2).range

The action of unitsMulComplexConjInv of the torsion is the same as the 2-power map.

theorem NumberField.IsCMField.unitsMulComplexConjInv_ker (K : Type u_1) [Field K] [NumberField K] [IsCMField K] : (unitsMulComplexConjInv K).ker = realUnits K

The kernel of unitsMulComplexConjInv is the subgroup of real units.

theorem NumberField.IsCMField.index_unitsMulComplexConjInv_range_dvd (K : Type u_1) [Field K] [NumberField K] [IsCMField K] : (unitsMulComplexConjInv K).range.index ∣ 2

The index of the image of unitsMulComplexConjInv divides 2.

@[reducible, inline]

noncomputable abbrev NumberField.IsCMField.indexRealUnits (K : Type u_1) [Field K] [NumberField K] : ℕ

The index of the subgroup of (𝓞 K)ˣ generated by the real units and the roots of unity. This index is equal to 1 or 2, see indexRealUnits_eq_one_or_two and indexRealUnits_eq_two_iff.

Equations

• NumberField.IsCMField.indexRealUnits K = (NumberField.IsCMField.realUnits K ⊔ NumberField.Units.torsion K).index

theorem NumberField.IsCMField.indexRealUnits_mul_eq (K : Type u_1) [Field K] [NumberField K] [IsCMField K] : indexRealUnits K * (unitsMulComplexConjInv K).range.index = 2

theorem NumberField.IsCMField.indexRealUnits_eq_one_or_two (K : Type u_1) [Field K] [NumberField K] [IsCMField K] : indexRealUnits K = 1 ∨ indexRealUnits K = 2

The index of the subgroup of (𝓞 K)ˣ generated by the real units and the roots of unity is equal to 1 or 2 (see NumberField.IsCMField.indexRealUnits_eq_two_iff for the computation of this index).

theorem NumberField.IsCMField.indexRealUnits_eq_two_iff (K : Type u_1) [Field K] [NumberField K] [IsCMField K] : indexRealUnits K = 2 ↔ ∃ (u : (RingOfIntegers K)ˣ), Subgroup.zpowers ((unitsMulComplexConjInv K) u) = ⊤

The index of the subgroup of (𝓞 K)ˣ generated by the real units and the roots of unity is equal to 2 iff there exists a unit whose image by unitsMulComplexConjInv generates the torsion subgroup of K.

noncomputable def NumberField.IsCMField.realFundSystem (K : Type u_1) [Field K] [NumberField K] [IsCMField K] (i : Fin (Units.rank K)) : (RingOfIntegers K)ˣ

The fundamental system of units of K⁺ as a family of (𝓞 K)ˣ.

Equations

• One or more equations did not get rendered due to their size.

theorem NumberField.IsCMField.closure_realFundSystem_sup_torsion (K : Type u_1) [Field K] [NumberField K] [IsCMField K] : Subgroup.closure (Set.range (realFundSystem K)) ⊔ Units.torsion K = realUnits K ⊔ Units.torsion K

theorem NumberField.IsCMField.regOfFamily_realFunSystem (K : Type u_1) [Field K] [NumberField K] [IsCMField K] : Units.regOfFamily (realFundSystem K) = 2 ^ Units.rank K * Units.regulator ↥(maximalRealSubfield K)

theorem NumberField.IsCMField.regulator_div_regulator_eq_two_pow_mul_indexRealUnits_inv (K : Type u_1) [Field K] [NumberField K] [IsCMField K] : Units.regulator K / Units.regulator ↥(maximalRealSubfield K) = 2 ^ Units.rank K * (↑(indexRealUnits K))⁻¹

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

theorem NumberField.IsCMField.ofCMExtension (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] : IsCMField K

If K/F is a CM-extension then K is a CM-field.

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

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

instance NumberField.CMExtension.of_isMulCommutative (K : Type u_2) [Field K] [NumberField K] [IsTotallyComplex K] [IsGalois ℚ K] [IsMulCommutative Gal(K/ℚ)] : IsCMField K

A totally complex abelian extension of ℚ is CM.