Totally real and totally complex number fields

This file defines the type of totally real and totally complex number fields.

Main Definitions and Results

• NumberField.IsTotallyReal: a field K is totally real if all of its infinite places are real. In other words, the image of every ring homomorphism K → ℂ is a subset of ℝ.
• NumberField.IsTotallyComplex: a field K is totally complex if all of its infinite places are complex.
• NumberField.maximalRealSubfield: the maximal real subfield of K. It is totally real, see NumberField.isTotallyReal_maximalRealSubfield, and contains all the other totally real subfields of K, see NumberField.IsTotallyReal.le_maximalRealSubfield

Tags

number field, infinite places, totally real, totally complex

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

A field K is totally real if all of its infinite places are real. In other words, the image of every ring homomorphism K → ℂ is a subset of ℝ.

• isReal (v : InfinitePlace K) : v.IsReal

theorem NumberField.isTotallyReal_iff (K : Type u_1) [Field K] : IsTotallyReal K ↔ ∀ (v : InfinitePlace K), v.IsReal

theorem NumberField.nrComplexPlaces_eq_zero_iff {K : Type u_2} [Field K] [NumberField K] : InfinitePlace.nrComplexPlaces K = 0 ↔ IsTotallyReal K

theorem NumberField.IsTotallyReal.complexEmbedding_isReal {K : Type u_2} [Field K] [IsTotallyReal K] (φ : K →+* ℂ) : ComplexEmbedding.IsReal φ

@[simp]

theorem NumberField.IsTotallyReal.mult_eq {K : Type u_2} [Field K] [IsTotallyReal K] (w : InfinitePlace K) : w.mult = 1

theorem NumberField.IsTotallyReal.ofRingEquiv {F : Type u_1} [Field F] {K : Type u_2} [Field K] [IsTotallyReal F] (f : F ≃+* K) : IsTotallyReal K

theorem NumberField.IsTotallyReal.of_algebra (F : Type u_1) [Field F] (K : Type u_2) [Field K] [IsTotallyReal K] [Algebra F K] [Algebra.IsAlgebraic F K] : IsTotallyReal F

theorem NumberField.isTotallyReal_iff_ofRingEquiv {F : Type u_1} [Field F] {K : Type u_2} [Field K] (f : F ≃+* K) : IsTotallyReal F ↔ IsTotallyReal K

@[simp]

theorem NumberField.isTotallyReal_top_iff {K : Type u_2} [Field K] : IsTotallyReal ↥⊤ ↔ IsTotallyReal K

instance NumberField.instIsTotallyRealSubtypeMemIntermediateFieldRatOfIsAlgebraic {K : Type u_2} [Field K] [IsTotallyReal K] [CharZero K] (F : IntermediateField ℚ K) [Algebra.IsAlgebraic (↥F) K] : IsTotallyReal ↥F

instance NumberField.instIsTotallyRealSubtypeMemSubfieldOfIsAlgebraic {K : Type u_2} [Field K] [IsTotallyReal K] (F : Subfield K) [Algebra.IsAlgebraic (↥F) K] : IsTotallyReal ↥F

@[simp]

theorem NumberField.IsTotallyReal.nrComplexPlaces_eq_zero (K : Type u_2) [Field K] [NumberField K] [h : IsTotallyReal K] : InfinitePlace.nrComplexPlaces K = 0

theorem NumberField.IsTotallyReal.finrank (K : Type u_2) [Field K] [NumberField K] [h : IsTotallyReal K] : Module.finrank ℚ K = InfinitePlace.nrRealPlaces K

instance NumberField.instIsTotallyRealRat : IsTotallyReal ℚ

instance NumberField.instIsTotallyRealSubtypeMemSubfieldTop (K : Type u_2) [Field K] [IsTotallyReal K] : IsTotallyReal ↥⊤

instance IntermediateField.isTotallyReal_bot (K : Type u_2) [Field K] [CharZero K] : NumberField.IsTotallyReal ↥⊥

instance Subfield.isTotallyReal_bot (K : Type u_2) [Field K] [CharZero K] : NumberField.IsTotallyReal ↥⊥

def NumberField.maximalRealSubfield (K : Type u_2) [Field K] : Subfield K

The maximal real subfield of K. It is totally real, see NumberField.isTotallyReal_maximalRealSubfield, and contains all the other totally real subfields of K, see NumberField.IsTotallyReal.le_maximalRealSubfield.

Equations

• NumberField.maximalRealSubfield K = { carrier := {x : K | ∀ (φ : K →+* ℂ), star (φ x) = φ x}, mul_mem' := ⋯, one_mem' := ⋯, add_mem' := ⋯, zero_mem' := ⋯, neg_mem' := ⋯, inv_mem' := ⋯ }

theorem NumberField.mem_maximalRealSubfield_iff {K : Type u_2} [Field K] (x : K) : x ∈ maximalRealSubfield K ↔ ∀ (φ : K →+* ℂ), star (φ x) = φ x

theorem NumberField.IsTotallyReal.le_maximalRealSubfield {K : Type u_2} [Field K] (E : Subfield K) [IsTotallyReal ↥E] : E ≤ maximalRealSubfield K

@[simp]

theorem NumberField.IsTotallyReal.maximalRealSubfield_eq_top {K : Type u_2} [Field K] [IsTotallyReal K] : maximalRealSubfield K = ⊤

theorem NumberField.instIsAlgebraicSubtypeMemSubfield {K : Type u_2} [Field K] [CharZero K] [Algebra.IsAlgebraic ℚ K] (k : Subfield K) : Algebra.IsAlgebraic (↥k) K

instance NumberField.isTotallyReal_maximalRealSubfield {K : Type u_2} [Field K] [CharZero K] [Algebra.IsAlgebraic ℚ K] : IsTotallyReal ↥(maximalRealSubfield K)

theorem NumberField.isTotallyReal_iff_le_maximalRealSubfield {K : Type u_2} [Field K] [CharZero K] [Algebra.IsAlgebraic ℚ K] {E : Subfield K} : IsTotallyReal ↥E ↔ E ≤ maximalRealSubfield K

instance NumberField.isTotallyReal_sup {K : Type u_2} [Field K] [CharZero K] [Algebra.IsAlgebraic ℚ K] {E F : Subfield K} [hE : IsTotallyReal ↥E] [hF : IsTotallyReal ↥F] : IsTotallyReal ↥(E ⊔ F)

instance NumberField.isTotallyReal_iSup {K : Type u_2} [Field K] [CharZero K] [Algebra.IsAlgebraic ℚ K] {ι : Type u_3} {k : ι → Subfield K} [∀ (i : ι), IsTotallyReal ↥(k i)] : IsTotallyReal ↥(⨆ (i : ι), k i)

theorem NumberField.maximalRealSubfield_eq_top_iff_isTotallyReal {K : Type u_2} [Field K] [CharZero K] [Algebra.IsAlgebraic ℚ K] : maximalRealSubfield K = ⊤ ↔ IsTotallyReal K

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

A field K is totally complex if all of its infinite places are complex.

• isComplex (v : InfinitePlace K) : v.IsComplex

theorem NumberField.isTotallyComplex_iff (K : Type u_1) [Field K] : IsTotallyComplex K ↔ ∀ (v : InfinitePlace K), v.IsComplex

theorem NumberField.nrRealPlaces_eq_zero_iff {K : Type u_2} [Field K] [NumberField K] : InfinitePlace.nrRealPlaces K = 0 ↔ IsTotallyComplex K

theorem NumberField.IsTotallyComplex.complexEmbedding_not_isReal {K : Type u_2} [Field K] [IsTotallyComplex K] (φ : K →+* ℂ) : ¬ComplexEmbedding.IsReal φ

@[simp]

theorem NumberField.IsTotallyComplex.mult_eq {K : Type u_2} [Field K] [IsTotallyComplex K] (w : InfinitePlace K) : w.mult = 2

theorem NumberField.isTotallyComplex_of_algebra (F : Type u_1) [Field F] (K : Type u_2) [Field K] [Algebra F K] [IsTotallyComplex F] : IsTotallyComplex K

@[simp]

theorem NumberField.IsTotallyComplex.nrRealPlaces_eq_zero (K : Type u_2) [Field K] [NumberField K] [h : IsTotallyComplex K] : InfinitePlace.nrRealPlaces K = 0

theorem NumberField.IsTotallyComplex.finrank (K : Type u_2) [Field K] [NumberField K] [h : IsTotallyComplex K] : Module.finrank ℚ K = 2 * InfinitePlace.nrComplexPlaces K