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 number 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 number field K is totally complex if all of its infinite places are complex.

Tags

number field, infinite places, totally real, totally complex

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

A number 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] [NumberField K] : IsTotallyReal K ↔ ∀ (v : InfinitePlace K), v.IsReal

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

@[simp]

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

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

instance NumberField.instIsTotallyRealRat : IsTotallyReal ℚ

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

A number 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] [NumberField K] : IsTotallyComplex K ↔ ∀ (v : InfinitePlace K), v.IsComplex

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

@[simp]

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

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