Embeddings of number fields

This file defines the embeddings of a number field into an algebraic closed field.

Main Definitions and Results

• NumberField.Embeddings.range_eval_eq_rootSet_minpoly: let x ∈ K with K number field and let A be an algebraic closed field of char. 0, then the images of x by the embeddings of K in A are exactly the roots in A of the minimal polynomial of x over ℚ.
• NumberField.Embeddings.pow_eq_one_of_norm_eq_one: an algebraic integer whose conjugates are all of norm one is a root of unity.
• NumberField.InfinitePlace: the type of infinite places of a number field K.
• NumberField.InfinitePlace.mk_eq_iff: two complex embeddings define the same infinite place iff they are equal or complex conjugates.
• NumberField.InfinitePlace.prod_eq_abs_norm: the infinite part of the product formula, that is for x ∈ K, we have Π_w ‖x‖_w = |norm(x)| where the product is over the infinite place w and ‖·‖_w is the normalized absolute value for w.

Tags

number field, embeddings, places, infinite places

noncomputable instance NumberField.Embeddings.instFintypeRingHom (K : Type u_1) [Field K] [NumberField K] (A : Type u_2) [Field A] [CharZero A] : Fintype (K →+* A)

There are finitely many embeddings of a number field.

Equations

• NumberField.Embeddings.instFintypeRingHom K A = Fintype.ofEquiv (K →ₐ[ℚ] A) RingHom.equivRatAlgHom.symm

theorem NumberField.Embeddings.card (K : Type u_1) [Field K] [NumberField K] (A : Type u_2) [Field A] [CharZero A] [IsAlgClosed A] : Fintype.card (K →+* A) = Module.finrank ℚ K

The number of embeddings of a number field is equal to its finrank.

instance NumberField.Embeddings.instNonemptyRingHom (K : Type u_1) [Field K] [NumberField K] (A : Type u_2) [Field A] [CharZero A] [IsAlgClosed A] : Nonempty (K →+* A)

theorem NumberField.Embeddings.range_eval_eq_rootSet_minpoly (K : Type u_1) (A : Type u_2) [Field K] [NumberField K] [Field A] [Algebra ℚ A] [IsAlgClosed A] (x : K) : (Set.range fun (φ : K →+* A) => φ x) = (minpoly ℚ x).rootSet A

Let A be an algebraically closed field and let x ∈ K, with K a number field. The images of x by the embeddings of K in A are exactly the roots in A of the minimal polynomial of x over ℚ.

theorem NumberField.Embeddings.coeff_bdd_of_norm_le {K : Type u_1} [Field K] [NumberField K] {A : Type u_2} [NormedField A] [IsAlgClosed A] [NormedAlgebra ℚ A] {B : ℝ} {x : K} (h : ∀ (φ : K →+* A), ‖φ x‖ ≤ B) (i : ℕ) : ‖(minpoly ℚ x).coeff i‖ ≤ (B ⊔ 1) ^ Module.finrank ℚ K * ↑((Module.finrank ℚ K).choose (Module.finrank ℚ K / 2))

theorem NumberField.Embeddings.finite_of_norm_le (K : Type u_1) [Field K] [NumberField K] (A : Type u_2) [NormedField A] [IsAlgClosed A] [NormedAlgebra ℚ A] (B : ℝ) : {x : K | IsIntegral ℤ x ∧ ∀ (φ : K →+* A), ‖φ x‖ ≤ B}.Finite

Let B be a real number. The set of algebraic integers in K whose conjugates are all smaller in norm than B is finite.

theorem NumberField.Embeddings.pow_eq_one_of_norm_eq_one (K : Type u_1) [Field K] [NumberField K] (A : Type u_2) [NormedField A] [IsAlgClosed A] [NormedAlgebra ℚ A] {x : K} (hxi : IsIntegral ℤ x) (hx : ∀ (φ : K →+* A), ‖φ x‖ = 1) : ∃ (n : ℕ) (_ : 0 < n), x ^ n = 1

An algebraic integer whose conjugates are all of norm one is a root of unity.

def NumberField.place {K : Type u_1} [Field K] {A : Type u_2} [NormedDivisionRing A] [Nontrivial A] (φ : K →+* A) : AbsoluteValue K ℝ

An embedding into a normed division ring defines a place of K

Equations

• NumberField.place φ = (IsAbsoluteValue.toAbsoluteValue norm).comp ⋯

@[simp]

theorem NumberField.place_apply {K : Type u_1} [Field K] {A : Type u_2} [NormedDivisionRing A] [Nontrivial A] (φ : K →+* A) (x : K) : (place φ) x = ‖φ x‖

@[reducible, inline]

abbrev NumberField.ComplexEmbedding.conjugate {K : Type u_1} [Field K] (φ : K →+* ℂ) : K →+* ℂ

The conjugate of a complex embedding as a complex embedding.

Equations

• NumberField.ComplexEmbedding.conjugate φ = star φ

@[simp]

theorem NumberField.ComplexEmbedding.conjugate_coe_eq {K : Type u_1} [Field K] (φ : K →+* ℂ) (x : K) : (conjugate φ) x = (starRingEnd ℂ) (φ x)

theorem NumberField.ComplexEmbedding.place_conjugate {K : Type u_1} [Field K] (φ : K →+* ℂ) : place (conjugate φ) = place φ

@[reducible, inline]

abbrev NumberField.ComplexEmbedding.IsReal {K : Type u_1} [Field K] (φ : K →+* ℂ) : Prop

An embedding into ℂ is real if it is fixed by complex conjugation.

Equations

• NumberField.ComplexEmbedding.IsReal φ = IsSelfAdjoint φ

theorem NumberField.ComplexEmbedding.isReal_iff {K : Type u_1} [Field K] {φ : K →+* ℂ} : IsReal φ ↔ conjugate φ = φ

theorem NumberField.ComplexEmbedding.isReal_conjugate_iff {K : Type u_1} [Field K] {φ : K →+* ℂ} : IsReal (conjugate φ) ↔ IsReal φ

def NumberField.ComplexEmbedding.IsReal.embedding {K : Type u_1} [Field K] {φ : K →+* ℂ} (hφ : IsReal φ) : K →+* ℝ

A real embedding as a ring homomorphism from K to ℝ .

Equations

• hφ.embedding = { toFun := fun (x : K) => (φ x).re, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem NumberField.ComplexEmbedding.IsReal.coe_embedding_apply {K : Type u_1} [Field K] {φ : K →+* ℂ} (hφ : IsReal φ) (x : K) : ↑(hφ.embedding x) = φ x

theorem NumberField.ComplexEmbedding.IsReal.comp {K : Type u_1} [Field K] {k : Type u_2} [Field k] (f : k →+* K) {φ : K →+* ℂ} (hφ : IsReal φ) : IsReal (φ.comp f)

theorem NumberField.ComplexEmbedding.isReal_comp_iff {K : Type u_1} [Field K] {k : Type u_2} [Field k] {f : k ≃+* K} {φ : K →+* ℂ} : IsReal (φ.comp ↑f) ↔ IsReal φ

theorem NumberField.ComplexEmbedding.exists_comp_symm_eq_of_comp_eq {K : Type u_1} [Field K] {k : Type u_2} [Field k] [Algebra k K] [IsGalois k K] (φ ψ : K →+* ℂ) (h : φ.comp (algebraMap k K) = ψ.comp (algebraMap k K)) : ∃ (σ : K ≃ₐ[k] K), φ.comp ↑σ.symm = ψ

def NumberField.ComplexEmbedding.IsConj {K : Type u_1} [Field K] {k : Type u_2} [Field k] [Algebra k K] (φ : K →+* ℂ) (σ : K ≃ₐ[k] K) : Prop

IsConj φ σ states that σ : K ≃ₐ[k] K is the conjugation under the embedding φ : K →+* ℂ.

Equations

• NumberField.ComplexEmbedding.IsConj φ σ = (NumberField.ComplexEmbedding.conjugate φ = φ.comp ↑σ)

theorem NumberField.ComplexEmbedding.IsConj.eq {K : Type u_1} [Field K] {k : Type u_2} [Field k] [Algebra k K] {φ : K →+* ℂ} {σ : K ≃ₐ[k] K} (h : IsConj φ σ) (x : K) : φ (σ x) = star (φ x)

theorem NumberField.ComplexEmbedding.IsConj.ext {K : Type u_1} [Field K] {k : Type u_2} [Field k] [Algebra k K] {φ : K →+* ℂ} {σ₁ σ₂ : K ≃ₐ[k] K} (h₁ : IsConj φ σ₁) (h₂ : IsConj φ σ₂) : σ₁ = σ₂

theorem NumberField.ComplexEmbedding.IsConj.ext_iff {K : Type u_1} [Field K] {k : Type u_2} [Field k] [Algebra k K] {φ : K →+* ℂ} {σ₁ σ₂ : K ≃ₐ[k] K} (h₁ : IsConj φ σ₁) : σ₁ = σ₂ ↔ IsConj φ σ₂

theorem NumberField.ComplexEmbedding.IsConj.isReal_comp {K : Type u_1} [Field K] {k : Type u_2} [Field k] [Algebra k K] {φ : K →+* ℂ} {σ : K ≃ₐ[k] K} (h : IsConj φ σ) : IsReal (φ.comp (algebraMap k K))

theorem NumberField.ComplexEmbedding.isConj_one_iff {K : Type u_1} [Field K] {k : Type u_2} [Field k] [Algebra k K] {φ : K →+* ℂ} : IsConj φ 1 ↔ IsReal φ

theorem NumberField.ComplexEmbedding.IsReal.isConjGal_one {K : Type u_1} [Field K] {k : Type u_2} [Field k] [Algebra k K] {φ : K →+* ℂ} : IsReal φ → IsConj φ 1

Alias of the reverse direction of NumberField.ComplexEmbedding.isConj_one_iff.

theorem NumberField.ComplexEmbedding.IsConj.symm {K : Type u_1} [Field K] {k : Type u_2} [Field k] [Algebra k K] {φ : K →+* ℂ} {σ : K ≃ₐ[k] K} (hσ : IsConj φ σ) : IsConj φ σ.symm

theorem NumberField.ComplexEmbedding.isConj_symm {K : Type u_1} [Field K] {k : Type u_2} [Field k] [Algebra k K] {φ : K →+* ℂ} {σ : K ≃ₐ[k] K} : IsConj φ σ.symm ↔ IsConj φ σ

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

An infinite place of a number field K is a place associated to a complex embedding.

Equations

• NumberField.InfinitePlace K = { w : AbsoluteValue K ℝ // ∃ (φ : K →+* ℂ), NumberField.place φ = w }

instance instNonemptyInfinitePlaceOfNumberField (K : Type u_2) [Field K] [NumberField K] : Nonempty (NumberField.InfinitePlace K)

noncomputable def NumberField.InfinitePlace.mk {K : Type u_2} [Field K] (φ : K →+* ℂ) : InfinitePlace K

Return the infinite place defined by a complex embedding φ.

Equations

• NumberField.InfinitePlace.mk φ = ⟨NumberField.place φ, ⋯⟩

instance NumberField.InfinitePlace.instFunLikeReal {K : Type u_4} [Field K] : FunLike (InfinitePlace K) K ℝ

Equations

• NumberField.InfinitePlace.instFunLikeReal = { coe := fun (w : NumberField.InfinitePlace K) (x : K) => ↑w x, coe_injective' := ⋯ }

theorem NumberField.InfinitePlace.coe_apply {K : Type u_4} [Field K] (v : InfinitePlace K) (x : K) : v x = ↑v x

theorem NumberField.InfinitePlace.ext {K : Type u_4} [Field K] (v₁ v₂ : InfinitePlace K) (h : ∀ (k : K), v₁ k = v₂ k) : v₁ = v₂

instance NumberField.InfinitePlace.instMonoidWithZeroHomClassReal {K : Type u_2} [Field K] : MonoidWithZeroHomClass (InfinitePlace K) K ℝ

instance NumberField.InfinitePlace.instNonnegHomClassReal {K : Type u_2} [Field K] : NonnegHomClass (InfinitePlace K) K ℝ

@[simp]

theorem NumberField.InfinitePlace.apply {K : Type u_2} [Field K] (φ : K →+* ℂ) (x : K) : (mk φ) x = Complex.abs (φ x)

noncomputable def NumberField.InfinitePlace.embedding {K : Type u_2} [Field K] (w : InfinitePlace K) : K →+* ℂ

For an infinite place w, return an embedding φ such that w = infinite_place φ .

Equations

• w.embedding = ⋯.choose

@[simp]

theorem NumberField.InfinitePlace.mk_embedding {K : Type u_2} [Field K] (w : InfinitePlace K) : mk w.embedding = w

@[simp]

theorem NumberField.InfinitePlace.mk_conjugate_eq {K : Type u_2} [Field K] (φ : K →+* ℂ) : mk (ComplexEmbedding.conjugate φ) = mk φ

theorem NumberField.InfinitePlace.norm_embedding_eq {K : Type u_2} [Field K] (w : InfinitePlace K) (x : K) : ‖w.embedding x‖ = w x

theorem NumberField.InfinitePlace.eq_iff_eq {K : Type u_2} [Field K] (x : K) (r : ℝ) : (∀ (w : InfinitePlace K), w x = r) ↔ ∀ (φ : K →+* ℂ), ‖φ x‖ = r

theorem NumberField.InfinitePlace.le_iff_le {K : Type u_2} [Field K] (x : K) (r : ℝ) : (∀ (w : InfinitePlace K), w x ≤ r) ↔ ∀ (φ : K →+* ℂ), ‖φ x‖ ≤ r

theorem NumberField.InfinitePlace.pos_iff {K : Type u_2} [Field K] {w : InfinitePlace K} {x : K} : 0 < w x ↔ x ≠ 0

@[simp]

theorem NumberField.InfinitePlace.mk_eq_iff {K : Type u_2} [Field K] {φ ψ : K →+* ℂ} : mk φ = mk ψ ↔ φ = ψ ∨ ComplexEmbedding.conjugate φ = ψ

def NumberField.InfinitePlace.IsReal {K : Type u_2} [Field K] (w : InfinitePlace K) : Prop

An infinite place is real if it is defined by a real embedding.

Equations

• w.IsReal = ∃ (φ : K →+* ℂ), NumberField.ComplexEmbedding.IsReal φ ∧ NumberField.InfinitePlace.mk φ = w

def NumberField.InfinitePlace.IsComplex {K : Type u_2} [Field K] (w : InfinitePlace K) : Prop

An infinite place is complex if it is defined by a complex (ie. not real) embedding.

Equations

• w.IsComplex = ∃ (φ : K →+* ℂ), ¬NumberField.ComplexEmbedding.IsReal φ ∧ NumberField.InfinitePlace.mk φ = w

theorem NumberField.InfinitePlace.embedding_mk_eq {K : Type u_2} [Field K] (φ : K →+* ℂ) : (mk φ).embedding = φ ∨ (mk φ).embedding = ComplexEmbedding.conjugate φ

@[simp]

theorem NumberField.InfinitePlace.embedding_mk_eq_of_isReal {K : Type u_2} [Field K] {φ : K →+* ℂ} (h : ComplexEmbedding.IsReal φ) : (mk φ).embedding = φ

theorem NumberField.InfinitePlace.isReal_iff {K : Type u_2} [Field K] {w : InfinitePlace K} : w.IsReal ↔ ComplexEmbedding.IsReal w.embedding

theorem NumberField.InfinitePlace.isComplex_iff {K : Type u_2} [Field K] {w : InfinitePlace K} : w.IsComplex ↔ ¬ComplexEmbedding.IsReal w.embedding

@[simp]

theorem NumberField.InfinitePlace.conjugate_embedding_eq_of_isReal {K : Type u_2} [Field K] {w : InfinitePlace K} (h : w.IsReal) : ComplexEmbedding.conjugate w.embedding = w.embedding

@[simp]

theorem NumberField.InfinitePlace.not_isReal_iff_isComplex {K : Type u_2} [Field K] {w : InfinitePlace K} : ¬w.IsReal ↔ w.IsComplex

@[simp]

theorem NumberField.InfinitePlace.not_isComplex_iff_isReal {K : Type u_2} [Field K] {w : InfinitePlace K} : ¬w.IsComplex ↔ w.IsReal

theorem NumberField.InfinitePlace.isReal_or_isComplex {K : Type u_2} [Field K] (w : InfinitePlace K) : w.IsReal ∨ w.IsComplex

theorem NumberField.InfinitePlace.ne_of_isReal_isComplex {K : Type u_2} [Field K] {w w' : InfinitePlace K} (h : w.IsReal) (h' : w'.IsComplex) : w ≠ w'

theorem NumberField.InfinitePlace.disjoint_isReal_isComplex (K : Type u_2) [Field K] : Disjoint {w : InfinitePlace K | w.IsReal} {w : InfinitePlace K | w.IsComplex}

noncomputable def NumberField.InfinitePlace.embedding_of_isReal {K : Type u_2} [Field K] {w : InfinitePlace K} (hw : w.IsReal) : K →+* ℝ

The real embedding associated to a real infinite place.

Equations

• NumberField.InfinitePlace.embedding_of_isReal hw = ⋯.embedding

@[simp]

theorem NumberField.InfinitePlace.embedding_of_isReal_apply {K : Type u_2} [Field K] {w : InfinitePlace K} (hw : w.IsReal) (x : K) : ↑((embedding_of_isReal hw) x) = w.embedding x

theorem NumberField.InfinitePlace.norm_embedding_of_isReal {K : Type u_2} [Field K] {w : InfinitePlace K} (hw : w.IsReal) (x : K) : ‖(embedding_of_isReal hw) x‖ = w x

@[simp]

theorem NumberField.InfinitePlace.isReal_of_mk_isReal {K : Type u_2} [Field K] {φ : K →+* ℂ} (h : (mk φ).IsReal) : ComplexEmbedding.IsReal φ

theorem NumberField.InfinitePlace.isReal_mk_iff {K : Type u_2} [Field K] {φ : K →+* ℂ} : (mk φ).IsReal ↔ ComplexEmbedding.IsReal φ

theorem NumberField.InfinitePlace.isComplex_mk_iff {K : Type u_2} [Field K] {φ : K →+* ℂ} : (mk φ).IsComplex ↔ ¬ComplexEmbedding.IsReal φ

@[simp]

theorem NumberField.InfinitePlace.not_isReal_of_mk_isComplex {K : Type u_2} [Field K] {φ : K →+* ℂ} (h : (mk φ).IsComplex) : ¬ComplexEmbedding.IsReal φ

noncomputable def NumberField.InfinitePlace.mult {K : Type u_2} [Field K] (w : InfinitePlace K) : ℕ

The multiplicity of an infinite place, that is the number of distinct complex embeddings that define it, see card_filter_mk_eq.

Equations

• w.mult = if w.IsReal then 1 else 2

theorem NumberField.InfinitePlace.mult_pos {K : Type u_2} [Field K] {w : InfinitePlace K} : 0 < w.mult

@[simp]

theorem NumberField.InfinitePlace.mult_ne_zero {K : Type u_2} [Field K] {w : InfinitePlace K} : w.mult ≠ 0

theorem NumberField.InfinitePlace.one_le_mult {K : Type u_2} [Field K] {w : InfinitePlace K} : 1 ≤ ↑w.mult

theorem NumberField.InfinitePlace.card_filter_mk_eq {K : Type u_2} [Field K] [NumberField K] (w : InfinitePlace K) : (Finset.filter (fun (φ : K →+* ℂ) => mk φ = w) Finset.univ).card = w.mult

noncomputable instance NumberField.InfinitePlace.NumberField.InfinitePlace.fintype {K : Type u_2} [Field K] [NumberField K] : Fintype (InfinitePlace K)

Equations

• NumberField.InfinitePlace.NumberField.InfinitePlace.fintype = Set.fintypeRange NumberField.place

theorem NumberField.InfinitePlace.sum_mult_eq {K : Type u_2} [Field K] [NumberField K] : ∑ w : InfinitePlace K, w.mult = Module.finrank ℚ K

noncomputable def NumberField.InfinitePlace.mkReal {K : Type u_2} [Field K] : { φ : K →+* ℂ // ComplexEmbedding.IsReal φ } ≃ { w : InfinitePlace K // w.IsReal }

The map from real embeddings to real infinite places as an equiv

Equations

• NumberField.InfinitePlace.mkReal = Equiv.ofBijective (fun (φ : { φ : K →+* ℂ // NumberField.ComplexEmbedding.IsReal φ }) => ⟨NumberField.InfinitePlace.mk ↑φ, ⋯⟩) ⋯

noncomputable def NumberField.InfinitePlace.mkComplex {K : Type u_2} [Field K] : { φ : K →+* ℂ // ¬ComplexEmbedding.IsReal φ } → { w : InfinitePlace K // w.IsComplex }

The map from nonreal embeddings to complex infinite places

Equations

• NumberField.InfinitePlace.mkComplex = Subtype.map NumberField.InfinitePlace.mk ⋯

@[simp]

theorem NumberField.InfinitePlace.mkReal_coe {K : Type u_2} [Field K] (φ : { φ : K →+* ℂ // ComplexEmbedding.IsReal φ }) : ↑(mkReal φ) = mk ↑φ

@[simp]

theorem NumberField.InfinitePlace.mkComplex_coe {K : Type u_2} [Field K] (φ : { φ : K →+* ℂ // ¬ComplexEmbedding.IsReal φ }) : ↑(mkComplex φ) = mk ↑φ

theorem NumberField.InfinitePlace.prod_eq_abs_norm {K : Type u_2} [Field K] [NumberField K] (x : K) : ∏ w : InfinitePlace K, w x ^ w.mult = ↑|(Algebra.norm ℚ) x|

The infinite part of the product formula : for x ∈ K, we have Π_w ‖x‖_w = |norm(x)| where ‖·‖_w is the normalized absolute value for w.

theorem NumberField.InfinitePlace.one_le_of_lt_one {K : Type u_2} [Field K] [NumberField K] {w : InfinitePlace K} {a : RingOfIntegers K} (ha : a ≠ 0) (h : ∀ ⦃z : InfinitePlace K⦄, z ≠ w → z ↑a < 1) : 1 ≤ w ↑a

theorem NumberField.is_primitive_element_of_infinitePlace_lt {K : Type u_2} [Field K] [NumberField K] {x : RingOfIntegers K} {w : InfinitePlace K} (h₁ : x ≠ 0) (h₂ : ∀ ⦃w' : InfinitePlace K⦄, w' ≠ w → w' ↑x < 1) (h₃ : w.IsReal ∨ |(w.embedding ↑x).re| < 1) : ℚ⟮↑x⟯ = ⊤

theorem NumberField.adjoin_eq_top_of_infinitePlace_lt {K : Type u_2} [Field K] [NumberField K] {x : RingOfIntegers K} {w : InfinitePlace K} (h₁ : x ≠ 0) (h₂ : ∀ ⦃w' : InfinitePlace K⦄, w' ≠ w → w' ↑x < 1) (h₃ : w.IsReal ∨ |(w.embedding ↑x).re| < 1) : Algebra.adjoin ℚ {↑x} = ⊤

@[reducible, inline]

noncomputable abbrev NumberField.InfinitePlace.nrRealPlaces (K : Type u_2) [Field K] [NumberField K] : ℕ

The number of infinite real places of the number field K.

Equations

• NumberField.InfinitePlace.nrRealPlaces K = Fintype.card { w : NumberField.InfinitePlace K // w.IsReal }

@[deprecated NumberField.InfinitePlace.nrRealPlaces (since := "2024-10-24")]

def NumberField.InfinitePlace.NrRealPlaces (K : Type u_2) [Field K] [NumberField K] : ℕ

Alias of NumberField.InfinitePlace.nrRealPlaces.

---

The number of infinite real places of the number field K.

Equations

• NumberField.InfinitePlace.NrRealPlaces = NumberField.InfinitePlace.nrRealPlaces

@[reducible, inline]

noncomputable abbrev NumberField.InfinitePlace.nrComplexPlaces (K : Type u_2) [Field K] [NumberField K] : ℕ

The number of infinite complex places of the number field K.

Equations

• NumberField.InfinitePlace.nrComplexPlaces K = Fintype.card { w : NumberField.InfinitePlace K // w.IsComplex }

@[deprecated NumberField.InfinitePlace.nrComplexPlaces (since := "2024-10-24")]

def NumberField.InfinitePlace.NrComplexPlaces (K : Type u_2) [Field K] [NumberField K] : ℕ

Alias of NumberField.InfinitePlace.nrComplexPlaces.

---

The number of infinite complex places of the number field K.

Equations

• NumberField.InfinitePlace.NrComplexPlaces = NumberField.InfinitePlace.nrComplexPlaces

theorem NumberField.InfinitePlace.card_real_embeddings (K : Type u_2) [Field K] [NumberField K] : Fintype.card { φ : K →+* ℂ // ComplexEmbedding.IsReal φ } = nrRealPlaces K

theorem NumberField.InfinitePlace.card_eq_nrRealPlaces_add_nrComplexPlaces (K : Type u_2) [Field K] [NumberField K] : Fintype.card (InfinitePlace K) = nrRealPlaces K + nrComplexPlaces K

theorem NumberField.InfinitePlace.card_complex_embeddings (K : Type u_2) [Field K] [NumberField K] : Fintype.card { φ : K →+* ℂ // ¬ComplexEmbedding.IsReal φ } = 2 * nrComplexPlaces K

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

theorem NumberField.InfinitePlace.nrComplexPlaces_eq_zero_of_finrank_eq_one {K : Type u_2} [Field K] [NumberField K] (h : Module.finrank ℚ K = 1) : nrComplexPlaces K = 0

theorem NumberField.InfinitePlace.nrRealPlaces_eq_one_of_finrank_eq_one {K : Type u_2} [Field K] [NumberField K] (h : Module.finrank ℚ K = 1) : nrRealPlaces K = 1

def NumberField.InfinitePlace.comap {k : Type u_1} [Field k] {K : Type u_2} [Field K] (w : InfinitePlace K) (f : k →+* K) : InfinitePlace k

The restriction of an infinite place along an embedding.

Equations

• w.comap f = ⟨(↑w).comp ⋯, ⋯⟩

@[simp]

theorem NumberField.InfinitePlace.comap_mk {k : Type u_1} [Field k] {K : Type u_2} [Field K] (φ : K →+* ℂ) (f : k →+* K) : (mk φ).comap f = mk (φ.comp f)

theorem NumberField.InfinitePlace.comap_id {K : Type u_2} [Field K] (w : InfinitePlace K) : w.comap (RingHom.id K) = w

theorem NumberField.InfinitePlace.comap_comp {k : Type u_1} [Field k] {K : Type u_2} [Field K] {F : Type u_3} [Field F] (w : InfinitePlace K) (f : F →+* K) (g : k →+* F) : w.comap (f.comp g) = (w.comap f).comap g

theorem NumberField.InfinitePlace.IsReal.comap {k : Type u_1} [Field k] {K : Type u_2} [Field K] (f : k →+* K) {w : InfinitePlace K} (hφ : w.IsReal) : (w.comap f).IsReal

theorem NumberField.InfinitePlace.isReal_comap_iff {k : Type u_1} [Field k] {K : Type u_2} [Field K] (f : k ≃+* K) {w : InfinitePlace K} : (w.comap ↑f).IsReal ↔ w.IsReal

theorem NumberField.InfinitePlace.comap_surjective {k : Type u_1} [Field k] {K : Type u_2} [Field K] [Algebra k K] [Algebra.IsAlgebraic k K] : Function.Surjective fun (x : InfinitePlace K) => x.comap (algebraMap k K)

theorem NumberField.InfinitePlace.mult_comap_le {k : Type u_1} [Field k] {K : Type u_2} [Field K] (f : k →+* K) (w : InfinitePlace K) : (w.comap f).mult ≤ w.mult

theorem NumberField.InfinitePlace.card_mono (k : Type u_1) [Field k] (K : Type u_2) [Field K] [Algebra k K] [NumberField k] [NumberField K] : Fintype.card (InfinitePlace k) ≤ Fintype.card (InfinitePlace K)

instance NumberField.InfinitePlace.instMulActionAlgEquiv {k : Type u_1} [Field k] {K : Type u_2} [Field K] [Algebra k K] : MulAction (K ≃ₐ[k] K) (InfinitePlace K)

The action of the galois group on infinite places.

Equations

• NumberField.InfinitePlace.instMulActionAlgEquiv = MulAction.mk ⋯ ⋯

@[simp]

theorem NumberField.InfinitePlace.instMulActionAlgEquiv_smul_coe_apply {k : Type u_1} [Field k] {K : Type u_2} [Field K] [Algebra k K] (σ : K ≃ₐ[k] K) (w : InfinitePlace K) (a✝ : K) : ↑(SMul.smul σ w) a✝ = ↑w (σ.symm a✝)

theorem NumberField.InfinitePlace.smul_eq_comap {k : Type u_1} [Field k] {K : Type u_2} [Field K] [Algebra k K] (σ : K ≃ₐ[k] K) (w : InfinitePlace K) : σ • w = w.comap ↑σ.symm

@[simp]

theorem NumberField.InfinitePlace.smul_apply {k : Type u_1} [Field k] {K : Type u_2} [Field K] [Algebra k K] (σ : K ≃ₐ[k] K) (w : InfinitePlace K) (x : K) : (σ • w) x = w (σ.symm x)

@[simp]

theorem NumberField.InfinitePlace.smul_mk {k : Type u_1} [Field k] {K : Type u_2} [Field K] [Algebra k K] (σ : K ≃ₐ[k] K) (φ : K →+* ℂ) : σ • mk φ = mk (φ.comp ↑σ.symm)

theorem NumberField.InfinitePlace.comap_smul {k : Type u_1} [Field k] {K : Type u_2} [Field K] {F : Type u_3} [Field F] [Algebra k K] (σ : K ≃ₐ[k] K) (w : InfinitePlace K) {f : F →+* K} : (σ • w).comap f = w.comap ((↑σ.symm).comp f)

theorem NumberField.InfinitePlace.isReal_smul_iff {k : Type u_1} [Field k] {K : Type u_2} [Field K] [Algebra k K] {σ : K ≃ₐ[k] K} {w : InfinitePlace K} : (σ • w).IsReal ↔ w.IsReal

theorem NumberField.InfinitePlace.isComplex_smul_iff {k : Type u_1} [Field k] {K : Type u_2} [Field K] [Algebra k K] {σ : K ≃ₐ[k] K} {w : InfinitePlace K} : (σ • w).IsComplex ↔ w.IsComplex

theorem NumberField.InfinitePlace.ComplexEmbedding.exists_comp_symm_eq_of_comp_eq {k : Type u_1} [Field k] {K : Type u_2} [Field K] [Algebra k K] [IsGalois k K] (φ ψ : K →+* ℂ) (h : φ.comp (algebraMap k K) = ψ.comp (algebraMap k K)) : ∃ (σ : K ≃ₐ[k] K), φ.comp ↑σ.symm = ψ

theorem NumberField.InfinitePlace.exists_smul_eq_of_comap_eq {k : Type u_1} [Field k] {K : Type u_2} [Field K] [Algebra k K] [IsGalois k K] {w w' : InfinitePlace K} (h : w.comap (algebraMap k K) = w'.comap (algebraMap k K)) : ∃ (σ : K ≃ₐ[k] K), σ • w = w'

theorem NumberField.InfinitePlace.mem_orbit_iff {k : Type u_1} [Field k] {K : Type u_2} [Field K] [Algebra k K] [IsGalois k K] {w w' : InfinitePlace K} : w' ∈ MulAction.orbit (K ≃ₐ[k] K) w ↔ w.comap (algebraMap k K) = w'.comap (algebraMap k K)

noncomputable def NumberField.InfinitePlace.orbitRelEquiv {k : Type u_1} [Field k] {K : Type u_2} [Field K] [Algebra k K] [IsGalois k K] : Quotient (MulAction.orbitRel (K ≃ₐ[k] K) (InfinitePlace K)) ≃ InfinitePlace k

The orbits of infinite places under the action of the galois group are indexed by the infinite places of the base field.

Equations

• NumberField.InfinitePlace.orbitRelEquiv = Equiv.ofBijective (Quotient.lift (fun (x : NumberField.InfinitePlace K) => x.comap (algebraMap k K)) ⋯) ⋯

theorem NumberField.InfinitePlace.orbitRelEquiv_apply_mk'' {k : Type u_1} [Field k] {K : Type u_2} [Field K] [Algebra k K] [IsGalois k K] (w : InfinitePlace K) : orbitRelEquiv (Quotient.mk'' w) = w.comap (algebraMap k K)

def NumberField.InfinitePlace.IsUnramified (k : Type u_1) [Field k] {K : Type u_2} [Field K] [Algebra k K] (w : InfinitePlace K) : Prop

An infinite place is unramified in a field extension if the restriction has the same multiplicity.

Equations

• NumberField.InfinitePlace.IsUnramified k w = ((w.comap (algebraMap k K)).mult = w.mult)

theorem NumberField.InfinitePlace.isUnramified_self {K : Type u_2} [Field K] (w : InfinitePlace K) : IsUnramified K w

theorem NumberField.InfinitePlace.IsUnramified.eq {k : Type u_1} [Field k] {K : Type u_2} [Field K] [Algebra k K] {w : InfinitePlace K} (h : IsUnramified k w) : (w.comap (algebraMap k K)).mult = w.mult

theorem NumberField.InfinitePlace.isUnramified_iff_mult_le {k : Type u_1} [Field k] {K : Type u_2} [Field K] [Algebra k K] {w : InfinitePlace K} : IsUnramified k w ↔ w.mult ≤ (w.comap (algebraMap k K)).mult

theorem NumberField.InfinitePlace.IsUnramified.comap_algHom {k : Type u_1} [Field k] {K : Type u_2} [Field K] {F : Type u_3} [Field F] [Algebra k K] [Algebra k F] {w : InfinitePlace F} (h : IsUnramified k w) (f : K →ₐ[k] F) : IsUnramified k (w.comap ↑f)

theorem NumberField.InfinitePlace.IsUnramified.of_restrictScalars {k : Type u_1} [Field k] (K : Type u_2) [Field K] {F : Type u_3} [Field F] [Algebra k K] [Algebra k F] [Algebra K F] [IsScalarTower k K F] {w : InfinitePlace F} (h : IsUnramified k w) : IsUnramified K w

theorem NumberField.InfinitePlace.IsUnramified.comap {k : Type u_1} [Field k] (K : Type u_2) [Field K] {F : Type u_3} [Field F] [Algebra k K] [Algebra k F] [Algebra K F] [IsScalarTower k K F] {w : InfinitePlace F} (h : IsUnramified k w) : IsUnramified k (w.comap (algebraMap K F))

theorem NumberField.InfinitePlace.not_isUnramified_iff {k : Type u_1} [Field k] {K : Type u_2} [Field K] [Algebra k K] {w : InfinitePlace K} : ¬IsUnramified k w ↔ w.IsComplex ∧ (w.comap (algebraMap k K)).IsReal

theorem NumberField.InfinitePlace.isUnramified_iff {k : Type u_1} [Field k] {K : Type u_2} [Field K] [Algebra k K] {w : InfinitePlace K} : IsUnramified k w ↔ w.IsReal ∨ (w.comap (algebraMap k K)).IsComplex

theorem NumberField.InfinitePlace.IsReal.isUnramified (k : Type u_1) [Field k] {K : Type u_2} [Field K] [Algebra k K] {w : InfinitePlace K} (h : w.IsReal) : IsUnramified k w

theorem NumberField.ComplexEmbedding.IsConj.isUnramified_mk_iff {k : Type u_1} [Field k] {K : Type u_2} [Field K] [Algebra k K] {σ : K ≃ₐ[k] K} {φ : K →+* ℂ} (h : IsConj φ σ) : InfinitePlace.IsUnramified k (InfinitePlace.mk φ) ↔ σ = 1

theorem NumberField.InfinitePlace.isUnramified_mk_iff_forall_isConj {k : Type u_1} [Field k] {K : Type u_2} [Field K] [Algebra k K] [IsGalois k K] {φ : K →+* ℂ} : IsUnramified k (mk φ) ↔ ∀ (σ : K ≃ₐ[k] K), ComplexEmbedding.IsConj φ σ → σ = 1

theorem NumberField.InfinitePlace.mem_stabilizer_mk_iff {k : Type u_1} [Field k] {K : Type u_2} [Field K] [Algebra k K] (φ : K →+* ℂ) (σ : K ≃ₐ[k] K) : σ ∈ MulAction.stabilizer (K ≃ₐ[k] K) (mk φ) ↔ σ = 1 ∨ ComplexEmbedding.IsConj φ σ

theorem NumberField.InfinitePlace.IsUnramified.stabilizer_eq_bot {k : Type u_1} [Field k] {K : Type u_2} [Field K] [Algebra k K] {w : InfinitePlace K} (h : IsUnramified k w) : MulAction.stabilizer (K ≃ₐ[k] K) w = ⊥

theorem NumberField.ComplexEmbedding.IsConj.coe_stabilzer_mk {k : Type u_1} [Field k] {K : Type u_2} [Field K] [Algebra k K] {σ : K ≃ₐ[k] K} {φ : K →+* ℂ} (h : IsConj φ σ) : ↑(MulAction.stabilizer (K ≃ₐ[k] K) (InfinitePlace.mk φ)) = {1, σ}

theorem NumberField.InfinitePlace.nat_card_stabilizer_eq_one_or_two (k : Type u_1) [Field k] {K : Type u_2} [Field K] [Algebra k K] (w : InfinitePlace K) : Nat.card ↥(MulAction.stabilizer (K ≃ₐ[k] K) w) = 1 ∨ Nat.card ↥(MulAction.stabilizer (K ≃ₐ[k] K) w) = 2

theorem NumberField.InfinitePlace.isUnramified_iff_stabilizer_eq_bot {k : Type u_1} [Field k] {K : Type u_2} [Field K] [Algebra k K] {w : InfinitePlace K} [IsGalois k K] : IsUnramified k w ↔ MulAction.stabilizer (K ≃ₐ[k] K) w = ⊥

theorem NumberField.InfinitePlace.isUnramified_iff_card_stabilizer_eq_one {k : Type u_1} [Field k] {K : Type u_2} [Field K] [Algebra k K] {w : InfinitePlace K} [IsGalois k K] : IsUnramified k w ↔ Nat.card ↥(MulAction.stabilizer (K ≃ₐ[k] K) w) = 1

theorem NumberField.InfinitePlace.not_isUnramified_iff_card_stabilizer_eq_two {k : Type u_1} [Field k] {K : Type u_2} [Field K] [Algebra k K] {w : InfinitePlace K} [IsGalois k K] : ¬IsUnramified k w ↔ Nat.card ↥(MulAction.stabilizer (K ≃ₐ[k] K) w) = 2

theorem NumberField.InfinitePlace.card_stabilizer {k : Type u_1} [Field k] {K : Type u_2} [Field K] [Algebra k K] {w : InfinitePlace K} [IsGalois k K] : Nat.card ↥(MulAction.stabilizer (K ≃ₐ[k] K) w) = if IsUnramified k w then 1 else 2

theorem NumberField.InfinitePlace.even_nat_card_aut_of_not_isUnramified {k : Type u_1} [Field k] {K : Type u_2} [Field K] [Algebra k K] {w : InfinitePlace K} [IsGalois k K] (hw : ¬IsUnramified k w) : Even (Nat.card (K ≃ₐ[k] K))

theorem NumberField.InfinitePlace.even_card_aut_of_not_isUnramified {k : Type u_1} [Field k] {K : Type u_2} [Field K] [Algebra k K] {w : InfinitePlace K} [IsGalois k K] [FiniteDimensional k K] (hw : ¬IsUnramified k w) : Even (Fintype.card (K ≃ₐ[k] K))

theorem NumberField.InfinitePlace.even_finrank_of_not_isUnramified {k : Type u_1} [Field k] {K : Type u_2} [Field K] [Algebra k K] {w : InfinitePlace K} [IsGalois k K] (hw : ¬IsUnramified k w) : Even (Module.finrank k K)

theorem NumberField.InfinitePlace.isUnramified_smul_iff {k : Type u_1} [Field k] {K : Type u_2} [Field K] [Algebra k K] {σ : K ≃ₐ[k] K} {w : InfinitePlace K} : IsUnramified k (σ • w) ↔ IsUnramified k w

def NumberField.InfinitePlace.IsUnramifiedIn {k : Type u_1} [Field k] (K : Type u_2) [Field K] [Algebra k K] (w : InfinitePlace k) : Prop

A infinite place of the base field is unramified in a field extension if every infinite place over it is unramified.

Equations

• NumberField.InfinitePlace.IsUnramifiedIn K w = ∀ (v : NumberField.InfinitePlace K), v.comap (algebraMap k K) = w → NumberField.InfinitePlace.IsUnramified k v

theorem NumberField.InfinitePlace.isUnramifiedIn_comap {k : Type u_1} [Field k] {K : Type u_2} [Field K] [Algebra k K] [IsGalois k K] {w : InfinitePlace K} : IsUnramifiedIn K (w.comap (algebraMap k K)) ↔ IsUnramified k w

theorem NumberField.InfinitePlace.even_card_aut_of_not_isUnramifiedIn {k : Type u_1} [Field k] {K : Type u_2} [Field K] [Algebra k K] [IsGalois k K] [FiniteDimensional k K] {w : InfinitePlace k} (hw : ¬IsUnramifiedIn K w) : Even (Fintype.card (K ≃ₐ[k] K))

theorem NumberField.InfinitePlace.even_finrank_of_not_isUnramifiedIn {k : Type u_1} [Field k] {K : Type u_2} [Field K] [Algebra k K] [IsGalois k K] {w : InfinitePlace k} (hw : ¬IsUnramifiedIn K w) : Even (Module.finrank k K)

theorem NumberField.InfinitePlace.card_isUnramified (k : Type u_1) [Field k] (K : Type u_2) [Field K] [Algebra k K] [NumberField K] [NumberField k] [IsGalois k K] : (Finset.filter (fun (w : InfinitePlace K) => IsUnramified k w) Finset.univ).card = (Finset.filter (fun (w : InfinitePlace k) => IsUnramifiedIn K w) Finset.univ).card * Module.finrank k K

theorem NumberField.InfinitePlace.card_isUnramified_compl (k : Type u_1) [Field k] (K : Type u_2) [Field K] [Algebra k K] [NumberField K] [NumberField k] [IsGalois k K] : (Finset.filter (fun (w : InfinitePlace K) => IsUnramified k w) Finset.univ)ᶜ.card = (Finset.filter (fun (w : InfinitePlace k) => IsUnramifiedIn K w) Finset.univ)ᶜ.card * (Module.finrank k K / 2)

theorem NumberField.InfinitePlace.card_eq_card_isUnramifiedIn (k : Type u_1) [Field k] (K : Type u_2) [Field K] [Algebra k K] [NumberField K] [NumberField k] [IsGalois k K] : Fintype.card (InfinitePlace K) = (Finset.filter (fun (w : InfinitePlace k) => IsUnramifiedIn K w) Finset.univ).card * Module.finrank k K + (Finset.filter (fun (w : InfinitePlace k) => IsUnramifiedIn K w) Finset.univ)ᶜ.card * (Module.finrank k K / 2)

class IsUnramifiedAtInfinitePlaces (k : Type u_1) [Field k] (K : Type u_2) [Field K] [Algebra k K] : Prop

A field extension is unramified at infinite places if every infinite place is unramified.

• isUnramified (w : NumberField.InfinitePlace K) : NumberField.InfinitePlace.IsUnramified k w

instance IsUnramifiedAtInfinitePlaces.id (K : Type u_2) [Field K] : IsUnramifiedAtInfinitePlaces K K

theorem IsUnramifiedAtInfinitePlaces.trans (k : Type u_1) [Field k] (K : Type u_2) [Field K] (F : Type u_3) [Field F] [Algebra k K] [Algebra k F] [Algebra K F] [IsScalarTower k K F] [h₁ : IsUnramifiedAtInfinitePlaces k K] [h₂ : IsUnramifiedAtInfinitePlaces K F] : IsUnramifiedAtInfinitePlaces k F

theorem IsUnramifiedAtInfinitePlaces.top (k : Type u_1) [Field k] (K : Type u_2) [Field K] (F : Type u_3) [Field F] [Algebra k K] [Algebra k F] [Algebra K F] [IsScalarTower k K F] [h : IsUnramifiedAtInfinitePlaces k F] : IsUnramifiedAtInfinitePlaces K F

theorem IsUnramifiedAtInfinitePlaces.bot (k : Type u_1) [Field k] (K : Type u_2) [Field K] (F : Type u_3) [Field F] [Algebra k K] [Algebra k F] [Algebra K F] [IsScalarTower k K F] [h₁ : IsUnramifiedAtInfinitePlaces k F] [Algebra.IsAlgebraic K F] : IsUnramifiedAtInfinitePlaces k K

theorem NumberField.InfinitePlace.isUnramified (k : Type u_1) [Field k] {K : Type u_2} [Field K] [Algebra k K] [IsUnramifiedAtInfinitePlaces k K] (w : InfinitePlace K) : IsUnramified k w

theorem NumberField.InfinitePlace.isUnramifiedIn {k : Type u_1} [Field k] (K : Type u_2) [Field K] [Algebra k K] [IsUnramifiedAtInfinitePlaces k K] (w : InfinitePlace k) : IsUnramifiedIn K w

theorem IsUnramifiedAtInfinitePlaces_of_odd_card_aut {k : Type u_1} [Field k] {K : Type u_2} [Field K] [Algebra k K] [IsGalois k K] [FiniteDimensional k K] (h : Odd (Fintype.card (K ≃ₐ[k] K))) : IsUnramifiedAtInfinitePlaces k K

theorem IsUnramifiedAtInfinitePlaces_of_odd_finrank {k : Type u_1} [Field k] {K : Type u_2} [Field K] [Algebra k K] [IsGalois k K] (h : Odd (Module.finrank k K)) : IsUnramifiedAtInfinitePlaces k K

theorem IsUnramifiedAtInfinitePlaces.card_infinitePlace (k : Type u_1) [Field k] (K : Type u_2) [Field K] [Algebra k K] [NumberField k] [NumberField K] [IsGalois k K] [IsUnramifiedAtInfinitePlaces k K] : Fintype.card (NumberField.InfinitePlace K) = Fintype.card (NumberField.InfinitePlace k) * Module.finrank k K

theorem IsPrimitiveRoot.nrRealPlaces_eq_zero_of_two_lt {K : Type u_1} [Field K] [NumberField K] {ζ : K} {k : ℕ} (hk : 2 < k) (hζ : IsPrimitiveRoot ζ k) : NumberField.InfinitePlace.nrRealPlaces K = 0

The infinite place of the rationals.

noncomputable def Rat.infinitePlace : NumberField.InfinitePlace ℚ

The infinite place of ℚ, coming from the canonical map ℚ → ℂ.

Equations

• Rat.infinitePlace = NumberField.InfinitePlace.mk (Rat.castHom ℂ)

@[simp]

theorem Rat.infinitePlace_apply (v : NumberField.InfinitePlace ℚ) (x : ℚ) : v x = ↑|x|

instance Rat.instSubsingletonInfinitePlace : Subsingleton (NumberField.InfinitePlace ℚ)

theorem Rat.isReal_infinitePlace : infinitePlace.IsReal

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

instance NumberField.instIsTotallyRealRat : IsTotallyReal ℚ