Totally real and totally complex fields at infinite places

An extension of a totally real field is unramified at every infinite place exactly when it is itself totally real. Indeed, a complex place above a real place is precisely a ramified infinite place.

A field containing an element whose square is a negative rational is totally complex: a real embedding would send that element to a real square root of a negative number. A totally complex field, having only complex infinite places, is then unramified at every infinite place in any extension, and in degree 2 it has exactly one such place.

Restricting a real place along a field embedding gives a real place, and the real embedding of the restriction is the composite of the embeddings. For an extension L / k, every place of L lies over its restriction to k. If w lies over v, then w.embedding and its conjugate restrict to v.embedding and its conjugate, in one order or the other.

Main results

• NumberField.IsTotallyReal.of_isUnramifiedAtInfinitePlaces: an everywhere-unramified extension of a totally real field is totally real.
• NumberField.isUnramifiedAtInfinitePlaces_iff_isTotallyReal: the resulting characterization.
• NumberField.isTotallyReal_of_sq_ratCast_of_nonneg: a nonnegative square generating the field forces total reality.
• NumberField.isTotallyComplex_of_sq_ratCast_of_neg: a negative square forces total complexity.
• NumberField.IsUnramifiedAtInfinitePlaces_of_isTotallyComplex: a totally complex base is unramified at all infinite places of any extension.
• NumberField.InfinitePlace.nrComplexPlaces_eq_one_of_finrank_eq_two: a totally complex field of degree 2 — an imaginary quadratic field — has exactly one complex place.
• NumberField.InfinitePlace.even_nrComplexPlaces_iff_zero_lt_discr: Brill's theorem in parity form, the number of complex places is even exactly when the discriminant is positive; hence nrComplexPlaces_eq_zero_of_zero_lt_discr (degree less than 4), nrComplexPlaces_eq_one_of_discr_lt_zero (degree less than 6) and NumberField.IsTotallyReal.of_zero_lt_discr read the signature off the sign of the discriminant in low degree.
• NumberField.InfinitePlace.finrank_sub_nrRealPlaces_div_two_eq_nrComplexPlaces: halving the degree less the real places counts the complex places, for any number field.
• NumberField.InfinitePlace.embedding_of_isReal_comap: the real embedding of a restricted real place.
• NumberField.InfinitePlace.liesOver_comap: a place lies over its restriction.
• NumberField.InfinitePlace.LiesOver.trans: lying over is transitive in a field tower.
• NumberField.InfinitePlace.LiesOver.embedding_comp_eq_and_conjugate_embedding_comp_eq_or: the embedding of a place and its conjugate restrict to the embedding of the place below and its conjugate, in one order or the other.

theorem NumberField.IsTotallyReal.of_isUnramifiedAtInfinitePlaces {K : Type u_1} [Field K] {k : Type u_2} [Field k] [Algebra k K] [IsTotallyReal k] [IsUnramifiedAtInfinitePlaces k K] : IsTotallyReal K

An extension of a totally real field unramified at infinity is totally real. If every infinite place of K is unramified over a totally real field k, then every infinite place of K is real: the only other alternative in InfinitePlace.isUnramified_iff would make its restriction a complex place of k.

theorem NumberField.IsTotallyReal.isUnramifiedAtInfinitePlaces {K : Type u_1} [Field K] {k : Type u_2} [Field k] [Algebra k K] [IsTotallyReal K] : IsUnramifiedAtInfinitePlaces k K

A totally real extension is unramified at every infinite place. Every infinite place of the extension is real, which is the first alternative in InfinitePlace.isUnramified_iff.

@[simp]

theorem NumberField.isUnramifiedAtInfinitePlaces_iff_isTotallyReal {K : Type u_1} [Field K] {k : Type u_2} [Field k] [Algebra k K] [IsTotallyReal k] : IsUnramifiedAtInfinitePlaces k K ↔ IsTotallyReal K

Over a totally real base, an extension is unramified at every infinite place exactly when it is totally real.

theorem NumberField.isTotallyReal_of_sq_ratCast_of_nonneg {K : Type u_1} [Field K] [Algebra ℚ K] {x : K} {r : ℚ} (hx2 : x ^ 2 = (algebraMap ℚ K) r) (hgen : ℚ[x] = ⊤) (hr : 0 ≤ r) : IsTotallyReal K

A field generated by a nonnegative rational square root is totally real. If K = ℚ(x), x² = r, and r ≥ 0, then every complex embedding of K is real. Each embedding sends x to a complex number whose square is the nonnegative real number r, so its imaginary part vanishes; the generator hypothesis determines the embedding on all of K.

theorem NumberField.isTotallyComplex_of_sq_ratCast_of_neg {K : Type u_1} [Field K] [NumberField K] {x : K} {r : ℚ} (hx2 : x ^ 2 = (algebraMap ℚ K) r) (hr : r < 0) : IsTotallyComplex K

A field with a negative square is totally complex. If some x : K has x² = r for a negative rational r, then every infinite place of K is complex.

theorem NumberField.IsUnramifiedAtInfinitePlaces_of_isTotallyComplex {k : Type u_2} {K : Type u_3} [Field k] [Field K] [Algebra k K] [IsTotallyComplex k] : IsUnramifiedAtInfinitePlaces k K

A totally complex base is unramified at all infinite places. Since a totally complex field has only complex infinite places and a complex place never ramifies, every infinite place is unramified in any extension K of a totally complex field k.

theorem NumberField.InfinitePlace.nrComplexPlaces_eq_one_of_finrank_eq_two {K : Type u_1} [Field K] [NumberField K] [IsTotallyComplex K] (hK : Module.finrank ℚ K = 2) : nrComplexPlaces K = 1

A totally complex field of degree 2 has exactly one complex place. Such a field satisfies Module.finrank ℚ K = 2 * nrComplexPlaces K, so degree 2 leaves exactly one complex place; with NumberField.IsTotallyComplex.nrRealPlaces_eq_zero it is the field's only infinite place. This is the imaginary quadratic case.

theorem NumberField.InfinitePlace.finrank_sub_nrRealPlaces_div_two_eq_nrComplexPlaces (K : Type u_1) [Field K] [NumberField K] : (Module.finrank ℚ K - nrRealPlaces K) / 2 = nrComplexPlaces K

Halving the degree less the real places counts the complex places. The degree is r₁ + 2 r₂, so subtracting the real places and halving leaves the complex ones.

theorem NumberField.InfinitePlace.even_nrComplexPlaces_iff_zero_lt_discr (K : Type u_1) [Field K] [NumberField K] : Even (nrComplexPlaces K) ↔ 0 < discr K

Brill's theorem, parity form. The number of complex places is even exactly when the discriminant is positive.

theorem NumberField.InfinitePlace.nrComplexPlaces_eq_zero_of_zero_lt_discr {K : Type u_1} [Field K] [NumberField K] (hd : 0 < discr K) (hK : Module.finrank ℚ K < 4) : nrComplexPlaces K = 0

The signature in degree less than 4, positive discriminant. Such a number field has no complex place.

theorem NumberField.InfinitePlace.nrComplexPlaces_eq_one_of_discr_lt_zero {K : Type u_1} [Field K] [NumberField K] (hd : discr K < 0) (hK : Module.finrank ℚ K < 6) : nrComplexPlaces K = 1

The signature in degree less than 6, negative discriminant. Such a number field has exactly one complex place: the number of complex places is odd and at most 2.

theorem NumberField.IsTotallyReal.of_zero_lt_discr {K : Type u_1} [Field K] [NumberField K] (hd : 0 < discr K) (hK : Module.finrank ℚ K < 4) : IsTotallyReal K

A number field of degree less than 4 with positive discriminant is totally real.

@[simp]

theorem NumberField.InfinitePlace.embedding_of_isReal_comap {K : Type u_1} [Field K] {k : Type u_2} [Field k] (f : k →+* K) {w : InfinitePlace K} (hw : w.IsReal) : embedding_of_isReal ⋯ = (embedding_of_isReal hw).comp f

The real embedding of the restriction of a real place w along f is the real embedding of w composed with f.

instance NumberField.InfinitePlace.liesOver_comap {k : Type u_2} {L : Type u_3} [Field k] [Field L] [Algebra k L] (w : InfinitePlace L) : w.LiesOver (w.comap (algebraMap k L))

An infinite place of L lies over its restriction to k.

Mathlib's AbsoluteValue.LiesOver instance is this statement for AbsoluteValue.under, which is not the spelling InfinitePlace.comap produces, so it is registered here. Constructions indexed by w.comap (algebraMap k L) that consume a LiesOver hypothesis, such as NumberField.LiesOver.completionMap, need it.

theorem NumberField.InfinitePlace.LiesOver.trans {k : Type u_2} {L : Type u_3} {M : Type u_4} [Field k] [Field L] [Field M] [Algebra k L] [Algebra L M] [Algebra k M] [IsScalarTower k L M] (u : InfinitePlace M) (w : InfinitePlace L) (v : InfinitePlace k) [u.LiesOver w] [w.LiesOver v] : u.LiesOver v

Lying over is transitive for infinite places in a field tower.

theorem NumberField.InfinitePlace.LiesOver.embedding_comp_eq_and_conjugate_embedding_comp_eq_or {k : Type u_2} {L : Type u_3} [Field k] [Field L] [Algebra k L] (w : InfinitePlace L) (v : InfinitePlace k) [w.LiesOver v] : w.embedding.comp (algebraMap k L) = v.embedding ∧ (ComplexEmbedding.conjugate w.embedding).comp (algebraMap k L) = ComplexEmbedding.conjugate v.embedding ∨ w.embedding.comp (algebraMap k L) = ComplexEmbedding.conjugate v.embedding ∧ (ComplexEmbedding.conjugate w.embedding).comp (algebraMap k L) = v.embedding

If w lies over v, the embedding of w and its conjugate restrict to the embedding of v and its conjugate, in one order or the other. This pairs the restriction of w.embedding given by InfinitePlace.LiesOver.embedding_comp_eq_or_conjugate_embedding_comp_eq with the matching restriction of its conjugate.