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 fieldK
is totally real if all of its infinite places are real. In other words, the image of every ring homomorphismK → ℂ
is a subset ofℝ
.NumberField.IsTotallyComplex
: a number fieldK
is totally complex if all of its infinite places are complex.NumberField.maximalRealSubfield
: the maximal real subfield ofK
. It is totally real, seeNumberField.isTotallyReal_maximalRealSubfield
, and contains all the other totally real subfields ofK
, seeNumberField.IsTotallyReal.le_maximalRealSubfield
Tags #
number field, infinite places, totally real, totally complex
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
Instances
theorem
NumberField.IsTotallyReal.ofRingEquiv
{F : Type u_1}
[Field F]
[NumberField F]
{K : Type u_2}
[Field K]
[NumberField K]
[IsTotallyReal F]
(f : F ≃+* K)
:
theorem
NumberField.IsTotallyReal.of_algebra
(F : Type u_1)
[Field F]
[NumberField F]
(K : Type u_2)
[Field K]
[NumberField K]
[IsTotallyReal K]
[Algebra F K]
:
instance
NumberField.instIsTotallyRealSubtypeMemIntermediateFieldRat
{K : Type u_2}
[Field K]
[NumberField K]
[IsTotallyReal K]
(F : IntermediateField ℚ K)
:
instance
NumberField.instIsTotallyRealSubtypeMemSubfield
{K : Type u_2}
[Field K]
[NumberField K]
[IsTotallyReal K]
(F : Subfield K)
:
@[simp]
theorem
NumberField.IsTotallyReal.nrComplexPlaces_eq_zero
(K : Type u_2)
[Field K]
[NumberField K]
[h : IsTotallyReal K]
:
theorem
NumberField.IsTotallyReal.finrank
(K : Type u_2)
[Field K]
[NumberField K]
[h : IsTotallyReal 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
Instances For
theorem
NumberField.IsTotallyReal.le_maximalRealSubfield
{K : Type u_2}
[Field K]
[NumberField K]
(E : Subfield K)
[IsTotallyReal ↥E]
:
theorem
NumberField.isTotallyReal_iff_le_maximalRealSubfield
{K : Type u_2}
[Field K]
[NumberField K]
{E : Subfield K}
:
instance
NumberField.isTotallyReal_sup
{K : Type u_2}
[Field K]
[NumberField K]
{E F : Subfield K}
[IsTotallyReal ↥E]
[IsTotallyReal ↥F]
:
IsTotallyReal ↥(E ⊔ F)
instance
NumberField.isTotallyReal_iSup
{K : Type u_2}
[Field K]
[NumberField K]
{ι : Type u_3}
{k : ι → Subfield K}
[∀ (i : ι), IsTotallyReal ↥(k i)]
:
IsTotallyReal ↥(⨆ (i : ι), k i)
A number field K
is totally complex if all of its infinite places are complex.
- isComplex (v : InfinitePlace K) : v.IsComplex
Instances
@[simp]
theorem
NumberField.IsTotallyComplex.nrRealPlaces_eq_zero
(K : Type u_1)
[Field K]
[NumberField K]
[h : IsTotallyComplex K]
:
theorem
NumberField.IsTotallyComplex.finrank
(K : Type u_1)
[Field K]
[NumberField K]
[h : IsTotallyComplex K]
: