Documentation

Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex

Totally real and totally complex number fields #

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

Main Definitions and Results #

Tags #

number field, infinite places, totally real, totally complex

source
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 ℝ.

Instances
    source
    theorem NumberField.isTotallyReal_iff (K : Type u_1) [Field K] [NumberField K] :
    IsTotallyReal K ↔ ∀ (v : InfinitePlace K), v.IsReal
    source
    theorem NumberField.nrComplexPlaces_eq_zero_iff {K : Type u_2} [Field K] [NumberField K] :
    InfinitePlace.nrComplexPlaces K = 0 ↔ IsTotallyReal K
    source
    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) :
    IsTotallyReal K
    source
    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] :
    IsTotallyReal F
    source
    instance NumberField.instIsTotallyRealSubtypeMemIntermediateFieldRat {K : Type u_2} [Field K] [NumberField K] [IsTotallyReal K] (F : IntermediateField ℚ K) :
    IsTotallyReal ↥F
    source
    instance NumberField.instIsTotallyRealSubtypeMemSubfield {K : Type u_2} [Field K] [NumberField K] [IsTotallyReal K] (F : Subfield K) :
    IsTotallyReal ↥F
    source
    @[simp]
    theorem NumberField.IsTotallyReal.nrComplexPlaces_eq_zero (K : Type u_2) [Field K] [NumberField K] [h : IsTotallyReal K] :
    InfinitePlace.nrComplexPlaces K = 0
    source
    theorem NumberField.IsTotallyReal.finrank (K : Type u_2) [Field K] [NumberField K] [h : IsTotallyReal K] :
    Module.finrank ℚ K = InfinitePlace.nrRealPlaces K
    source
    instance NumberField.instIsTotallyRealRat :
    IsTotallyReal ℚ
    source
    def NumberField.maximalRealSubfield (K : Type u_2) [Field K] [NumberField 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
    Instances For
      source
      instance NumberField.isTotallyReal_maximalRealSubfield (K : Type u_2) [Field K] [NumberField K] :
      IsTotallyReal ↥(maximalRealSubfield K)
      source
      theorem NumberField.IsTotallyReal.le_maximalRealSubfield {K : Type u_2} [Field K] [NumberField K] (E : Subfield K) [IsTotallyReal ↥E] :
      E ≤ maximalRealSubfield K
      source
      theorem NumberField.isTotallyReal_iff_le_maximalRealSubfield {K : Type u_2} [Field K] [NumberField K] {E : Subfield K} :
      IsTotallyReal ↥E ↔ E ≤ maximalRealSubfield K
      source
      instance NumberField.isTotallyReal_sup {K : Type u_2} [Field K] [NumberField K] {E F : Subfield K} [IsTotallyReal ↥E] [IsTotallyReal ↥F] :
      IsTotallyReal ↥(E ⊔ F)
      source
      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)
      source
      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.

      Instances
        source
        theorem NumberField.isTotallyComplex_iff (K : Type u_1) [Field K] [NumberField K] :
        IsTotallyComplex K ↔ ∀ (v : InfinitePlace K), v.IsComplex
        source
        theorem NumberField.nrRealPlaces_eq_zero_iff {K : Type u_1} [Field K] [NumberField K] :
        InfinitePlace.nrRealPlaces K = 0 ↔ IsTotallyComplex K
        source
        @[simp]
        theorem NumberField.IsTotallyComplex.nrRealPlaces_eq_zero (K : Type u_1) [Field K] [NumberField K] [h : IsTotallyComplex K] :
        InfinitePlace.nrRealPlaces K = 0
        source
        theorem NumberField.IsTotallyComplex.finrank (K : Type u_1) [Field K] [NumberField K] [h : IsTotallyComplex K] :
        Module.finrank ℚ K = 2 * InfinitePlace.nrComplexPlaces K